基于精化的Stateflow图顺序实现验证
Refinement-based verification of sequential implementations of Stateflow charts
摘要：
Simulink/Stateflow图在工业中广泛用于控制系统的规范，这些控制系统通常是安全关键的。这表明有必要对这种模式进行正式处理。在以前的工作中，我们已经提出了一种技术自动生成的正式模型的Stateflow块，以支持基于细化的推理。在这篇文章中，我们提出了一个细化策略，支持自动生成的顺序C实现的Stateflow图的验证。特别是，我们将讨论如何将这种策略专门化，以利用架构功能，从而实现更高水平的自动化。
英文摘要：
Simulink/Stateflow charts are widely used in industry for the specification of control systems, which are often safety-critical. This suggests a need for a formal treatment of such models. In previous work, we have proposed a technique for automatic generation of formal models of Stateflow blocks to support refinement-based reasoning. In this article, we present a refinement strategy that supports the verification of automatically generated sequential C implementations of Stateflow charts. In particular, we discuss how this strategy can be specialised to take advantage of architectural features in order to allow a higher level of automation.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
