The security of civil aviation is regulated by a series of international standards and recommended practices. The EDEMOI project aims at investigating di erent techniques to analyse these standards. In this paper, we address two automated analysis techniques. First statetransition 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.
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 [
However, it is di cult 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 extracted 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 dangerous scenarios can occur. Section 2 gives an overview of the context of the ? This work was done in the EDEMOI project of program \ACI : Securite Informatique" supported by the French Ministry of Research and New Technologies. project. Section 3 shows how state-transition diagrams (statecharts) are built. Section 4 indicates how scenarios are generated by using testing techniques. 2
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 signi cant step to prevent acts of unlawful interference during
a ight. The main general document (Annex 17 [
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 speci cation meets these requirements by
using formal proofs. A goal-oriented requirements method such as KAOS [
We have used UML diagrams as the representational schema for our product
models (requirements and system models). Although these diagrams do not
convey all the details of Annex 17, they help in structuring the models and, above
all, provide a support for the discussion with certi cation authorities and for
further validation of the models. The requirement engineering process of EDEMOI
has been explained and detailed in [
The second element of modelling relies upon formal models. In the considered
part of the project, formal models are written in B [
As it is recognized, formal methods and their associated mathematical
language are di cult to understand. So, in the EDEMOI approach, graphical and
formal models are built together, and are partially related by tool translation,
as, for example, the tool presented in [
A B model is a system de ned by a component which contains (i) static declarations, as the global sets of baggages, passengers, and the speci cation of static relations and functions of the domain; (ii) dynamic entities, as the set of ights, passengers currently in the airport, screened passengers, relations between passengers and their ight, baggages of the passengers, etc. They constitute the state of the component; (iii) a sequence of events, which de ne 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 ights: open boarding, close boarding, { introduction of categories of passengers: new originating passenger, new transit passenger, new transfer passenger { actions of the passengers in the airport: check in registration, passing the screening point, passing the control point, mixing or contact, boarding in cabin.
The \GeneSyst" tool [
[G] [G] passing_the_control_point_zz zze transferPassengers any_aa_event any_aa_event: [G] [ ] new_originating_passenger_aa [G] [ ] check_in_registration_aa [G] [ ] passing_the_screening_point_aa [G] [ ] new_transit_passenger_aa [G] [ ] new_transfer_passenger_aa [G] [ ] passing_the_control_point_aa [G] [ ] mixing_or_contact_aa [G] [ ] loading_in_cabin_aa any_aa_event [G] [ ] check_in_registration_zz [G] [G] passing_the_screening_point_zz
zz eoriginatingPassengers [G] [G] passing_the_screening_point_zz [ ] [ ] mixing_or_contact_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 (post x of event is \ zz") or not (post x 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 transition 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 under 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 speci es 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.
The GeneSyst tool can take into account re nement levels. It then produces hierarchical diagrams that represent re nement of data or actions. For instance, one can re ne the previous model to distinguish between several kinds of passengers, such as ordinary, obliged and armed passengers. The speci c events related to these passengers become new transitions inside old states. Another example of action re nement is the decomposition of the screening check-point into several more elementary steps. 4
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 e ectively 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 modi ed
events. This transformation builds new models that contain a lot of scenarios: e.g.
passengers can move without ful lling all the conditions wrt. the initial model.
From these models, the BZ-TT test generation tool [
For instance, in a very simple case generation process, we determined that an originating passenger can pass through the control-point instead of the screeningpoint. For the adequate values of the variables determined by the tool, the sequence 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 ne-grain security conditions on more re ned models.
The tests generation technique needs to be improved and adapted to our goals, but it is already promising. The determination of mandatory conditions 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
The EDEMOI project is dedicated to modelling regulation documents in order 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 rst 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 modi cation of the regulation documents, and to provide help for writing security check-lists.