800 Regulations Modelling and their Validation and Verification Validation of Regulation Documents by Automated Analysis of Formal Models? Didier Bert1 , Fabrice Bouquet2 , Yves Ledru1 , and Sylvie Vignes3 1 LSR-IMAG, Grenoble, France 2 LIFC, Besançon, France 3 GET/ENST, Département Informatique et Réseaux, Paris, France Abstract. The security of civil aviation is regulated by a series of inter- national standards and recommended practices. The EDEMOI project aims at investigating different techniques to analyse these standards. In this paper, we address two automated analysis techniques. First state- transition diagrams are extracted to visualize the nominal behavior of the involved actors. Then, models are lightly altered, and test scenarios are generated to determine how security measures could be breaked. Keywords. Civil aviation standards, security, modelling, formal meth- ods, test generation. 1 Introduction The security of civil aviation is regulated by a series of international standards and recommended practices. The main reference is Annex 17 to the Convention on International Civil Aviation [1]. The EDEMOI project [6] aims to provide different techniques to analyse these standards and to develop tools to study the consistency of regulation documents. Standards are written in English and it is not easy to ensure that some parts of the document are not in conflict with other parts or, more commonly, that some cases are not forgotten in particular situations. Moreover, the documents are updated frequently, and it is necessary to verify that the security level of a version is not lowered in the next version. However, it is difficult to automatically validate these documents. So, the approach of the EDEMOI project is to represent regulation documents by several models which are closely related. Among them, formal models are useful to make standards more precise and to analyse them by means of tools issued from software engineering methods. In this paper, we present two complementary automated techniques applied to the formal models. First, we consider state-transition diagrams that can be ex- tracted from the models to visualize the nominal behavior of the involved actors. Then, models are lightly altered, and test scenarios leading to an inconsistent state are generated. They help to determine how erroneous and potentially dan- gerous scenarios can occur. Section 2 gives an overview of the context of the ? This work was done in the EDEMOI project of program “ACI : Sécurité Informa- tique” supported by the French Ministry of Research and New Technologies. REMO2V'06 801 project. Section 3 shows how state-transition diagrams (statecharts) are built. Section 4 indicates how scenarios are generated by using testing techniques. 2 Context of the EDEMOI project The project is dedicated to the investigation of regulation about airport security. The airport is the place where passengers and their baggage are controlled before boarding an aircraft. Preventing dangerous objects from being brought on board an aircraft is a significant step to prevent acts of unlawful interference during a flight. The main general document (Annex 17 [1]) must be followed by all countries that are members of the International Civil Aviation Organization (ICAO). In the litterature, regulation modelling has not attracted much attention from the computer science research community. We have developed a requirement engineering (RE) method by extending or adapting existing RE methods. Indeed, our goal is not the development and production of software: it is to exhibit the security requirements described in the standards in order to specify the whole system and to check that the specification meets these requirements by using formal proofs. A goal-oriented requirements method such as KAOS [5] is the most appropriate. The main goal is the security of the flights. It can be decomposed into several subgoals (with respect to the airport security) such as: no dangerous object is in cabin, no dangerous object is in hold. Again, to prevent dangerous objects for being in cabin, other subgoals must be satisfied: screening of passengers and cabin baggages, no contact between screened passengers and non-screened, and so on. Once these relationships on security properties are established, the process consists in modelling situations and actors of an airport, where the subgoals are brought into play: registration desk, screening check- point, boarding-room, passenger boarding, etc. In all these situations, the model must describe which “events” can occur, and under which conditions the security levels are respected. We have used UML diagrams as the representational schema for our product models (requirements and system models). Although these diagrams do not con- vey all the details of Annex 17, they help in structuring the models and, above all, provide a support for the discussion with certification authorities and for fur- ther validation of the models. The requirement engineering process of EDEMOI has been explained and detailed in [8]. It is pictured in Fig. 1. The second element of modelling relies upon formal models. In the considered part of the project, formal models are written in B [2], a method dedicated to software development of critical software. Formal specifications provide tools to check the consistency of models. They can also be used as a starting point for animating specifications [4], for the generation of state transition diagrams [3] and for a test generation process [9]. As it is recognized, formal methods and their associated mathematical lan- guage are difficult to understand. So, in the EDEMOI approach, graphical and 802 Regulations Modelling and their Validation and Verification Fig. 1. Documents and actors of the modelling process. formal models are built together, and are partially related by tool translation, as, for example, the tool presented in [7]. 3 Building state-transition diagrams A B model is a system defined by a component which contains (i) static decla- rations, as the global sets of baggages, passengers, and the specification of static relations and functions of the domain; (ii) dynamic entities, as the set of flights, passengers currently in the airport, screened passengers, relations between pas- sengers and their flight, baggages of the passengers, etc. They constitute the state of the component; (iii) a sequence of events, which define the behavior of the entities. An event can be executed when its guard is true (a guard is a boolean condition on the state). Security properties are modelled as invariants of the system. For example, the main security property is that there is no dangerous objects in an aircraft, unless these objects are given an explicit authorization. This property is mathematically stated in the model and one can prove that it is preserved by the events. The airport has been modelled following Annex 17. For brevity, we do not detail this model in the paper. The events are: – management of the flights: open boarding, close boarding, – introduction of categories of passengers: new originating passenger, new tran- sit passenger, new transfer passenger – actions of the passengers in the airport: check in registration, passing the scree- ning point, passing the control point, mixing or contact, boarding in cabin. The “GeneSyst” tool [3] can automatically extract a state-transition dia- grams from the formal model. Fig. 2 is an example of such ST diagram. It describes the set of transitions of a passenger called zz from a state where zz enters the airport (first state after initialization), then zz is considered as either REMO2V'06 803 any_aa_event: QInit [G] [ ] new_originating_passenger_aa [G] [ ] check_in_registration_aa [G] [ ] passing_the_screening_point_aa [ ] [G] Init [G] [ ] new_transit_passenger_aa [G] [ ] new_transfer_passenger_aa any_aa_event [G] [ ] passing_the_control_point_aa not(zz ε (originatingPassengers\/transitPassengers\/transferPassengers)) & [G] [ ] mixing_or_contact_aa not(zz ε departurePassengers)) [G] [ ] loading_in_cabin_aa [G] [ ] new_originating_passenger_zz [G] [ ] new_transfer_passenger_zz any_aa_event [G] [ ] check_in_registration_zz [G] [ ] new_transit_passenger_zz [G] [G] passing_the_screening_point_zz [G] [G] passing_the_control_point_zz zz ε originatingPassengers any_aa_event zz ε transitPassengers [G] [G] passing_the_control_point_zz any_aa_event zz ε transferPassengers [G] [G] passing_the_control_point_zz [G] [G] passing_the_control_point_zz [G] [G] passing_the_screening_point_zz [ ] [ ] mixing_or_contact_zz [ ] [ ] loading_in_cabin_zz zz ε departurePassengers any_aa_event Fig. 2. Transition diagram generated by GeneSyst for passenger zz. originating or in transit or in transfer. After that, zz is controlled or screened according to her/his characteristics, and zz becomes a departure passenger, if the checks succeed. Finally, zz is on board (not represented as a state). Each event is split into the cases where the passenger is zz (postfix of event is “ zz”) or not (postfix of event is “ aa”). During the evolution of passenger zz, some events can occur for managing other passengers than zz (factorized as “any aa event”, put for the events in the square box). For this generation, passenger zz (a new fresh variable) is introduced in the system. The resulting diagram is shown in Fig. 2. On the diagram, a transition like [][]event between state1 and state2 , means that event is always enabled in state1 and that it always reaches state2 . A tran- sition like [G][]event means that event is enabled in state1 under some condition and similarly [][G]event means that state2 is reachable from state1 by event un- der some condition. By clicking on the transitions, the GeneSyst tool displays the involved conditions. For the construction of ST diagrams, the states of interest are provided by the user. So, various views of the model can be explored following the entities examined in the states. An application of this generation is to check if the formal model specifies the expected behavior of the actors. If some transitions seem dubious or missing, the user can verify in the formal model and in the initial documents if this fact is due to omissions or inconsistencies, or possibly, to a misunderstanding of the regulation documents. 804 Regulations Modelling and their Validation and Verification The GeneSyst tool can take into account refinement levels. It then produces hierarchical diagrams that represent refinement of data or actions. For instance, one can refine the previous model to distinguish between several kinds of passen- gers, such as ordinary, obliged and armed passengers. The specific events related to these passengers become new transitions inside old states. Another example of action refinement is the decomposition of the screening check-point into several more elementary steps. 4 Generating test scenarios Another useful analysis technique is to determine whether, when and where a given condition is really mandatory to garantee the expected security level. If it is so in the formal model, then the condition must effectively be checked in the real world of the airports. To perform this analysis, each event is transformed in such a way that each conjunct of its “guard” is replaced by its negation (to force the cases where really the condition does not hold). So, an event may produce several modified events. This transformation builds new models that contain a lot of scenarios: e.g. passengers can move without fulfilling all the conditions wrt. the initial model. From these models, the BZ-TT test generation tool [9] is able to automatically generate sequences of events starting from a given state and reaching an expected event where the state is inconsistent. A typical exemple of scenario is to search how (i.e. through which sequence of events) a given originating passenger can enter the cabin of an aircraft without satisfying the security conditions. On the set of all the generated scenarios, only those where a regular behavior can lead to a modified event and then produces an inconsistency, are selected. In that case, the condition which is falsified is really mandatory to avoid the erroneous detected scenario. The usefulness of such a generation is that it is automated and exhaustive. For instance, in a very simple case generation process, we determined that an originating passenger can pass through the control-point instead of the screening- point. For the adequate values of the variables determined by the tool, the se- quence is: open boarding; new originating passenger; check in registration; bad passing the control point where the test which fails is that the passenger must be in transit or in transfer. Another erroneous sequence shows that a transfer passenger can go on board without passsing the control-point, and so on. In each case, it is easy to determine what is the point which fails in the scenario. We expect that we shall be able to detect fine-grain security conditions on more refined models. The tests generation technique needs to be improved and adapted to our goals, but it is already promising. The determination of mandatory conditions REMO2V'06 805 could be a guide to generate check-lists for the control of airports by security inspectors. Indeed, completeness of the check-lists is a concern of the ICAO experts. 5 Conclusion The EDEMOI project is dedicated to modelling regulation documents in or- der to analyze the resulting models by tools issued from software engineering techniques. In this short paper, we have presented the requirements engineering approach adapted to the kind of documents we have to deal with. We have shown two techniques developed in the project, based on the B models. The first one is the generation of state-transition diagrams by the GeneSyst tool. The second one is the generation of faulty scenarios to detect security holes. We believe that these approaches can be useful to validate models, to detect omissions or inconsistencies, to ensure non-regression in case of evolution or modification of the regulation documents, and to provide help for writing security check-lists. References 1. A17. Annex 17 to the Convention on International Civil Aviation - Security - Safe- guarding International Civil Aviation against acts of unlawful interference. ICAO, april 2002. 2. J.-R. Abrial. The B Book - Assigning Programs to Meanings. Cambridge University Press, August 1996. 3. D. Bert, M.-L. Potet, and N. Stouls. GeneSyst: A Tool to Reason about Behavioral Aspects of B Event Specifications. Application to Security Properties. In Proceedings of ZB2005 Conference, LNCS 3455, pages 299–318. Springer-Verlag, 2005. 4. F. Bouquet, B. Legeard, and F. Peureux. A constraint Solver to Animate a B Specification. Int. Journal on Software Tools for Technology Transfer, 6, 2004. 5. A. Dardenne, A. v. Lamsweerde, and S. Fickas. Goal-directed Requirements Acqui- sition. Science of Computer Programming, 20:3–50, 1993. 6. Edemoi. EDEMOI project web site. http://www-lsr.imag.fr/EDEMOI/, 2004. 7. A. Idani, Y. Ledru, and D. Bert. Derivation of UML Class Diagrams as Static Views of Formal B Developments. In Proceedings of the 7th Int. Conference on Formal Engineering Methods (ICFEM’05), LNCS 3785, pages 37–51. Springer-Verlag, 2005. 8. R. Laleau, S. Vignes, Y. Ledru, M. Lemoine, D. Bert, V. Donzeau-Gouge, C. Dubois, and F. Peureux. Application of Requirements Analysis Techniques to the Analysis of Civil Aviation Security Standards. In Proceedings of SREP’05 - 13th IEEE Int. Requirements Engineering Conf., pages 91–106. IEEE, 2005. 9. B. Legeard, F. Peureux, and M. Utting. Automated Boundary Testing from Z and B. In Proceedings of FME’02 - Formal Methods Europe, LNCS 2391, pages 21–40. Springer-Verlag, 2002.