.png){kind=icon}
返回
Machine-Checked Compositional Specification and Proofs for Embedded Systems
.png){kind=icon}
PRE
AI
DOI：10.1007/978-3-031-98208-8_5.png)
.png){kind=icon}
原文求助.png){kind=icon}
分享.png){kind=icon}
收藏
摘要
En 中文
形式化验证大型异构系统的努力需要与交互组件的数量成线性比例，才能在工业实践中可行。这是通过组合式规范方法和证明系统实现的。在本文中，我们演示如何为一个与工业相关的嵌入式系统（燃油液位显示器）进行可信赖的验证分解。我们首先在HOL4定理证明器中形式化基础理论，并扩展该理论以允许使用度量区间时序逻辑（MITL）进行规范。然后，我们使用MITL为系统声明顶层规范，并将其分解到系统组件。我们的HOL4形式化提供了对先前工作中一种通用规范语言和证明系统的修正和扩展重述，并展示了其对于系统验证分解的实用性。
Keyword:
Compositional proof
formal verification
embedded systems
HOL4
期刊
T
IF:
0
论文数:
17
被引数:
0
.png){kind=icon}
查看更多内容