首页 | 本学科首页   官方微博 | 高级检索  
     


Formal Specification and Quantitative Analysis of a Constellation of Navigation Satellites
Authors:Zhaoguang Peng  Yu Lu  Alice Miller  Tingdi Zhao  Chris Johnson
Affiliation:1. China Ceprei Laboratory, Guangzhou, China;2. School of Reliability and Systems Engineering, Beijing University of Aeronautics and Astronautics, Beijing, China;3. School of Computing Science, University of Glasgow, Glasgow, UK
Abstract:Navigation satellites are a core component of navigation satellite‐based systems such as Global Positioning System, Global Navigation Satellite System and Galileo, which provide location and timing information for a variety of uses. Such satellites are designed for operating on orbit to perform tasks and have lifetimes of 10 years or more. Reliability, availability and maintainability analysis of systems has been indispensable in the design phase of satellites in order to achieve minimum failures or to increase mean time between failures and thus to plan maintenance strategies, optimise reliability and maximise availability. In this paper, we present formal models of both a single satellite and a navigation satellite constellation and logical specification of their reliability, availability and maintainability properties, respectively. The probabilistic model checker PRISM has been used to perform automated analysis of these quantitative properties. Copyright © 2014 John Wiley & Sons, Ltd.
Keywords:navigation satellite systems  reliability  availability  maintainability  probabilistic model checking
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号