How reliable is satellite navigation for aviation? Checking availability properties with probabilistic verification. (December 2015)

• Record Type: Journal Article
• Authors: Lu, Yu; Peng, Zhaoguang; Miller, Alice A.; Zhao, Tingdi; Johnson, Christopher W.
• Is Part Of: Reliability engineering & system safety. Volume 144(2015:Dec.)
• Page Start: 95
• Page End: 116
• Publication Date: 2015-12
• Subjects: Satellite systems -- Formal methods -- Model checking -- Reliability -- Availability -- Probabilistic verification; Reliability (Engineering) -- Periodicals; System safety -- Periodicals; Industrial safety -- Periodicals; Fiabilité -- Périodiques; Sécurité des systèmes -- Périodiques; Sécurité du travail -- Périodiques; 620.00452
• DOI: 10.1016/j.ress.2015.07.020
• Languages: English
• ISSNs: 0951-8320

Abstract

Abstract: This paper highlights a promising application of the analysis technique of probabilistic verification. We prove that it is able and suitable to analyse GNSS based positioning in aviation sectors for aircraft guidance. In particular, the focus is a widely used formal method called probabilistic model checking, and its generalisation to the analysis of quantitative aspects of a specific civil flight. We construct a formal model of the GNSS based positioning system for this application in the probabilistic π -calculus, a process algebra which supports modelling of concurrency, uncertainty, and mobility. After that, we encode our model in language of the PRISM symbolic probabilistic model checker. We then formalise and analyse the logical properties that relate to the dependability of the underlying system to check the system reliability and availability. We demonstrate how model specification and verification techniques can be successfully applied to the reliability and availability analysis of our case study. Abstract : Highlights: We construct a model of a GNSS-based navigation system for aviation with the probabilistic π -calculus. We translate the model into formal language of the PRISM probabilistic model checker. We analyse availability properties specified for the system configurations using PRISM. We examine the results and analyse various impacts on the system׳s availability. Probabilistic verification can be helpful to assist industrial designers of the GNSS.