Machine-checked executable semantics of Stateflow
Abstract
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.
Cite
@article{arxiv.2207.11965,
title = {Machine-checked executable semantics of Stateflow},
author = {Shicheng Yi and Shuling Wang and Bohua Zhan and Naijun Zhan},
journal= {arXiv preprint arXiv:2207.11965},
year = {2022}
}
Comments
26 pages