Title :
Reasoning about Airport Security Regulations Using the Focal Environment
Author :
Delahaye, David ; Etienne, J.-F. ; Donzeau-Gouge, Véronique Viguié
Author_Institution :
CEDRIC/CNAM, Paris
Abstract :
We present the validation of regulations intended to ensure airport security in the framework of civil aviation. In particular, we describe the proofs of correctness/completeness for two standards, one at the international level and the other at the European level, and we show how the properties of the European level refines those of the international level. These models are expressed using the Focal environment, an object- oriented specification and proof system, and the proofs described by means of a declarative-like language are processed by the automated theorem prover Zenon. We show how Zenon appears quite appropriate when dealing with abstract specifications like our case study, but also how it should be controlled to present readable proofs.
Keywords :
airports; formal specification; object-oriented methods; security of data; theorem proving; Focal environment; airport security regulation; automated theorem prover Zenon; declarative-like language; object-oriented specification; Airports; Automatic control; Humans; Law; Legal factors; Natural languages; Safety; Security; Standards organizations; Technical drawing;
Conference_Titel :
Leveraging Applications of Formal Methods, Verification and Validation, 2006. ISoLA 2006. Second International Symposium on
Conference_Location :
Paphos
Print_ISBN :
978-0-7695-3071-0
DOI :
10.1109/ISoLA.2006.25