Validation of Regulation Documents by Automated Analysis of Formal Models

The security of civil aviation is regulated by a series of inter- national standards and recommended practices. The EDEMOI project aims at investigating dieren t 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. 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 dieren t 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 conict 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 dicult 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 ecurit e Informa- tique" supported by the French Ministry of Research and New Technologies.