...
  • 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Computer science review >Linear Temporal Logic Symbolic Model Checking
【24h】

Linear Temporal Logic Symbolic Model Checking

机译：线性时间逻辑符号模型检查

获取原文
获取原文并翻译 | 示例
           
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

We are seeing an increased push in the use of formal verification techniques in safety-critical software and hardware in practice. Formal verification has been successfully used to verify systems such as air traffic control, airplane separation assurance, autopilot, CPU designs, life-support systems, medical equipment (such as devices which administer radiation), and many other systems which ensure human safety. This survey provides a perspective on the formal verification technique of linear temporal logic (LTL) symbolic model checking, from its history and evolution leading up to the state-of-the-art. We unify research from 1977 to 2009, providing a complete end-to-end analysis embracing a users' perspective by applying each step to a real-life aerospace example. We include an in-depth examination of the algorithms underlying the symbolic model-checking procedure, show proofs of important theorems, and point to directions of ongoing research. The primary focus is on model checking using LTL specifications, though other approaches are briefly discussed and compared to using LTL.
机译：在实践中，我们看到在安全关键型软件和硬件中使用形式验证技术的呼声越来越高。正式验证已成功用于验证系统，例如空中交通管制，飞机分离保证，自动驾驶，CPU设计，生命支持系统，医疗设备（例如管理辐射的设备）以及许多其他确保人身安全的系统。这项调查提供了从线性时间逻辑（LTL）符号模型检查的形式验证技术的角度，从其历史和演变直至最新技术。我们将1977年至2009年的研究统一起来，通过将每个步骤应用于现实生活中的航空航天示例，从而提供了包含用户观点的完整的端到端分析。我们对符号模型检查程序的基础算法进行了深入研究，展示了重要定理的证明，并指出了正在进行的研究方向。主要重点是使用LTL规范进行模型检查，尽管简要讨论了其他方法并将其与使用LTL进行比较。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号