Modeling Airport Security Regulations in Focal
David Delahaye, Jean-Frédéric Étienne, Véronique Viguié Donzeau-Gouge · 2006
We describe the formal models of two standards related to airport security: 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 speci cation and proof system. We show how Focal is appropriate for building a clean hierarchical speci cation for our case study using, in particular, object-oriented features to re ne the international level into the European level and parameterization to modularize the development.