Abstract
The main cause of major accidents in airport traffic is an incursion of a vehicle into a runway of a landing or taking-off aircraft. This article presents a method to increase the runway safety, where it strongly depends on human made decisions, regulated by national and local laws of deontic nature, i.e. rules of obligation, permission etc. We propose to model and verify such a communication control system, and related behavioral deontic rules, as finite state automata in the Symbolic Model Verifier NuSMV, where the deonticity is built in the automata, and the verification thereof uses CTL temporal logic formulas. The method is simple in modeling the system and in specifying and verifying it. It can also easily find a possible path of states leading to a user-defined hazard.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Cholvy, L., Saurel. C.: Checking compliance of a system with regulations: towards a formalisation. In: Proceedings of ReMoD (2008)
Demasi, R. et al.: Synthesizing masking fault-tolerant systems from deontic specifications. In: Automated Technology for Verification and Analysis. Springer International Publishing (2013)
Shi, K.: Making existing reactive systems anticipatory: methodology and case studies. Doctoral Dissertation, Graduate School of Science and Engineering, Saitama Univ. (2013)
Schönefeld, J., Möller D.: Runway incursion prevention systems: a review of runway incursion avoidance and alerting system approaches. In: PiAS 51 (2012)
Gabillon, A., Laurent, G.: An availability model for avionic databuses. In: Proceedings of the Workshop on Issues in Security and Petri Nets. Eindhoven, Netherlands. vol. 23 (2003)
Han, CH. et al.: Spatio-temporal deontic relevant logic as the logical basis for air traffic control systems. In: Advances in Biomedical Engineering 8 (2012)
Cimatti, A. et al.: NuSMV: a new symbolic model checker. In: International Journal on Software Tools for Technology Transfer 2.4 (2000)
Emerson, E.A.: Temporal and modal logic. In: Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics (B) (1990)
Cavada, R. et al.: NuSMV 2.5 User Manual. FBK-irst, Trento (2011)
Cavada, R. et al.: NuSMV 2.5 Tutorial. FBK-irst, Trento (2011)
Aviation Investigation Report A13O0049. Transportation Safety Board of Canada (2014)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Głuchowski, P. (2016). NuSMV Model Verification of an Airport Traffic Control System with Deontic Rules. In: Zamojski, W., Mazurkiewicz, J., Sugier, J., Walkowiak, T., Kacprzyk, J. (eds) Dependability Engineering and Complex Systems. DepCoS-RELCOMEX 2016. Advances in Intelligent Systems and Computing, vol 470. Springer, Cham. https://doi.org/10.1007/978-3-319-39639-2_17
Download citation
DOI: https://doi.org/10.1007/978-3-319-39639-2_17
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-39638-5
Online ISBN: 978-3-319-39639-2
eBook Packages: EngineeringEngineering (R0)