基于传统工程模型的组合形式化分析
Compositional Formal Analysis Based on Conventional Engineering Models
摘要：
状态空间探索的形式化方法已成功应用于评估鲁棒关键软件系统。形式化方法能够发现常规测试可能遗漏的错误条件，并有助于规划复杂的系统操作。然而，形式化方法的广泛应用受到了为实际系统生成形式化规范所需的努力的阻碍。在本文中，我们提出了状态链接接口符合性引擎的数据（SLICED），一种方法，它解决了复杂的正式状态机规范生成，利用传统的工程模型，以获得组成的正式状态模型，并生成正式的断言的状态机。我们演示切片使用虚拟自适应模型发表的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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
