文件大小：2M
摘要：机载系统在航空航天领域起着至关重要的作用，其突出的安全性使得软件需求的形式化验证成为一个非常重要的问题.但是随着机载系统需求复杂度和设备数量的增加，其形式化验证中出现了状态空间爆炸的问题.为了缓解该问题，提出了一种机载系统需求的建模与分时组合验证方法.这种方法通过利用时间维度，将复杂的验证系统分解为相互独立的组件，实现了对各组件的独立验证，进而综合出整个系统的验证结果.通过实际的案例研究，证明了该方法的可行性.并通过评估说明该方法不但可以验证一些传统单体验证不能验证的系统，缓解状态空间爆炸，而且可以避免不考虑分时所造成的误报.这一方法为机载系统的软件需求验证提供了一种新的技术途径，有助于提高验证的准确性和效率，确保机载系统的安全性.
文章目录
1 相关工作
1.1 机载系统的需求建模与形式化验证
1.2 需求的组合验证
2 预备知识
2.1 问题图和情景图
2.2 时钟约束规约语言CCSL
3 方法框架
4 方法细节
4.1 需求建模
4.2 验证系统架构生成
4.3 可执行验证模型生成
4.4 不一致性验证与定位
5 案例与评估
5.1 案例研究
5.1.1 设备模型库
5.1.2 需求建模
5.1.3 验证系统结构生成
5.1.4 可执行验证模型生成
5.1.5 动态验证与定位
5.2 方法评估
5.3 讨论
