Formal Modeling of Airport Security Regulations using the Focal Environment

We present the formalization of regulations intended to ensure airport security in the framework of civil aviation. In particular, we describe the formal models of two standards, one at the international level and the other at the European level. These models are expressed using the Focal environment, which is an object-oriented specification and proof system. In addition, we show that these models are correct and complete thanks to the Zenon automated theorem prover, which is the dedicated reasoning support of Focal. Finally, we propose an automatic transformation of Focal specifications to UML class diagrams, in order to provide a graphical documentation of formal models for developers, and in the long-term, for certification authorities.