An operational semantics for Simulink's simulation engine - Archive ouverte HAL Access content directly
Conference Papers Year : 2012

An operational semantics for Simulink's simulation engine

(1) , (2)


The industrial tool Matlab/Simulink is widely used in the design of embedded systems. The main feature of this tool is its ability to model in a common formalism the software and its physical environment. This makes it very useful for validating the design of embedded software using numerical simulation. However, the formal verification of such models is still problematic as Simulink is a programming language for which no formal semantics exists. In this article, we present an operational semantics of a representative subset of Simulink which includes both continuous-time and discrete-time blocks. We believe that this work gives a better understanding of Simulink and it defines the foundations of a general framework to apply formal methods on Simulink's high level descriptions of embedded systems.
Not file

Dates and versions

hal-00819373 , version 1 (30-04-2013)



Olivier Bouissou, Alexandre Chapoutot. An operational semantics for Simulink's simulation engine. 13th ACM SIGPLAN/SIGBED International Conference on Languages, Compilers, Tools and Theory for Embedded Systems, Jun 2012, Pekin, China. pp.129-138, ⟨10.1145/2248418.2248437⟩. ⟨hal-00819373⟩
128 View
0 Download



Gmail Facebook Twitter LinkedIn More