Certifying 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 also briefly presented. Focal is an object-oriented specification and proof system, where we can write programs together with properties which can be proved semi-automatically. We show how Focal is appropriate for building a clean hierarchical specification for our case study using, in particular, the object-oriented features to refine the international level into the European level and parameterization to modularize the development.