论文标题
机器检查状态流的可执行语义
Machine-checked executable semantics of Stateflow
论文作者
论文摘要
Simulink是一个广泛使用的嵌入式系统的基于模型的开发环境。状态流是通过层次状态机和流程图建模事件驱动控制的Simulink的组件。但是，状态流缺乏正式的正式语义，因此很难正式证明其模型在安全至关重要的应用中的特性。在本文中，我们为大量状态流量定义了正式的语义，涵盖了复杂的功能，例如层次状态和过渡，事件广播，早期返回，临时操作员等。语义是在伊莎贝尔/hol中形式化的，被证明是确定性的。我们实施了一种自动执行Isabelle语义的策略，以及Python中的翻译器将状态流模型转换为Isabelle中的语法。使用这些工具，我们根据说明我们涵盖的功能的示例集验证语义。
Simulink is a widely used model-based development environment for embedded systems. Stateflow is a component of Simulink for modeling event-driven control via hierarchical state machines and flow charts. However, Stateflow lacks an official formal semantics, making it difficult to formally prove properties of its models in safety-critical applications. In this paper, we define a formal semantics for a large subset of Stateflow, covering complex features such as hierarchical states and transitions, event broadcasts, early return, temporal operators, and so on. The semantics is formalized in Isabelle/HOL and proved to be deterministic. We implement a tactic for automatic execution of the semantics in Isabelle, as well as a translator in Python transforming Stateflow models to the syntax in Isabelle. Using these tools, we validate the semantics against a collection of examples illustrating the features we cover.
