Sophie Coudert
email: sophie.coudert@telecom-paristech.fr

Tullio Joseph Tanzi
email: tullio.tanzi@telecom-paristech.fr

Formal Methods for Safe Design of Autonomous Systems Dedicated to Risk Management

Keywords: Autonomous systems, Formal methods, Safety, Security

A new generation of Autonomous systems (UAVs, ROVERs, etc.) is coming that will help improve the situational awareness and assessment, especially in difficult conditions like disasters. Rescuers should be relieved from time-consuming data collection tasks as much as possible and at the same time, Autonomous systems should assist data collection through a more insightful and automated guidance thanks to advanced sensing capabilities. In order to achieve this vision, two challenges must be addressed though. The first one is to achieve a sufficient autonomy. The second one relates to the reliability with respect to accidental (safety) or even malicious (security) risks. This however requires the design of new embedded architectures to be more autonomous, while mitigating the harm they may potentially cause. Increased complexity and flexibility requires resorting to modelling, simulation and formal verification techniques in order to validate such critical aspects.

Introduction

According to Guhar-Sapir and Hoyois [START_REF] Guha-Sapir | Annual disaster statistical review 2012: The number and trends[END_REF], in 2012, naturally triggered disasters (earthquakes, landslides, and severe weather, such as tropical cyclones, severe storms, floods) killed a total of 9,655 people, and 124.5 million people became victims, worldwide. Although those numbers were well below the 2002-2011 annual averages (107,000 people killed and 268 million victims), economic damages did show an increase to above-average levels (143 billion USD). When a natural disaster occurs in a populated area, it is mandatory to organize disaster management operations quickly and eff ectively in order to assist the population, to reduce the number of victims, and to mitigate the economic consequences [START_REF] Guha-Sapir | Annual disaster statistical review 2012: The number and trends[END_REF], [START_REF] Chatterjee | Subsidence of Kolkata (Calcutta) city, India during the 1990s as observed from space by diff erential synthetic aperture radar interferometry technique[END_REF], [START_REF] Tanzi | T´el´ecoms pour ling´enierie du risque[END_REF], [START_REF] Tanzi | Radio Sciences and Disaster Management[END_REF]. A non-optimal organization causes supplementary losses and delays in resuming the situation to normal (http://www.un-spider.org/). At any time, the rescue teams need immediate and relevant information concerning the situations they have to face: disaster evolution, surviving persons, critical zones, access to refugee camps, spread assistance tools, etc. The required information is provided by a comprehensive data handling system fed with data generally produced by organizations and space agencies involved in the International Charter Space and Major Disasters.

As explained in [START_REF] Tanzi | T´el´ecoms pour ling´enierie du risque[END_REF], new approaches and the use of new technologies are required for a more efficient management, before, during, and after a crisis. Every specific action at each step of the crisis must be specifically taken into account. For that purpose, new dedicated tools and methodologies are required to better handle crisis situations.

We present in this paper a new approach for which a new generation autonomous systems may help improve the response of rescue teams. In particular, we discuss how autonomous systems may support rescue teams and help them to more systematically explore their surroundings. We discuss the important challenges that must be addressed in terms of navigation and detection autonomy, as well as reliability in terms of safety and security, in order to enable the seamless use of such systems by non-experts persons.

Potential Applications of Autonomous Systems

We have identified three critical fields in the relief missions: i) communications and coordination, ii) recognition field, and finally iii) search operations.

During such an event, maintaining a communication link with the various actors of the response on the one hand and with victims on the other hand is crucial. Unfortunately, when the communication infrastructure has been hit, rescue teams rely essentially on radios or satellite communications. This link remains essential even in the face of non-catastrophic circumstances, like for instance a major black-out in a network (electricity, water, etc.).

Autonomous systems might extend the communication range available as they may be deployed as mobile radio relays. They may also convey messages in a disruption tolerant network (DTN) fashion, during their normal operations, typically between the actors involved. Data sensing results have to be communicated as they are produced, and will serve for the coordination of relief operations. In this sense, the systems should also be autonomous in deciding which data to pre-process and to communicate in order to establish operational priorities.

The detection and the monitoring of the impact of natural disasters on terrain are mainly performed by space borne and air borne relying on radio and optical instruments. Due to limitations in the time window observation attached to optical instruments (i.e. no observation at night or in presence of cloud cover), radio observations are available 24/7 and relatively insensitive to atmospheric conditions: these are therefore particularly useful during the "Response phase" when information must be delivered to the disaster cell with a delay as short as possible delay [START_REF] Wilkinson | The Role of the Radio Sciences in the Disaster Management[END_REF], [START_REF] Lefeuvre | International union of radio science, international council for science (icsu), joint board of geospatial information societies (jbgis)[END_REF], [START_REF] Tanzi | The Contribution Of Radio Sciences to Disaster Management[END_REF].

Autonomous systems may bring significant improvements with respect to those issues. They can be easily equipped with various kinds of sensors in addition to optical ones depending on their potential mission. Their capacities make it easy to observe below a cloud cover. For example, search and rescue teams may carry UAVs and deploy them upon need on site, for instance to explore some flooded area in order to find a practicable path to victims, or a ruined building. In this respect, UAVs extend the exploration range of rescue teams while at the same time improving their safety in areas that may reveal dangerous for their own safety. The senseFly UAV has for instance demonstrated the automated mapping capabilities of small drones and how they could improve the lives of victims in the aftermath of the Ha¨ıti 2010 earthquake, by enabling the authorities to quickly draw maps of devastated areas [START_REF] Ackerman | Drone adventures uses uavs to help make the world a better place[END_REF].

After a brief presentation of context and an introduction to safety and security aspects (sections 1 and 2), section 3 is a brief high level introduction to formal methods. Section 4 provides some more concrete example of applying them, in the domain of autonomous systems and risk avoidance. Section 5 is a discussion about present and future development followed by conclusion.

Reliability: Safety and Security

Legal and ethical constraints arise out of potential risks incurred by the use of an autonomous systems with respect to both victims and rescuers. For instance, a UAV crash may cause damages and harm people; as another example, privacy requires the release of any footage of a disaster to be controlled. Satisfying those constraints requires taking into account the risks linked with fault-tolerance (like for instance in case of the violation of real-time deadlines of safety-critical tasks) and security (sensed data piracy, hijacking, etc.) and to prevent them with adequate countermeasures. Mitigating or preventing those risks involves the introduction of multiple security and safety mechanisms into components as well as in the overall architectural design, which we detail per domain below.

A common way to ensure that a sensor (navigation or payload) has not failed or that its data have not been corrupted by interference, noise or attacks is to perform a plausibility check. Those checks can be done on sensor data in isolation. Many embedded functions also rely on the data produced by several sensors, and checks will consist in ensuring their consistency. Typically, the stabilisation system relies on data issued from the gyroscope, altimeter, etc. Such a verification must be used in our system architecture to improve both the safety of critical function and to limit the impact of attacks.

The deployment of Autonomous systems for such applications will also bring up societal challenges. Indeed, the apparition of a UAV may be terrifying to an unprepared victim (Predator Syndrome), which might reduce the eff ectiveness of the detection operations. In contrast, victims may not notice UAVs flying at a high altitude and therefore fail to signal their position as they would for an aircraft. New standards will probably have to be defined in this respect.

Furthermore, in critical applications regarding safety, a solution must be validated before it is applied on the field. It is forbidden to test solutions directly on the real system for safety reasons. Any attempt of modification or intrusion of a safety system must be approached with the utmost care. The proposed solutions must be validated, and, if possible, formally validated. It is the case of prevention systems for accidents, installed on highways. They also are in charge of gathering information in the case of an accident actually occurring. In this context, we aim to provide an approach to validate the behaviour of a critical system before its eff ective realization (rapid prototyping). Since the tests are not covering all the possibilities, we then move to formally verifyingthe critical properties. This formal analysis is made possible by the mathematical grounds used.

Regarding the critical applications, meaning the applications for which a system failure could cause important damages to the people and/or the installations, it is possible to gain enough confidence about the systems functioning by imposing suitable development and validating methods. Norms indicating the methods to follow can be found. For instance, the techniques used in a safety functional analysis highlight external specifications defects that may have gone unnoticed during the various stages of the study. The past few years have witnessed progresses made in the field of operating reliability for the technical parts of risky systems. Nevertheless, some issues still remain:

─ What level of reliability should we allocate to each component? ─ How do we assess this reliability? ─ What are the main default risks? ─ How do we identify them? ─ How do we measure them? ─ …

To conclude this first part, it is necessary to constitute an approach based on formal methodology able to insure the safety of the autonomous system behaviour. Mathematical models and formal methods are tools with interesting features to ensure these objectives.

Formal Methods Overview

As pointed by [START_REF] Sommerville | Chapter 27. formal methods[END_REF] in a chapter about formal methods, mathematical analysis modelling is not new in engineering. The specificity of formal methods is their close relation to computer science, mechanisation and automating. They originate in modern formal logics which characterises reasoning rules as pure shapes and then allow to mechanically check valid reasoning as strict combination of valid rules. The soundness of such reasoning relies on the mathematical proof of each rulethe inference it allows is always true (roughly speaking, in set theory)and on the mathematical proof of the combination principles: combining valid rules leads to valid deductions or inferences. This kind of approach has then been extended to other way of reasoning on mathematical models such as model checking for example which allows to establish properties on state machines by going through all possible states. Thus the first historical interest of formal tools was to avoid human mistakes in reasoning. The profit was a very strong guaranty but the cost was very high. Indeed, formal reasoning requires each elementary step be explicit and is thus very complexe. For example, proving that a+b+c+d+e=e+a+c+b requires multiple application of rules x+y=y+x and (x+y)+z=x+(y+z). Model checking is limited by the number of states of FSM (Finite State Machines), etc. On the other hand, formalizing allows some total or partial automating. As computers were slow, it was of limited interest but as computing capabilities increased a lot, things have changed. And the last three decades have seen the development of many enhancements, complementary technics, associated tools, methodologies, etc. (see [START_REF] Almeida | Chapter 2. An Overview of Formal Methods Tools and Techniques[END_REF]). Thus, although intrinsic complexity and induced cost remains an obstacle to the substantial use of formal methods in industry, the scope of these methods has extended to more than only guaranteeing critical small systems or small critical parts of systems.

Experience around formal methods leads to the emergence of some keys trends in recurrent difficulties to apply them and solutions to overcome these difficulties. These solutions have led to develop knowledge useful beyond the simple aim to rigorously prove properties. Here we summarise this in three points without claiming to be exhaustive.

Abstraction, refinement and early modelling. The idea is simple: omitting information which does not matter with respect to an expected property makes it easier to establish this property. For example, you can ignore identities of people in a queue if you are only interested in the size of the queue. Abstraction provides simpler models and thus significally simplifies applying formal technics. It reduces the number of states of state machines for model checking. It reduces the number of formulas and makes them simpler for logically specified properties. In brief, it makes checking feasible where it would not be without abstraction. The major issue for a reliable guaranty is then to ensure that omitted information actually doesn't matter. Much scientific results in formal methods address this concern: they characterize reliable relations between abstract and concrete models to ensure good abstractions.

As shown by Error! Reference source not found., refinement is the methodological counterpart of abstraction: mathematical relations are similar and the diff erence is the order in which models are produced. Abstraction extracts property-relevant information from a more concrete model while refining adds details to an abstract model to move toward complete model. Properties can be checked at each level and mathematical guaranty about relations between models ensures high level properties are inherited by lower levels. Another similar aspect is composition: diff erent parts or agents of a system can be specified separately and these specifications are then combined using specific rules. Preservation (or not) of properties by composition is also mathematically assured but additional verifications are sometime necessary.

The perfect warranty is proof (interactive or automatic, depending of method) but the amount of induced work often leads to compromises. Despite this restriction, experience shows that using techniques of formal methods and the use of abstraction, very early in the design process seriously improves the reliability of the result. Another gain is early detection of high level design errors. It avoids the enormous cost induced by the late detection and long and costly ex-post checks. Formal guaranty applies only in the case of mathematical models. Human expertise is very important both to design the detailed model corresponding to the real system and to specify the required high level properties.

Diversifying the use of formal models. Not everything can be proved, but once formal model have been produced, they are also used to apply a wide variety of techniques taking benefit of rigor and abstraction. Here we just give an idea of some of these approaches. Formal techniques allow rapid prototyping. Formal model can be animated and, for example, used for validation: a human can observe the global behaviour of the system before it is implemented. Using computing and abstraction, rapid simulation can be implemented by optimized algorithms and although all paths and states of the system are not covered, the automatically tested part of the system is then much more substantial compared to previous simulation approaches. Formal specification can also be used to automatically produce test sets with a good understanding of the scope of these sets. As high level specification describe "what" the system does and not "how", they can be used to provide infered high level results to compare with the expected ones (i.e. they provide an "oracle"). It is well known that confronting two solutions to obtain a safer result is a good approach when these solutions are very diff erent; here the specification plays the role of one solution. Some works exists also about automatic generation of human readable documentation. As development of formal methods is quite recent, complementary tools using their models continue to emerge nowadays and this presentation is not exhaustive. And last but not least, it is widely recognized that formal modelling alone suffices to highly enhance the design process. Indeed as formal specifying is exigent, it forces to make all requirement precise and unambiguous which leads to debugging them at the beginning of the design process, which is very rentable.

Making specification more user-friendly and providing methodologies. Models must properly represent reality and thus be validated by humans. Unfortunately expertise both in application domain and formal notation is rare which compromises the use of formal technics. Tools are developed to overcome this problem. For example, graphical notations are used to describe systems in an intuitive way and the result is then automatically translated into formal description. Previously mentioned animation of models or automatic generation of natural language helps humans to confront formal specifications with their expectations without formal expertise. Such tools are often integrated in environments with associated methodologies combining formal and unformal verifications. Much has been done to make use of formal methods more attractive and convincing and to allow experts of application domain to play their role.

It would be unrealistic to believe that use of formal methods can be done without formal method experts. The way in which specifications are written has a significant impact on the efficiency of the tools or the size of the proofs. Scientific work continues to propose guidelines, methodologies and associated tools for finding good abstraction and structuring. Concrete expertise is also required on tools themselves. For example in some context a semi-automatic theorem prover may be more powerful using a property written "b=a" than using the same property written "a=b". The lack of such expertise is an obstacle but it is an inherent problem as formal methods are recent. The situation is changing and some businesses begin to have their own team of specifiers. For example Parisian metropolitan company (RATP) uses the B method since the nineties and has its own team of specialists.

As formal methods have essentially been developed by mathematicians moving to computer science, they naturally have been initially applied to software engineering. As a paradox, the programmer's world was not familiar with mathematical modelling and it has probably put the brakes on their integration in real practice. Moreover time to market consideration have become more important than safety in this domain and despite all previously presented enhancements, historical cost of formal methods have been dissuasive. Of course, much of these enhancements and specialisations have targeted software engineering. But in general they may be useful for a lot of other disciplines. Logics can not only model software but potentially anything in the world. This appears in recent developments. They have been applied to computer hardware verification and then more generally to hardware-software system design such as embedded systems. Security aspects, i.e protection against attacks are also addressed. More recently, they are extended to cyber-physical systems ( [START_REF] Fitzgerald | Cyber-physical systems design: Formal foundations, methods and integrated tool chains[END_REF] [START_REF] Drechsler | Formal Modeling and Verification of Cyber-Physical Systems[END_REF]) and the question of modelling not only discrete time but also continuous aspects arise. And as illustrated in section 4.3 new applications appear, for example to validate human-machine interaction( [START_REF] Bolton | Using formal verification to evaluate humanautomation interaction: A review[END_REF]).

Today formal methods have attained a certain level of maturity and are relevant to explore new domains and particularly those were safety is crucial. For all these reasons we believe that formal methods may yield interesting benefits to "risk management". And here we focus on autonomous systems in this context.

Autonomous Systems Illustrations

Applications of formal methods already exist in relation to risk management and autonomous systems. In this section we present some of them. The examples of the two first subsections are extracted from our previous works concerning various equipments dedicated to the safety road (cf. 4.1) or autonomous system such as UAV (cf. 4.2). The third one briefly summarise other works in the literature.

Transportation Example: Motorway

In this illustration, taken from [START_REF] Tanzi | Mod´elisation synchrone appliqu´ee la suˆret´e de fonctionnement[END_REF], we adopt a synchronous approach to model and analyse the behaviour of devices related to safety on the highways. This approach provides guarantees on system behaviour and allows you to test its behaviour as soon as the design phases (see Error! Reference source not found.). The selected graphic synchronous model, which is based on the concepts of States and transitions, allows more communication with the users of the system, without recourse to the underlying synchronous language explicitly. Associated tools facilitate the implementation and operation of test scenarios. These tests can also be carried out interactively. Even more interesting is the possibility of formally establishing properties of safety. The knowledge acquired during the design phase, i.e. before the actual performance of the system, can be reflected immediately toward the design team.

The goal is the definition of an information system for the technical data necessary to maintain the level of viability and security of a highway network. The studied solution proposes to use private communication network buried along the motorway to transmit information. The network used is a basic emergency call network (RAU). If a user comes to use emergency phone at the same time as relief, its communication becomes a priority at the expense of any other operation. In case of malfunction of the classic RAU, the system must be able to off er an alternative of taking over and relief by routing the message to the next connection point operational.

Fig. 2. Example of behaviour modelling

Given the formal nature of the model used, it is possible to prove properties related to the model. The technique that we have adopted is that of symbolic model checking. The idea is to explore exhaustively the State space of the model. This assumes that our model has a finite number of states. However, this space while finite can be so large that the audit programs are unable to analyse it. The use of a symbolic evaluation avoids an explicit construction of the state-space and makes it possible to tackle potentially very large areas.

The models are translated into a system of Boolean equations that represent the control of the program. As there are very eff ective techniques based on the BDD (Binary Decision Diagrams) to evaluate the systems of Boolean equations symbolically, we can apply techniques of symbolic verification to our models.

In a simplified way, a security property expresses the fact that, no matter how the system changes, we won't get unwanted situations. Being able to prove this kind of property is naturally important in critical systems. In our applications, we distinguish between diff erent classes of safety properties: i) Combinatorial properties. They express that a predicate is always true for all available states (for example, a mutual exclusion between actions). ii) Properties of sequential type. These properties are usually expressed by formulas of temporal logics. It comes, for example to show that a dangerous succession of actions will never happen.

In conclusion, we thus have very valuable assistance, because the created scenarios correspond to changes that the tester may not even think about. It is clear that this technique may lead the user to discover anomalies deeply hidden in its specifications or design.

Autonomous System: Safety Drone Born

We now illustrate some results obtained from the modelling and validation methodology of a mini-drone aimed at autonomously indoor navigating. This drone was implemented on top of an existing drone platform ( [START_REF] Ranft | 3d perception for autonomous navigation of a lowcost mav using minimal landmarks[END_REF]). It uses a 720p monocular camera to capture 2D images. "Corkscrew flight" allows to reconstruct the UAV 3D environment from the captured 2D images. This requires the synchronization between the motion control (MC) subsystem and the payload management (PM) in charge of image acquisition. The UAV deduces from its environment model flight orders that are sent to the flight control agent. The approach consists in a three-step methodology: (i) model the functions of the system, (ii) capture the candidate hardware architectures, which is defined in terms of processors, buses and memories, and finally (iii) allocate functions and their communications to the resources of the hardware architecture and study the impact of this allocation with respect to the properties assessed.

In the first iterations of the design, the main purpose of validation is not so much to search for possible deadlock situations usually studied on more accurate models than to study the load of processors and platform buses, and the impact of this load on the flight capabilities of the drone.

For instance, one can clearly see that data from the diff erent sensors (video, attitude, altitude) are sent separately to the ComputingNavigationOrders function that fuses them to interpret the scene before sending commands to the FlightControl.

Modelling tools computes the CPU load resulting from a simulation of the diff erent tasks at hand, as well as a simulation of the inter-CPU information flows triggered by function interactions. This can be used to determine that it would be quite safe to run the emergency tasks on the drone CPU for instance. Other simulations about emergency situations have also been successfully performed to verify that this partitioning of functional tasks can support emergency response functions within acceptable real-time constraints.

Other Works

A) B-method, metro and railway story. The numerous uses of the Bmethod [START_REF] Abrial | The B-book: Assigning Programs to Meanings[END_REF][START_REF] Fantechi | Twenty-five years of formal methods and railways: What next?[END_REF][START_REF] Fantechi | Some Trends in Formal Methods Applications to Railway Signaling[END_REF][START_REF] Lecomte | Formally checking large data sets in the railways[END_REF] in the domain of rail transportation [START_REF]Sil4 railway software[END_REF] is an atypical example of successful early introduction of such a kind of method in industrial practice. Indeed, It relies on interactive proving of set theoretic properties, which requires lot of human expertise and manpower. Thus, thirty years ago, it was difficult to convince industry to move to such approaches. Moreover complete implementation of the method supposes to entirely prove the respect of abstract specifications and required properties by final software. This is particularly demanding and binding unlike model checking, for example, which off ers automatic tools and can be applied punctually on some specific aspects of systems. The counterpart is one of the strongest possible guaranties. Success of B method is essentially due to the eff ort made by its designer for proposing a language closed to programming languages, and also to its first well-known real-size application: METEOR, the first driver-free Parisian metro. As French RATP decided to use formal method to off er strong guaranty, they developed their own team of specifier and this first use of B-method has been followed by other ones. Then B-method provider developed a deep expertise and successfully promotes the use of the method for other railway businesses in the world. A lot of these railway applications concern autonomous and automatic systems (driver-free trains, automatic doors, etc.). Error! Reference source not found.. provides a very simplified view of the Bmethod, without any technical consideration. At abstract high level main properties and operations are described without any implementation details. For example, moving can be described without speed considerations. Only necessary order between actions is provided and order depending on implementation choices is ignored. Refining consist in adding details on state and operation steps: introducing speed, door control, etc. Last level is fully deterministic (all order choices have been done) and contains all details of relevant state for software implementation. Language changes during process: high level language handles parallelism while implementation language provides programming language constructs. At each level proof obligations are generated, and proving them (with an interactive prover) ensures that all invariants are satisfied and that low level operation behaviour respects high level operation description. Thus high level invariants have not to be re-proved at low level. This relies on proved mathematical (set theoretic) foundations of the method. To have a total confidence in final software, three other conditions must hold: high level specification is well written, code generation does not introduce errors (there are certified generators) and the computer on which it runs is reliable, of course (which is not in the scope of the method). B) Autonomous vehicle coordination. In this example [START_REF] Asplund | A Formal Approach to Autonomous Vehicle Coordination[END_REF], the addressed problem is coordination of autonomous vehicles and the used technique is "satisfiability decision" (more precisely "satisfying modulo theories"). In mathematical logic, satisfiability and validity are elementary concepts of semantics.

Driver-less vehicles already exist and the state of Nevada even passed legislation allowing them to operate on public roads. One of the main safety requirements is to avoid collisions. As it would be very expensive to put equipments to all crossing, the chosen solution is a distributed one: decision algorithms are located in vehicles which communicate with each other using messages and message acknowledgments.

Satisfiability is well known in logics. Considering a set of properties (logical formulas), the problem is to decide whether all these properties can be true together. Lots of algorithms have been developed and optimized about this. The goal of the authors is to apply this fully automatic proving technique to the vehicle coordination problem. The presented work evaluates feasibility on a simplified but realistic case.

The applied method consists in providing descriptions by way of usual logical formulas. Descriptions concern both the behaviour of a vehicle and the constraints to respect in order to avoid dangerous situations. Vehicles send requests to access areas of the crossing and the communication protocol together with the vehicle behaviours ensure that only one vehicle can occupy an area at any time. Using the satisfiability as technique is then asking the prover if "not safe" is possible, where "not safe" is described by formulas. Authors had to add some invariants (intermediate properties) to help the prover to automatically establish the expected result using Authors also discuss the scope of the case study and find results convincing despite simplifications (essentially, one single crossing).

This approach is interesting from several points of view. Used proof principles, such as induction, are powerful ones and this does not compromise automating. As considered functions have not to be fully interpreted, the modelling can concern continuous time, infinite and dense data sets. For example, location and speed are expressed with reals and they use abstractions such are "near", "far", "safe-distance" for reasoning. These abstraction are mathematically related to the continuous representation (location, speed, etc.). Applying such technique as formal method to the addressed problem is quite recent and the work is academic. Although proof is automatic, it requires expertise to find the "good" invariants for helping the prover; the language is mathematical logic and no user-friendly environment is evocated. Results are promising and authors claim to be aiming for the integration of the approach in a general tool for vehicular applications in the future. C) Confidence in autonomous systems. [START_REF] Heitmeyer | Obtaining trust in autonomous systems: Tools for formal model synthesis and validation[END_REF] concerns military application of autonomous vehicles, but the questions they address are very similar to our ones and the paper is a good illustration of our point, with a lot of relevant references. A serious obstacle to the use of autonomous systems is the lack of human trust in autonomy software. Thus most military UAVs are still under remote monitoring. Authors distinguish two kinds of trust: system trust and operational trust. The first one expects system to do what it is supposed to do. The second one expects system to actually help human to complete tasks successfully. The use of formal methods is presented as a solution to seriously increase both kinds of trust. Authors promote the use of formal models to verify that systems satisfy critical requirements. About this purpose, they mention existing intensive use of model checking and also robot's software synthesis from formal models. And about operational trust they use powerful simulation based on these models and also evocate model checking to validate human-machine interaction. For this, they have developed an approach in which cognitive models predict human behaviour ( [START_REF] Heitmeyer | Building high assurance human-centric decision systems[END_REF]).

[15] focusses on two main practical problems evocated in section 3: how to produce formal models and how to exploit them in a sufficiently intuitive way to be useful for non-specialists. To solve the first problem, they present a tool which synthetises models from graphical representations of scenarios (ESC: Event Sequence Charts). As some information is sometime missing in ESCs, the tool interactively asks for it during synthesis. To solve the second problem they developed a 3D simulator for autonomy software. These developments are intended to complete the FORMAL (FOrmal Requirements Modeling and AnaLysis) toolset they use. FORMAL integrates a lot of tools for checking consistency, generating invariants, simulating and checking properties at each simulation step, and also model checkers, theorem provers, automatic test generation and source code synthesis (many references are given in the paper). It is a good illustration of the variety of services formal methods can off er to guaranty autonomy software, and of current developments to make their use easier.

Discussion About Present and Future

Presented examples illustrate how existing approaches can be used to guaranty reliability of autonomous systems and in particular autonomous for risk management, where safety considerations are not reduced by time-to-market ones. Current methods can be used as they are. But as their development is recent and as they are evolving, future application is promising. From this study we identify some major lines, briefly summarized in the following points. the first two ones are shared with other application domains and the last ones is a short discussion about prospective for the risk area.

Combining methods. All methods are not efficient for the same aspects or properties. For example timed automata may be used for real time constraints but the complexity of timed models leads to avoid them for time independent question. Interactive proof is very powerful but also tedious and costly, thus it should be reserved to chosen aspects. Thus a rich approach would be to combine methods, and also to combine them with non-formal ones. Such approaches already exist. Some merging are easy: for example, as b-method machines are state machine, they can allow some model checking or model animation. Hybrid approaches can strongly enhance confidence in result but require some complementary fundamental research to off er mathematical guaranty of consistence between models of the diff erent methods.

Using formal methods early in design process. As pointed in part 3 experiment shows that using formal methods at requirement and abstract levels is very profitable. A well designed general system (before details are added) is easier to verify, handle and develop. Some approaches such as the B-method or [START_REF] Tanzi | Uavs for humanitarian missions: Autonomy and reliability[END_REF] are intrinsically top-down and another main reason for this is that it makes efficient applying of formal methods easier. Another complementary reason is that applying formal methods to already developed systems implies to extract formal models from low-level descriptions and rebuild abstraction where intentional information have disappeared (replaced by operational one). It requires a difficult reverse engineering process. This delicate process is not easy and potentially error-prone.

Prospective. Paragraph 4.3.C) already shows that new application domains lead to new ideas about how to use formal models. Other recent evolving may be very interesting for the risk field. Among them, let us cite the extension of these methods to cyberphysical-systems: systems with sensors and strong interaction with physical environment. And another very relevant aspect is that formal methods may not only be used to model computing systems but also environment and physical systems. As the B-method presented above is used to develop software, a more recent version targets system modelling ( [START_REF] Abrial | Modeling in Event-B: System and Software Engineering[END_REF]). Theory is similar but methodology is diff erent: operations are replaced by events; high level specifies the problem and low level specifies the solution. As example, [START_REF] Abrial | Modeling in Event-B: System and Software Engineering[END_REF] presents the behaviour of traffic lights controlling the access to an island. The high level specification only says that no more than x cars can be on the island at a same time. The high level property is the real safety and totally abstracts the way to obtain it. Then refinement gradually introduces a bridge, lights, sensors, etc. And only last level introduces the controlling software driving the lights, and its communications with sensors. This approach allows to prove that a solution correctly solves a problem expressed at a pure user level (see also [START_REF] Banach | The Landing Gear Case Study in Hybrid Event-B[END_REF]). Its implementation remains difficult today as efficient decomposition (avoiding that adding an event leads to redo all proofs) is not easy. However guidelines are studied for this [START_REF] Sato | Separation of considerations in event-b refinement toward industrial use[END_REF] and experience shows that with good decomposition the amount of proofs is easily balanced by the benefit of the analysis: proofs can be relatively direct without a lot of distortions to cope with the formalism. It results that beyond designing autonomous systems, it is particularly interesting to explore specialisation of formal methods to risk issues, as people in this field do not have the same needs and the same culture as those working in software development, and as domain requires strong guaranty about multiple aspects.

In order to conceive a risk-sharing system, one must answer those questions well before their exploitation. In this context, it is important to have access to tools allowing the assessment of production and support policies about reliability and efficiency and the systems operational performances, especially its availability, safety, robustness, etc. Using a simulation is part of this process. It allows to support the technological approach upstream and to help overcoming various kinds of difficulties: i) complexity of the system: dynamic, multiple resources interacting, gradual deployment; ii) lack of feedback; iii) necessity of multiple and partial approaches.

Conclusion

The design of autonomous systems, such as Drones for example, intended to carry out complex missions is an important challenge. The realisation of such a stand-alone system designed to evolve in its post-disaster conditions is still more demanding, mainly in the design of the architecture that must support this autonomy with a very good level of security and efficiency.

The use of the techniques of simulation on test cases, coupled with mathematical proof techniques allow to size and check the properties and safety features. The analysis focuses on functional and non-functional properties for safety and performance aspects. This new approach allows us to find the limits and to validate the consistency of complex systems without having to build real prototypes. It also lets us collect information on a new system, low-cost and at an early stage of the project. A lot of dysfunction, when using the system, appears when the operational conditions are diff erent from those defined for the design. Checking and verifying all options in a design is not always possible before its realisation.

Complex systems are difficult to test and validate in extreme conditions. Designers can provide the use of a prototype to refine their approach. However, the prototype can hardly be comprehensive and fully representative of the final behaviour. It goes the same for test conditions. By building a virtual prototype, able to model more critical behaviours, it is possible to reproduce a functioning according to operational conditions. This process integration from the early stages of the project, allows having retroactive eff ect immediately on the design.

Tools of modelling and verification are an important improvement to the mastering of complexity. This allows to improve confidence in performance, safety and security properties needed by the real operational conditions. Moreover, present evolution of formal techniques and recent applications to risk management issues are promising attractive opportunities. Benefits for risk field must be increased and diversified in the future.

Fig. 1 .

 1 Fig. 1. Abstraction -Refinement

Fig. 3 .

 3 Fig. 3. Intuitive overview of the B method


Audrey Fertier
email: audrey.fertier@mines-albi.fr

Anne-Marie Barthe-Delanoë
email: annemarie.barthe@ensiacet.fr

Aurélie Montarnal

Sébastien Truptil

Frédérick Bénaben

The Generation of a Situation Model, in Real-time, as a Support to Crisis Management

Keywords: Modeling, Big Data, Situation Awareness, Crisis Management, Common Operational Picture

There are more and more data sources available in the world every day. This is the opportunity for organizations to improve their situation awareness in order to take better decisions, faster than ever before. The GéNéPi project was set up to help them: it aims to support their collaboration, in real-time, whatever the complexity or instability of the environment. To set up and test the solution proposed by the project's consortium, a crisis use case has been developed by official sources. This article shows a new approach to automating the creation and update of a situation model, in real-time to offer: (i) the decision-makers a common operational picture; (ii) the GéNéPi project a base on which a collaborative process is defined and maintained to the benefits of the decision makers.

Introduction

During a crisis situation, the inter-connection of networks compels the stakeholders to collaborate. To make this collaboration possible, on the field and between the several decisional levels, crisis cells are set up. Their main purpose includes the information sharing and a centralized decision-making. The number of incoming and outgoing communications of the crisis cells quickly takes up everybody's time. Moreover, the innate instability of the situation compels the decision-makers, far from the field, to obtain the best possible situation awareness in real-time.

The growing number of data sources over the last decade is the opportunity to quickly obtain information on the on-going situation. Unfortunately, if the crisis cells want to avoid drowning in raw data and information, they have to limit their investigation area on inner sensors, devices or internal reports. To support the stakeholders' collaboration on the field and relieve the decision-makers, the GéNéPi (The GéNéPi project is funded by the French national association for research. It considers using the innate granularity of the management levels in crisis context to better support coordination (cf. ANR-14-CE28-0029) project aims to design, orchestrate and monitor a re-sponse collaborative process in real time. One innovation involves the automatic generation of a situation model on the basis of raw data. This model is created and updated in two rounds: (i) A ground truth model comes first and describes fact coming directly from trusted data sources; (ii) New information is automatically deduced from the ground truths in regards with the knowledge base, thanks to deduction rules. During these two phases, the system instantiates a model called meta-model (A meta-model can be defined as "explicit specification of an abstraction" [START_REF] Bézivin | Towards a precise definition of the OMG/MDA framework[END_REF]. In the GéNéPi project, the meta-model is a model that describes the crisis collaboration domain.).

This paper presents a new methodology for supporting decision-makers in managing data and information, inside French crisis cells. The output is the situation model that will be used as an input for: (i) the inference and monitoring of the collaborative process; (ii) the generation of a common operational picture for every crisis cell.

To answer these topics, the second part of this article concerns the opportunities and threats brought by the amount of available data in crisis situation. The third one explains how to benefit from the particularities of crisis collaborations. The fourth one focuses on the features of events to be dealt with during a crisis response. Then, the fifth and last part presents two existing approaches answering to the 'how to?' question of the third part, along with a new methodology, answering to all the data features' issues presented in the fourth part.

2

Excessive Amount of Available Data to Be Processed in Real-time According to Ackoff [START_REF] Ackoff | From data to wisdom[END_REF]: data represents 'properties of objects and events', information is 'contained in descriptions' (Who? What? Where? How many?), and knowledge is 'conveyed by instructions' (How to?). This section explains where all this available data comes from, why is it important to manage it all, and how fast data needs to be processed by the crisis cells.

The Decision-makers' Needs

Growing networks of people, devices, and organizations generate more and more data. These data sources are numerous and heterogeneous: they introduce complexity in crisis management at several levels. If the decision-makers want to take advantages of this new situation, they will need to: locate data sources; identify them; infer new information describing the situation; sum up and share their information and knowledge inside the crisis cell; etc. Their goal is to obtain the most reliable and accurate view of the situation, as a common operational picture, to be able to make well-informed decisions [START_REF] Dautun | Placer "l'humain" au coeur des crises[END_REF].

The Time Pressure

A shared situation awareness (SA) can be defined as "the degree to which team members have the same SA on shared SA requirement" [START_REF] Endsley | A model of inter-and intrateam situation awareness: Implications for design, training and measurement . New trends in cooperative activities: Understanding system dynamics in complex environments[END_REF]. This has to be achieved in real-time to fit the innate instability of crisis. To generate it, data and information have to be gathered from the stakeholders involved in the crisis response. Unfortunately, it takes significant and precious time to obtain and spread the right data or information to the right person or device at the right time. That's the reason why, the decision-makers choose to limit the number of their data sources.

Balance Between Swiftness and Quality

Limitations on data collection enable crisis cells to save time for decision-making but it also raises several issues as:

 Outdated perceptions of the situation. The instability of crisis situation makes things nearly impossible to predict. It is then critical to be informed, in time, of any on-going development. The stakeholders involved in a crisis expect systems to respect this 'on-the-fly' requirement and harshly judge failures. For instance, the SAIP application for smartphones [START_REF] Intérieur | Lancement de l'application mobile SAIP[END_REF] turns out useless because of a time lag of three (!) hours [START_REF]French Minister of the Interior[END_REF] during the Nice terrorist attack on July 15 th , 2016.  Misjudging. French crisis cells' emergency plans include meetings that are planned on a regular basis. One of the purposes of these meetings includes the sharing of information and the decision-making based on these information. Nevertheless, the order of the data arrival may lead to various interpretations that impact the resulting decision-making process. For example, the observations of: (a) a crowd movement, (b) few people injured, (c) loud noises can be interpreted in more than on way. If the order of the observations is (a,b,c), the situation can be understood as a classical crowd movement, whereas (c,b,a) where the situation could be due to gun shots.  Information loss. Some data, as weak signals, is by nature not sufficient to attract the attention, as well as some other will not fit the information system of the crisis cells and will be lost for good.

To sum up, the growing number of available data is an incredible opportunity to improve the situation awareness of stakeholders, while facilitating decision-making through an always more accurate situation model. Meanwhile, the stakeholders have to face issues such as time lag, misjudging and information loss. Crisis information systems are then needed, in real-time, to both support the decision-makers [START_REF] Finn | Exploring big 'crisis' data in action: potential positive and negative externalities[END_REF] and generate the best situation model possible in order to generate the expected common operational picture.

How to automatically generate the best situation model possible describing the ongoing collaborative situation, while being on real-time update to match with the innate instability of a crisis?

3

The Generation of a Situation Model in Real-time Data mining may be considered as one of the relevant answers to the automatic generation of a situation model issue. A lot of data mining approaches are rather dedicated to business than to crisis situations, and there are huge differences between the two contexts of application. This section aims to highlight those differences and to define how data mining could be used to serve the management of huge amount of available crisis data, considering the challenging issues underlined in section 2.

Particularities of Data Processing in Industry

Data mining approaches are frequently used by companies to monitor customers' relationships (CRM), or to identify the best market opportunities (BI), with the final objective to support business decision-making. H. Wang and S. Wang [START_REF] Wang | A knowledge management approach to data mining process for business intelligence[END_REF] claim that one strong approach is to use data mining to bond the gap between: (i) the data gathering, data accessing and data analyzing; and (ii) the creation and exploitation of knowledge. They also propose a step that enables the data miners to extract and mine the data, while the business insiders learn from the results and take actions in consequence.

Three hypotheses have been made in this context:

 Data sources known in advance. Business insiders, in connection with data miners, plane data extractions according to their objectives. As the objectives are already known, it is somewhat easy to pick the most interesting data sources and analyze their streams with precise rules.  Narrow scope of decisions. In most of the cases, companies have a precise decomposition of their functions: therefore, the scope of actions that can be taken to solve potential issues, or reach an objective, remains narrow.  Large timeline. The data extraction may be conducted on a broad timeline to enrich the dataset and, hopefully, improve the accuracy and relevancy of the data mining results.

Particularities of Data Processing During the Crisis Response

Data extractions techniques depend on their field of application: objectives-conducted for industrial applications and 'data sources'-oriented for crisis response applications. A wide scope of data sources has to be streamed during a crisis to prevent lack of information, information loss, misunderstandings and snap judgements. This represents a huge data volume as varied as satellite imagery, photographs, reports, social media messages, newspaper articles, GPS locations or sensors data that has to be processed in real-time. If only automated, such a data processing could infer precious knowledge. A valuable output could be a common operational picture consisting of a map where people, actors, risks, facts [START_REF] Norheim-Hagtun | Crowdsourcing for crisis mapping in Haiti[END_REF], sentiments [START_REF] Caragea | Mapping moods: geomapped sentiment analysis during hurricane Sandy[END_REF] or on-going tasks have been localized on the crisis field.

However, crisis situations are far from the industrial cases and hypothesis:

 Fuzzy, unknown data sources. Data miners cannot predict the outcomes of their mining, nor the location of relevant and accurate data. Then, how to access data sources that are not known in advance, knowing that the more they are, the more reliable the result.

 Unpredictable uses.

A data extracted from one data source may refer to several types of information, related or not to the decision-makers objectives. Hence, the classification rules have to be at once permissive to treat as many data as possible, and accurate to meet the decision-makers expectations.  Relevant actions hard to trigger. The number of actions available to answer a risk or treat a bad effect is spreading as the number of stakeholders increases (whatever their operational/strategic level). In addition, performance indicators cannot be preestablished and the results of the response process are hardly assessable in short schedule.  Tight timeline. One single event is enough to trigger or alter a crisis in a very short time. Under these conditions, the IT system should be able to detect such events within minutes.

A Three-level IT System as a Basis to Data Management During Crisis Situation

The particularities of the industry and the crisis field reveal two important differences on: (i) the volume and quality of data that can be extracted in real time; (ii) the volume of possible actions to be taken. This is why there is a high interest in using data streams, not only to maintain a situation model, but also to define and monitor actions.

In this perspective, a three-levels IT system, as depicted in Error! Reference source not found., is needed:  Data. The raw data is directly extracted from heterogeneous and various data sources (such as GIS, sensors, social media...). In the see Error! Reference source not found.Error! Reference source not found., the shadowed part illustrates the existence and needed use of unknown sources. Here, the extracted data are heterogeneous, numerous, more or less reliable and time dated.  Information. This level corresponds to the contextualization of the previous data.

Concretely, the information level aims at providing a state of the crisis situation in real-time. The common operational picture consists of a map where important instances are localized. Once implemented, this could support the decision making inside every crisis cells. A meta-model is used to standardize and facilitate this modelling. The information level is illustrated in white (see Error! Reference source not found.) to show that the modeled information can be easily recover.  Knowledge. It consists of the actions to be taken, considering the crisis situation established at the information level. The actions are, for instance, part of the collaborative process that is: (i) deduced by the GéNéPi partners; and (ii) executed by the stakeholders. There is a wide range of possibilities in the action selection process. The shadowed part illustrates the fact that some actions, unknown at the beginning, have to be discovered in time to improve the quality of the crisis response.

The following sections focus on solutions to process crisis data in real-time and obtain the most relevant information to be put in the situation model. How to automatically generate the best situation model possible describing the ongoing collaborative situation, while being able in real-time update to match with the innate instability of a crisis, thanks to a three-level IT system?

Particularities of Crisis Events' Data

Event can be understood as "the thing that happened" (as defined by Luckham & Schulte and Etzion & Niblett [START_REF] Luckham | Event Processing Glossary -Version 2[END_REF][START_REF] Etzion | Event Processing in Action[END_REF][START_REF] Chandy | Event processing: designing IT systems for agile companies[END_REF]). For example, it could be a tsunami, a water level reaching a threshold, the reception of an email, the new version of a web page, a comment on a Facebook status, etc. Here, they will be called field events. As a field event occurs or is about to occur, another one is created into an information system [START_REF] Luckham | Event processing glossary-version 1.1[END_REF] in the shape of an object, a message or a tuple. In this paper, the last event will be called the IT event and it will at least contain:

 A unique ID  The time of occurrence of the field event  A description of the field event (data or information from the field)

To generate automatically the situation model representing the collaboration on the field, the system needs to describe the context, the partners and the crisis itself. Both the context and the partners can be represented in the preparation phase. That's why the system could focus, at first, on modelling the risks and effects of the crisis.

Overall Descriptions of the Field Events to Be Observed

To be able to avoid mistakes or delays in the generation of the common operational picture, based on the situation model, field events have to be observed through the entire Internet of Events (IoE) defined by Van Der Aalst [START_REF] Aalst | Process mining: discovery, conformance and enhancement of business processes[END_REF]. It consists in four overlapping classes, as described in the following subsections.

The Internet of Things. This class embeds any physical object connected to the network through an Internet connection or thanks to unique ID tags such as barcodes or 'Radio frequency identification' tags. During a crisis, identification systems, like the 'Wireless internet information system for medical response in disasters', are used to report victims' position and medical record during triage [START_REF] Koenig | Koenig and Schultz's Disaster Medicine: Comprehensive Principles and Practices[END_REF].

The Internet of People. These data are generated from social interactions between people. It can be e-mails, messages sent through social networks such as Facebook, Twitter or Instagram. During a crisis, people tend to focus on social media to communicate, or to be informed on the on-going crisis, because of the 1-to-n principle: post only one message on Twitter and n followers will be warned at the same time. This emergent crowdsourcing is particularly interesting in the context of crisis management to support context awareness [START_REF] Meier | Digital Humanitarians: How Big Data Is Changing the Face of Humanitarian Response[END_REF].

The Internet of Locations. It includes any data with a spatial dimension. For instance, Tweets, Facebook posts, even pictures can embed geospatial attributes through the geolocation service provided by modern smartphones and cameras. During a crisis, a significant percentage (49% according to Kouadia and Douvinet [START_REF] Sekedoua Kouadio | Les smartphones peuvent-ils aider à une meilleure remontée des données en cas de crue rapide pour améliorer les systèmes d'alerte ?[END_REF]) of the potential victims has a smartphone and can be localized on a map. This crisis representation can therefore be used as a common operational picture to support local decision-making inside the crisis cells.

The Internet of content. It represents the information created by humans, like web pages, Wikipedia, YouTube, news feeds. During a crisis, official recommendations to assist victims could be transmitted directly to on-site people wanting to help, etc.

As van der Aalst [START_REF] Aalst | Data Scientist: The Engineer of the Future[END_REF] pointed out, event data is the major source of information. Therefore, all these available events are numerous and the data and information they contain is more or less reliable, comes from varied sources, in various types and format, and are time-dated.

Issues Due to the Volume, Variety, Velocity and Veracity of the Data Coming from the Field

Available events describe data and information coming from outside as from: the crisis field, upper crisis cells, lower crisis cells or the Internet. This section describes the characteristics of those heterogeneous inputs. It will focus on data features because an information from one person can be considered as a data by another [START_REF] Lukoianova | Veracity roadmap: Is big data objective, truthful and credible?[END_REF].

The Volume. It refers to the quantity of data generated continuously per time unit. The volume is proportional to the size of the data [START_REF] Demchenko | Addressing big data issues in scientific data infrastructure[END_REF] and therefore to the type of data [START_REF] Krishnan | Data warehousing in the age of big data[END_REF]. A balance has to be found between widening the influence zone and spending energy to process data in time. Yet, the more data, the more creation of hidden information and patterns the decision makers will get [START_REF] Hashem | The rise of "big data" on cloud computing: Review and open research issues[END_REF]. And as the time passes by, the volume of available data continues increasing while the available capacity to process them stays the same [START_REF] Bifet | Mining big data: current status, and forecast to the future[END_REF].

The Variety. It refers to the diversity of data types, as videos or data logs [START_REF] Krishnan | Data warehousing in the age of big data[END_REF][START_REF] Hashem | The rise of "big data" on cloud computing: Review and open research issues[END_REF][START_REF] Bifet | Mining big data: current status, and forecast to the future[END_REF][START_REF] Chalmers | Big Data-State of the Art[END_REF][START_REF] Ohlhorst | Big data analytics: turning big data into big money[END_REF][START_REF] Power | Using 'Big Data'for analytics and decision support[END_REF], and data formats (Either structured, unstructured, semi-structured or mixed data set.), as structured or unstructured sets [START_REF] Demchenko | Addressing big data issues in scientific data infrastructure[END_REF], [START_REF] Hashem | The rise of "big data" on cloud computing: Review and open research issues[END_REF]. Bypass issues linked to variety is possible thanks to metadata identifying what is contained in the actual data [START_REF] Krishnan | Data warehousing in the age of big data[END_REF], even though a lot of details are lost in the process.

The Velocity. It refers to the speed needed to retrieve and process data in time [START_REF] Krishnan | Data warehousing in the age of big data[END_REF][START_REF] Bifet | Mining big data: current status, and forecast to the future[END_REF][START_REF] Chalmers | Big Data-State of the Art[END_REF][START_REF] Power | Using 'Big Data'for analytics and decision support[END_REF]. To avoid losing data, which could be essential to infer critical information for the decision makers, it is crucial to improve the swiftness of all the analysis' steps [START_REF] Kaisler | Big data: Issues and challenges moving forward[END_REF]. Velocity also refers to how quickly the data is generated [START_REF] Demchenko | Addressing big data issues in scientific data infrastructure[END_REF][START_REF] Bifet | Mining big data: current status, and forecast to the future[END_REF][START_REF] Power | Using 'Big Data'for analytics and decision support[END_REF].

The Veracity. It refers to the reliability, accuracy, consistency and security of data [START_REF] Lukoianova | Veracity roadmap: Is big data objective, truthful and credible?[END_REF][START_REF] Demchenko | Addressing big data issues in scientific data infrastructure[END_REF][START_REF] Gantz | Extracting value from chaos[END_REF]. Lukoianova & Rubin [20] also identify objectivity, truthfulness and credibility as three complementary dimensions of veracity. As an illustration, the Error! Reference source not found. represents four blind monks. If they keep their own data without sharing, they will see elephants as hoses, walls, trees or ropes… Rajaraman & Ullman [START_REF] Rajaraman | Mining of massive datasets[END_REF] go further by assuming that the studied situation changes constantly (as a crisis situation should). The analysis process has then to aggregate heterogeneous data from as many diverse sources as possible (blind men) to generate the most reliable situation model (shape and gesture of the elephant) in real-time (because of the changes).

At last, one of the goals of event processing is to improve and favor the value of the data inside the system. This value generally decreases in proportion to the age, the type, the richness and quantity of the element in the system [START_REF] Kaisler | Big data: Issues and challenges moving forward[END_REF]. The veracity and variety should be considered when computing the value of the data or when analyzing the data [START_REF] Lukoianova | Veracity roadmap: Is big data objective, truthful and credible?[END_REF][START_REF] Kaisler | Big data: Issues and challenges moving forward[END_REF].

To sum up, in order to offer the decision-makers the best common operational picture possible, the three-level IT system will have to process numerous, varied, more or less reliable data, in time, during a crisis situation. This is known as Big Data issues.

How to automatically generate the best situation model possible describing the ongoing collaborative situation, while being on real-time update to match with the innate instability of a crisis, thanks to a three-level IT system that manages all the issues linked to crisis 'Big' data features?

Approaches to Generating Situation Models from Raw Data

According to the descriptions of data features above, a good analysis tool has to access as many events as possible (volume, velocity), from heterogeneous sources (variety). It also has to compute the veracity and value of every data inside the system. If not, the data will be used randomly. Methodologies covering at least one of these points already exist. This section presents two of them.

General Approaches Talking Down at Least One of the 4Vs' Issues

KDD -Fayyad. [START_REF] Fayyad | From data mining to knowledge discovery in databases[END_REF]. The knowledge discovery in structured data base process has been set up to map low-level data, too voluminous to be easily aggregated. The process use patterns to link data together. These patterns have to be validated (veracity) and potentially useful (value). The whole process is made up of five main steps [START_REF] Gantz | Extracting value from chaos[END_REF]:

 Data selection: Focus on a subset, on a sample to improve the performance of the system;  Data preprocessing: Clean data by using pre-defined operations to remove noise, handle missing data, etc.;  Data transformation: Identify useful features to represent data and achieve the users' goals;  Data mining: Match the users' goals to a particular data mining method such as summarization, classification, regression, clustering, etc. Search for patterns by applying the closed method;  Patterns interpretation/evaluation: Interpret mined pattern and resolve potential conflicts thanks to visualizations and the possibility of returning to any previous step. [START_REF] Endsley | Toward a Theory of Situation Awareness in Dynamic Systems[END_REF]. The situation awareness of a system is measured by its ability to perceive elements in a particular environment, to understand them and project them in the future. The whole situation awareness process is therefore made up of three main stages [START_REF] Rajaraman | Mining of massive datasets[END_REF]:

SA -Endsley

 Perception of the elements: Observe and retrieve the status, attributes and dynamics of relevant elements on the field;  Comprehension of the current situation: Gather retrieved elements and infer new elements that convey more and more meanings for the users and their goals;  Projection of future status: Foresee the evolution of the elements' status to project its future dynamic in the environment.

The goal is to provide the knowledge and time (velocity) required by the decisionmakers, in the sight of their objectives (value).

Table 1. Proposition of a particular classification along with some results (x: the V is taken into account by the methodology, -: the V is not considerate inside the methodology)

Name Volume Variety Velocity Veracity Value KDD x - - x x SA x - x - x
These two tools partially cover the data features issues raised earlier. The three-level IT system can therefore combine these two methodologies to support the decision-makers in managing all the issues linked to a Big Data & crisis context.

A New Approach Taking Into Account All the Vs of Big Data

The GéNéPi project includes the Big Data management in the collaboration support system. Events are to be directly analyzed to generate up-to date situation models, in run time. During a crisis, these models will be used by:  Other partners to deduce and orchestrate a collaborative process between the services on the field;  Decision-makers through the generation of a common operational picture in each crisis cell to facilitate the decision-making.

The events treatment system has to take into account all the issues linked to the 'Big Data' features of crisis data. Thanks to the two approaches introduced in section 5.1, three of the five types of issues can be solved, at least to some extent. The five 'operations' of the KDD approach should then be adapted to the three 'time steps' of the SA approach as to the three-level IT system features. Following this assumption, a new methodology has been set up inside the GéNéPi project.

The next subsections describe each step of the new approach illustrated in Error! Reference source not found. and introduced by this paper.

Extract Raw Data from the Crisis Field. As underlined before, decision makers do not lack available data: it is recovered from the field through the reception of numerous events from diverse sources such as:  The services involved (or to be involved) in the crisis response delivering ground truth data thanks to sensors dispatched on the field;  The people taking part in the crisis response and victims of the crisis' effects come along with their smartphone full of sensors and, as the stakeholders, their own perceptions. For instance, Haiti, Japan or China are known for their citizen capability to ask for help or take part in the response through social media in times of crisis [START_REF] Ling | ICT-enabled community empowerment in crisis response: Social media in Thailand flooding 2011[END_REF];  The open data sources accessible through the Internet (objective or not). Only few sources are known from the crisis cells, while all the others are ready to be requested for, if discovered. Hence, to be able to discover new sources, along with their communication protocols, topics of emission and types of emitted events, a 'scan' of the crisis field has to be performed. The challenge is to find the key event sources [START_REF] Kaisler | Big data: Issues and challenges moving forward[END_REF] that is involved in inferring valuable (value) and reliable (veracity) information for the decision-makers on the crisis cells. The volume is also tackled thanks to rules that mainly filter and aggregate data. The goal is to avoid a pathological accumulation of data [START_REF] Kaisler | Big data: Issues and challenges moving forward[END_REF]: the "quantity vs quality" quest. As an output, the filtered and aggregated data is tagged with a use-by date to be defined for each type of event sent by the sources (velocity).

The 'Extract' box refers to the data selection step of the KDD approach and the perception phase of the SA approach.

Unify the Data. The variety issue is solved thanks to a unified approach of interoperability [START_REF] Chen | Architectures for enterprise integration and interoperability: Past, present and future[END_REF]. This approach offers an unlimited access to the unified data from any part of the system and unable the 'Analyze' box to query the unified data set or the MM's instances set, regardless of all the variety issues. This transformation implies: (i) the identification of the type of data contained in the input event; (ii) the availability of a transformation rule concerning this particular type of data. If the rule does not exist in the system, the files' metadata can be used to get around the problem.

The 'Unify' box refers to the data preprocessing step of the KDD approach, adapted to unstructured data set.

Transform Instances. A data can skip the 'Unify' box if is already in the targeted type or if it is already contextualized, and in other words, if it is already an information. In the last case, if it is an instance of a known meta-model MM*, different from the system's meta-model MM, a model transformation has to be set up [START_REF] Wang | An automatic model-to-model mapping and transformation methodology to serve model-based systems engineering[END_REF]. Else, the information is considered as a data. The target meta-model MM, used by the system (cf. level 2 of the three-level IT system), is composed of: (i) a core (see Error! Reference source not found.) that can describe any kind of collaboration; (ii) several layers inheriting from at least one core concept. The situation model, final output of the system, consists of all the instances stocked in the "MM's instances" set (see Error! Reference source not found.). They instantiates concepts form the triplet {Partners, Context, Ob-jectives}:

 The 'Context' describes the surroundings as it appears with or without the crisis.

To adapt the situation model to a particular risk (as flooding or road crisis), sub-parts have been developed around the main context.  The 'Partner' describes the services (resp. people) available for the crisis response, along with their resources, sensors, and capabilities.  The 'Objectives' describes the danger, effects and risks due to crisis events and affecting one part of the context.

As underlined before, the generation of situation model in real-time mainly concerns the 'Objectives' part, because the others are to be prepared in advance, before the crisis.

The 'Transform' box refers to the data transformation step of the KDD approach, adapted to unstructured data set.

Instantiate the Unified Data. The first rules to be applied on the crisis events are business rules. An example from a French crisis management plan can be: 'IF the predicted water level is higher than a 'level1' dike's threshold (which protects big cities from flooding) and IF there is, at least, 48h left before the overrun, THEN the protected city has to be evacuated'. In the GéNéPi project, these rules are directly based on: (i) the French crisis response plans of several defense zones and counties; (ii) the experience

The 'Analyze' box refers to the evaluation step of the KDD approach, and could serve for the projection phase of the SA approach.

The five boxes of the Error! Reference source not found. enable a two-level system to deliver an organized set of information in the form of a situation model. Thanks to it, a common operational picture can be delivered and adapted to the context, objectives and resources of each crisis cells. Inner communications, and therefore decisionmaking, will be reinforced. Moreover, thanks to the GéNéPi project, collaboration processes (third level) will be deduced from this situation model, as orchestrated and maintain all along the crisis response. These two innovations will improve the decisionmakers environment by maintaining the collaboration on the field (horizontal distribution) and by properly sharing information to the other crisis cells (vertical granularity).

Conclusion

Nowadays, more and more data sources produce more and more data each day. This is an opportunity for the crisis decision-makers to improve their own situation awareness. But, to avoid being drowned in data streams, they limit their number of accessible data sources. This situation could lead to data loss, data misjudging and outdated situation awareness. That is the reason why there is a need for data management support in the crisis response field. The solution could be found in existing techniques coming from the industry. Alas, there is a big difference between: (i) known and unknown data sources; (ii) predictable and unpredictable use of data; (iii) finite and infinite number of relevant actions; (iv) minimize and maximize the time spent on the gathering part.

In this context, two approaches have been studied and valued considering the issues linked to crisis data features. The result of this study enables the implementation of a new approach, combining the qualities of both the Endsley's SA and the Fayyad's KDD.

This approach has now to be implemented in: (i) the IO Suite tool [START_REF] Bénaben | A Metamodel for Knowledge Management in Crisis Management[END_REF], enabling the collaboration support during crisis responses in the CGI laboratory of Mines d'Albi and in (ii) the GéNéPi prototype. In addition, more business rules have to be written thanks to the CEREMA partner, along with models transformation rules needed in the 'Transform' box.

In the future, such a tool, enabling the automatic generation of a situation model in real-time, whatever the complexity and instability of the context, will benefit, not only to crisis decision makers, but also to industries willing to quickly adapt in a day-to-day fashion.

Fig. 1 .

 1 Fig. 1. Data, information and knowledge levels to support collaborations during crisis response.

Fig. 2 .

 2 Fig. 2. The blind monks and the elephant [30].

Fig. 3 .

 3 Fig. 3. Data deposition: Five steps to counter the 4vs of Big Data

of the actor that have already been involved in a crisis response; (iii) the doctrines of the services that are to be involved in a crisis response. All this knowledge, answering to 'how to respond to a crisis?', has been recovered from interviews conducted by the CEREMA (Study & expertise center of risks, environment, mobility and development), partner in the GéNéPi project.

The 'Instantiate' box refers to the data mining step of the KDD approach, and to the comprehension phase of the SA approach Analyze the instances. This last step enables the system to deduce information from others thanks to modeling rules. For example, if the danger 'Flooding' has been deduced from the 'Instantiate' box, several risks have to be added on the situation model. Depending on the context, one of the new instances could be a 'risk of victims' linked with a school or a hospital, or a 'risk of pollution' linked with industries. This is possible thanks to the existence of a knowledge base, where all the rules contained in the system apply.

The 'Analyze' phase is also the opportunity to monitor the generation and the projection of the situation model. Here, all the instances of MM and all the unified data are tag with veracity levels and value estimations. These iterations, between unified data and instances, are critical: without them, the system would be amnesic and unable to learn [START_REF] Demchenko | Addressing big data issues in scientific data infrastructure[END_REF]. In this context, the research works of Lukoianova and Rubin [START_REF] Lukoianova | Veracity roadmap: Is big data objective, truthful and credible?[END_REF] can be highlighted as they showed the possibility of measuring deception, subjectivity and credibility of certain data types. The iterations enable the system to:  Improve 'unified data' and 'MM's instances' quality by optimizing their veracity value and value estimation;  Check whether the situation model stocked in the MM's instances box, faithfully represents the crisis field reality;  Put aside all the event sources judged as unreliable ones;  Improve the MM meta-model's coverage by analyzing the veracity and value of unused 'unified data'.