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

fYear

2014

fDate

19-21 Dec. 2014

Firstpage

704

Lastpage

713

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Computational Science and Engineering (CSE), 2014 IEEE 17th International Conference on

Conference_Location

Chengdu

Print_ISBN

978-1-4799-7980-6

Type

conf

DOI

10.1109/CSE.2014.148

Filename

7023658