Machine-checked executable semantics of Stateflow

TL;DR

This paper provides a formal, machine-checked semantics for a significant subset of Stateflow, enabling formal verification of models in safety-critical systems using Isabelle/HOL.

Contribution

It introduces a formal semantics for Stateflow, implemented in Isabelle/HOL, including tools for automatic execution and model translation.

Findings

Semantics covers complex Stateflow features like hierarchical states and temporal operators.

The semantics is proven deterministic in Isabelle/HOL.

Tools validate the semantics against various Stateflow examples.

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.