Machine-checked executable semantics of Stateflow

Shicheng Yi, Shuling Wang, Bohua Zhan +1

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 ma…