Abstract
Security of civil aviation has become a major concern in recent years, especially due to the increasing number of potential and real threats imposing dynamically changing risks on airport and aircraft security. We propose here a novel computational approach to checking consistency, coherence and completeness of aviation security requirements and provide a framework for systematic analysis of the efficiency and effectiveness of procedural security measures. Our approach deals with the inherent uncertainty of security systems by utilizing advanced computational and probabilistic modeling techniques (namely, Abstract State Machines and Probabilistic Timed Automata) in combination with Probabilistic Model Checking tools.
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)
Altenhofen, M., Börger, E., Lemcke, J.: A High-Level Specification for Mediators (Virtual Providers). In: Bussler, C., Haller, A. (eds.) Proceedings of Business Process Management Workshops, pp. 116–129 (2005)
Börger, E.: The ASM ground model method as a foundation for requirements engineering. J. Verification: Theory and Practice, 145–160 (2003)
Börger, E., Glässer, U., Müller, W.: Formal Definition of an Abstract VHDL’93 Simulator by EA-Machines. In: Kloos, C.D., Breuer, P.T. (eds.) Formal Semantics for VHDL, pp. 107–139. Kluwer Academic Publishers, Dordrecht (1995)
Börger, E., Stärk, R.: Abstract State Machines: A Method for High-Level System Design and Analysis. Springer, Heidelberg (2003)
Brantingham, P.L., Kinney, B., Glässer, U., Singh, K., Vajihollahi, M.: A Computational Model for Simulating Spatial Aspects of Crime in Urban Environments. In: Jamshidi, M. (ed.) Proceedings of 2005 IEEE International Conference on Systems, Man and Cybernetics, pp. 3667–3674. IEEE, Los Alamitos (2005)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2000)
The Economist Airport Screening Technology: Full Exposure. The Economist 389(8491), 21–21 (2006)
Farahbod, R., et al.: The CoreASM Project, http://www.coreasm.org
Farahbod, R., Glässer, U., Vajihollahi, M.: An Abstract Machine Architecture for Web Service Based Business Process Management. The special issue on Business Processes and Services of the International Journal of Business Process Integration and Management (IJBPIM) (to appear, 2006)
The fifth estate, Fasten Your Seatbelts. First aired Nov 9, 2005 on CBC-TV (2006) Last visited November 2006, http://www.cbc.ca/fifth/fastenseatbelts/index.html
Gatersleben, M.R., van der Weij, S.W.: Analysis and Simulation of Passenger Flows in an Airport Terminal. In: Farrington, P.A., Nembhard, H.B., Evans, G.W. (eds.) Proceedings of the 1999 Winter Simulation Conference, pp. 1226–1231 (1999)
Glässer, U., Gotzhein, R., Prinz, A.: The formal semantics of SDL-2000: status and perspectives. J. Comput. Networks 42(3), 343–358 (2003)
Glässer, U., Rastkar, S., Vajihollahi, M.: Computational Modeling and Experimental Validation of Aviation Security Procedures. In: Mehrotra, S., Zeng, D.D., Chen, H., Thuraisingham, B., Wang, F.-Y. (eds.) ISI 2006. LNCS, vol. 3975, pp. 420–432. Springer, Heidelberg (2006)
Glässer, U., Rastkar, S., Vajihollahi, M.: Computational Modeling and Experimental Validation of Aviation Security Procedures. Technical Report SFU-CMPT-TR-2006-23. Simon Fraser University (2006)
Hinton, A., Kwiatkowska, M., Norman, G., Parker, D.: Prism: A tool for automatic verification of probabilistic systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006 and ETAPS 2006. LNCS, vol. 3920, pp. 441–444. Springer, Heidelberg (2006)
International Civil Aviation Organization (ICAO), Annex 17 to the Convention on International Civil Aviation: Standards and Recommended Practices - Security - Safeguarding International Civil Aviation against Acts of Unlawful Interference (2002)
Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic model checking in practice: Case studies with PRISM. J. ACM SIGMETRICS Performance Evaluation Review 32(4), 16–21 (2005)
Kwiatkowska, M., Norman, G., Parker, D., Sproston, J.: Performance analysis of probabilistic timed automata using digital clocks. J. Formal Methods in System Design 29, 33–78 (2006)
Kwiatkowska, M., Norman, G., Segala, R., Sproston, J.: Automatic verification of real-time systems with discrete probability distributions. J. Theoretical Computer Science 282, 101–150 (2002)
Kwiatkowska, M., Norman, G., Sproston, J.: Probabilistic model checking of the IEEE 802.11 wireless local area network protocol. In: Hermanns, H., Segala, R. (eds.) PROBMIV 2002, PAPM-PROBMIV 2002, and PAPM 2002. LNCS, vol. 2399, pp. 169–187. Springer, Heidelberg (2002)
Kwiatkowska, M., Norman, G., Sproston, J.: Probabilistic model checking of deadline properties in the IEEE 1394 FireWire root contention protocol. J. Formal Aspects of Computing 14(3), 295–318 (2003)
Laleau, R., Vignes, S., Ledru, Y., Lemoine, M., Bert, D., Donzeau-Gouge, V., Dubois, C., Peureux, F.: Application of Requirements Analysis Techniques to the Analysis of Civil Aviation Security Standards. In: Ralyté, J., Ågerfalk, P.J., Kraiem, N. (eds.) Proceedings of the First International Workshop on Situational Requirements Engineering Processes (SREP 2005), pp. 91–107 (2006)
Ledru, Y.: Project EDEMOI - An Approach to Model and Validate Airport Security. (Final report) (2006)
Microsoft FSE Group, The Abstract State Machine Language (2003), http://research.microsoft.com/fse/asml/
Pendergraft, D.R., Robertson, C.V., Shrader, S.: Simulation of an Airport Passenger Security System. In: Ingalls, R.G., Rossetti, M.D., Smith, J.S., Peters, B.A. (eds.) Proceedings of the 2004 Winter Simulation Conference, pp. 874–878 (2004)
PRISM Web Site, http://www.cs.bham.ac.uk/~dxp/prism
Rutten, J., Kwiatkowska, M., Norman, G., Parker, D.: Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems. In: Panangaden, P., van Breugel, F. (eds.). CRM Monograph Series, vol. 23. American Mathematical Society (2004)
Stärk, R., Schmid, J., Börger, E.: Java and Java Virtual Machine: Definition, Verification, Validation. Springer, Heidelberg (2001)
Takakuwa, S., Oyama, T.: Simulation Analysis of International-Departure Passenger Flows in an Airport Terminal. In: Chick, S., Sanchez, P.J., Ferrin, D., Morrice, D.J. (eds.) Proceedings of the 2003 Winter Simulation Conference (2003)
The European Parliament and the Council of the European Union, Regulation (EC) No 2320/2002 of the European Parliament and of the Council - Establishing Common Rules in the Field of Civil Aviation Security (2002)
Wilson, D.L.: Use of Modeling and Simulation to Support Airport Security. IEEE Aerospace and Electronic Systems Magazine 20(8), 3–6 (2005)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Glässer, U., Rastkar, S., Vajihollahi, M. (2008). Modeling and Validation of Aviation Security. In: Chen, H., Yang, C.C. (eds) Intelligence and Security Informatics. Studies in Computational Intelligence, vol 135. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-69209-6_18
Download citation
DOI: https://doi.org/10.1007/978-3-540-69209-6_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-69207-2
Online ISBN: 978-3-540-69209-6
eBook Packages: EngineeringEngineering (R0)