论文标题
基于常规工程模型的组成形式分析
Compositional Formal Analysis Based on Conventional Engineering Models
论文作者
论文摘要
正式方法用于状态空间探索的应用已成功应用于评估强大的关键软件系统。正式方法可以发现常规测试可能会错过的错误条件，并可以帮助计划复杂的系统操作。但是，正式方法的广泛应用已受到为真实系统制定形式规格所需的努力的阻碍。在本文中，我们介绍了数据链接的数据（切片）的链接接口合规引擎，该方法通过利用传统的工程模型来推导成分正式状态模型并在状态机器上生成正式的主张来解决正式状态机规范生成的复杂性。我们使用NASA发布的虚拟适应模型来证明切片，并通过使用Simulink复制它们来验证我们的结果。
Applications of formal methods for state space exploration have been successfully applied to evaluate robust critical software systems. Formal methods enable discovery of error conditions that conventional testing may miss, and can aid in planning complex system operations. However, broad application of formal methods has been hampered by the effort required to generate formal specifications for real systems. In this paper we present State Linked Interface Compliance Engine for Data (SLICED), a methodology that addresses the complexity of formal state machine specification generation by leveraging conventional engineering models to derive compositional formal state models and to generate formal assertions on the state machines. We demonstrate SLICED using the Virtual ADAPT model published by NASA and validate our results by replicating them using Simulink.
