Title :
Availability Analysis of Satellite Positioning Systems for Aviation Using the PRISM Model Checker
Author :
Yu Lu ; Miller, Alice ; Johnson, Chris ; Zhaoguang Peng ; Tingdi Zhao
Author_Institution :
Sch. of Comput. Sci., Univ. of Glasgow, Glasgow, UK
Abstract :
This paper highlights an application of probabilistic model checking to satellite positioning systems for aircraft guidance. After introducing our formal approach based on using the PRISM model checker, we built a model of a global navigation satellite system (GNSS) based positioning system for a specific flight in the probabilistic π-calculus, a process algebra which supports modelling of concurrency, uncertainty, and mobility. After that, we encode our model into the PRISM language. We then analyse the availability properties that relate to the dependability and overall performance of the underlying system. The aim of our research is to use PRISM to assist industrial designers and developers of the GNSS.
Keywords :
aerospace computing; artificial satellites; formal verification; pi calculus; GNSS based positioning system; PRISM language; PRISM model checker; availability property; aviation; concurrency modeling; global navigation satellite system; mobility modeling; probabilistic π-calculus; probabilistic model checking; process algebra; satellite positioning system; uncertainty modeling; Analytical models; Atmospheric modeling; Global Positioning System; Monitoring; Probabilistic logic; Satellites; GNSS; availability analysis; aviation; probabilistic model checking; satellite positioning;
Conference_Titel :
Computational Science and Engineering (CSE), 2014 IEEE 17th International Conference on
Conference_Location :
Chengdu
Print_ISBN :
978-1-4799-7980-6
DOI :
10.1109/CSE.2014.148
