首页> 外文期刊>Reliability Engineering & System Safety >How reliable is satellite navigation for aviation? Checking availability properties with probabilistic verification
【24h】

How reliable is satellite navigation for aviation? Checking availability properties with probabilistic verification

机译:航空卫星导航的可靠性如何?通过概率验证检查可用性属性

获取原文
获取原文并翻译 | 示例
           

摘要

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 pi-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. (C) 2015 Elsevier Ltd. All rights reserved.
机译:本文着重介绍了概率验证分析技术的有希望的应用。我们证明,它有能力并且适合分析基于GNSS的航空部门定位,以进行飞机制导。特别是,重点是一种广泛使用的形式化方法,称为概率模型检查,并将其推广到特定民用航班定量方面的分析。我们为概率pi演算中的此应用程序构建了基于GNSS的定位系统的正式模型,这是一个支持并发,不确定性和移动性建模的过程代数。之后,我们使用PRISM符号概率模型检查器的语言对模型进行编码。然后,我们形式化并分析与基础系统的可靠性相关的逻辑属性,以检查系统的可靠性和可用性。我们演示了如何将模型规范和验证技术成功应用于案例研究的可靠性和可用性分析。 (C)2015 Elsevier Ltd.保留所有权利。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱:kefu@zhangqiaokeyan.com

京公网安备:11010802029741号 ICP备案号:京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有
  • 客服微信

  • 服务号