Availability analysis of satellite positioning systems for aviation using the PRISM model checker

Yu Lu, Alice Miller, Chris Johnson, Zhaoguang Peng, Tingdi Zhao

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

7 Citations (Scopus)

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.

Original languageEnglish
Title of host publicationProceedings - 17th IEEE International Conference on Computational Science and Engineering, CSE 2014, Jointly with 13th IEEE International Conference on Ubiquitous Computing and Communications, IUCC 2014, 13th International Symposium on Pervasive Systems, Algorithms, and Networks, I-SPAN 2014 and 8th International Conference on Frontier of Computer Science and Technology, FCST 2014
EditorsXingang Liu, Didier El Baz, Ching-Hsien Hsu, Kai Kang, Weifeng Chen
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages704-713
Number of pages10
ISBN (Electronic)9781479979813
DOIs
Publication statusPublished - 26 Jan 2015
Externally publishedYes
Event17th IEEE International Conference on Computational Science and Engineering, CSE 2014 - Jointly with 13th IEEE International Conference on Ubiquitous Computing and Communications, IUCC 2014, 13th International Symposium on Pervasive Systems, Algorithms, and Networks, I-SPAN 2014 and 8th International Conference on Frontier of Computer Science and Technology, FCST 2014 - Chengdu, China
Duration: 19 Dec 201421 Dec 2014

Publication series

NameProceedings - 17th IEEE International Conference on Computational Science and Engineering, CSE 2014, Jointly with 13th IEEE International Conference on Ubiquitous Computing and Communications, IUCC 2014, 13th International Symposium on Pervasive Systems, Algorithms, and Networks, I-SPAN 2014 and 8th International Conference on Frontier of Computer Science and Technology, FCST 2014

Conference

Conference17th IEEE International Conference on Computational Science and Engineering, CSE 2014 - Jointly with 13th IEEE International Conference on Ubiquitous Computing and Communications, IUCC 2014, 13th International Symposium on Pervasive Systems, Algorithms, and Networks, I-SPAN 2014 and 8th International Conference on Frontier of Computer Science and Technology, FCST 2014
Country/TerritoryChina
CityChengdu
Period19/12/1421/12/14

Fingerprint

Dive into the research topics of 'Availability analysis of satellite positioning systems for aviation using the PRISM model checker'. Together they form a unique fingerprint.

Cite this