Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abrial, J.R.: The B Book, Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)
The European Civil Aviation Conference. Regulation (EC) N°2320/2002 of the European Parliament and of the Council of 16 December 2002 establishing Common Rules in the Field of Civil Aviation Security (December 2002)
Dubois, C., Hardin, T., Viguié Donzeau-Gouge, V.: Building Certified Components within Focal. In: Symposium on Trends in Functional Programming (TFP), Munich, Germany, November 2004, vol. 5, pp. 33–48, Intellect (Bristol, UK) (2004)
Jaume, M., Morisset, C.: Formalisation and Implementation of Access Control Models. In: Information Assurance and Security (IAS), International Conference on Information Technology (ITCC), Las Vegas, USA, April 2005, pp. 703–708. IEEE CS Press, Los Alamitos (2005)
Laleau, R., Vignes, S., Ledru, Y., Lemoine, M., Bert, D., Viguié Donzeau-Gouge, V., Peureux, F.: Application of Requirements Engineering Techniques to the Analysis of Civil Aviation Security Standards. In: International Workshop on Situational Requirements Engineering Processes (SREP), in conjunction with the 13th IEEE International Requirements Engineering Conference, Paris, France (August 2005)
Lamport, L.: How to Write a Proof. American Mathematical Monthly 102(7), 600–608 (1995)
The International Civil Aviation Organization. Annex 17 to the Convention on International Civil Aviation, Security - Safeguarding International Civil Aviation against Acts of Unlawful Interference, Amendement 11 (November 2005)
The EDEMOI project (2003), http://www-lsr.imag.fr/EDEMOI/
The SAFEE project (2004), http://www.safee.reading.ac.uk/
The Coq Development Team: Coq, version 8.0. INRIA (January 2006), Available at: http://coq.inria.fr/
The Cristal Team: Objective Caml, version 3.09.1. INRIA (January 2006), Available at: http://caml.inria.fr/
The Focal Development Team: Focal, version 0.3.1. CNAM/INRIA/LIP6 (May 2005), Available at: http://focal.inria.fr/
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Delahaye, D., Étienne, JF., Donzeau-Gouge, V.V. (2006). Certifying Airport Security Regulations Using the Focal Environment. In: Misra, J., Nipkow, T., Sekerinski, E. (eds) FM 2006: Formal Methods. FM 2006. Lecture Notes in Computer Science, vol 4085. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11813040_4
Download citation
DOI: https://doi.org/10.1007/11813040_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-37215-8
Online ISBN: 978-3-540-37216-5
eBook Packages: Computer ScienceComputer Science (R0)