research-article

An operational semantics for Simulink's simulation engine

Authors:

Olivier Bouissou,

Alexandre ChapoutotAuthors Info & Claims

LCTES '12: Proceedings of the 13th ACM SIGPLAN/SIGBED International Conference on Languages, Compilers, Tools and Theory for Embedded Systems

Pages 129 - 138

https://doi.org/10.1145/2248418.2248437

Published: 12 June 2012 Publication History

Abstract

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.

References

[1]

A. Agrawal, G. Simon, and G. Karsai. Semantic translation of Simulink/Stateflow models to hybrid automata using graph transformations. ENCS, 109:43--56, 2004.

Digital Library

[2]

R. Alur, A. Kanade, S. Ramesh, and K. C. Shashidhar. Symbolic analysis for improving simulation coverage of Simulink/Stateflow models. In EMSOFT, pages 89--98. ACM, 2008.

Digital Library

[3]

J. Bertrane, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, and X. Rival. Static analysis by abstract interpretation of embedded critical software. In UML and Formal Methods. IEEE, 2010.

[4]

P. Caspi, A. Curic, A. Maignan, C. Sofronis, and S. Tripakis. Translating discrete-time Simulink to Lustre. ACM Transaction on Embedded Computing Systems, 4(4):779--818, 2003.

Digital Library

[5]

A. Chapoutot and M. Martel. Abstract Simulation: a static analysis of Simulink models. In ICESS, pages 83--92. IEEE Press, 2009.

Digital Library

[6]

C. Chen, J. Dong, and J. Sun. A formal framework for modeling and validating simulink diagrams. Formal Aspects of Computing, 2009.

[7]

P. Cousot. Integrating physical systems in the static analysis of embedded control software. In APLAS, volume 3780 of LNCS, pages 135--138. Springer, 2005.

Digital Library

[8]

P. Cousot and R. Cousot. Abstract Interpretation Frameworks. Journal of Logic and Computation, 2(4):511--547, 1992.

[9]

B. Denckla and P. Mosterman. Formalizing causal block diagrams for modeling a class of hybrid dynamic systems. In IEEE Conference on Decision and Control, 2005.

[10]

E. Goubault, M. Martel, and S. Putot. Static analysis-based validation of floating-point computations. In Numerical Software with Result Verification, volume 2991 of LNCS, pages 306--313. Springer, 2003.

[11]

E. Hairer, S. Norsett, and G. Wanner. Solving Ordinary Differential Equations I: Nonstiff Problems. Springer-Verlag, 2nd edition, 1993.

Digital Library

[12]

A. Kanade, R. Alur, F. Ivancic, S. Ramesh, S. Sankaranarayanan, and K. C. Shashidhar. Generating and analyzing symbolic traces of Simulink/Stateflow models. In CAV, volume 5643 of LNCS, 2009.

Digital Library

[13]

C. Le Guernic and A. Girard. Zonotope-hyperplane intersection for hybrid systems reachability analysis. In HSCC'08, volume 4981 of LNCS, pages 215--228. Springer, 2008.

Digital Library

[14]

E. A. Lee and H. Zheng. Operational semantics of hybrid systems. In HSCC, number 3414 in LNCS. Springer, 2005.

Digital Library

[15]

G. D. Plotkin. A structural approach to operational semantics. Journal of Logic and Algebraic Programming, 60--61:17--139, 2004.

[16]

L. Shampine and M. Reichelt. The MATLAB ODE Suite. Journal on Sci. Comput., 18(1):1--22, 1997.

Digital Library

[17]

L. Shampine, I. Gladwell, and S. Thompson. Solving ODEs with MATLAB. Cambridge Univ. Press, 2003.

Digital Library

[18]

J. Sifakis. A vision for computer science -- the system perspective. Central European Journal of Computer Science, 1(1):108--116, 2011.

[19]

A. Tiwari. Formal semantics and analysis methods for Simulink Stateflow models. Technical report, SRI Intl., 2002.

[20]

A. Tiwari, N. Shankar, and J. Rushby. Invisible formal methods for embedded control systems. Proceedings of the IEEE, 91(1):29--39, 2003.

[21]

F. Zhang, M. Yeddanapudi, and P. Mosterman. Zero-crossing location and detection algorithms for hybrid system simulation. In 17th IFAC World Congress, pages 7967--7972, 2008.

Cited By

Jesus JSampaio A(2024)Local deadlock analysis of Simulink models based on timed behavioural patterns and theorem provingScience of Computer Programming10.1016/j.scico.2024.103113236:COnline publication date: 1-Sep-2024
https://dl.acm.org/doi/10.1016/j.scico.2024.103113
Jaulin L(2024)Integral algebra for simulating dynamical systems with interval uncertaintiesInternational Journal of Approximate Reasoning10.1016/j.ijar.2024.109353(109353)Online publication date: Dec-2024
https://doi.org/10.1016/j.ijar.2024.109353
Guo SJiang HXu ZLi XRen ZZhou ZChen RRoychoudhury ACadar CKim M(2022)Detecting Simulink compiler bugs via controllable zombie blocks mutationProceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering10.1145/3540250.3549159(1061-1072)Online publication date: 7-Nov-2022
https://dl.acm.org/doi/10.1145/3540250.3549159
Show More Cited By

Index Terms

An operational semantics for Simulink's simulation engine

Recommendations

An operational semantics for Simulink's simulation engine
LCTES '12

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 ...
An operational semantics for ZCCS
ICFEM '97: Proceedings of the 1st International Conference on Formal Engineering Methods

G. Bruns (1995) has proposed a version of value-passing CCS in which an agent language, based on that proposed by Milner, is augmented with a rich data language. The data language can be used to describe sets, tuples and sequences etc. constructed from ...
Trace-Based Abstract Interpretation of Operational Semantics

We present trace-based abstract interpretation, a unification of several lines of research on applying Cousot-Cousot-style abstract interpretation a.i. to operational semantics definitions (such as flowchart, big-step, and small-step semantics) that ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

LCTES '12: Proceedings of the 13th ACM SIGPLAN/SIGBED International Conference on Languages, Compilers, Tools and Theory for Embedded Systems

June 2012

153 pages

ISBN:9781450312127

DOI:10.1145/2248418

General Chair:
Reinhard Wilhelm
Saarland University Saarbrücken
,
Program Chairs:
Heiko Falk
Ulm University
,
Wang Yi
Uppsala University

ACM SIGPLAN Notices Volume 47, Issue 5
LCTES '12
MAY 2012
152 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/2345141
Issue’s Table of Contents

Copyright © 2012 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 12 June 2012

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

LCTES '12

Sponsor:

LCTES '12: SIGPLAN/SIGBED Conference on Languages, Compilers and Tools for Embedded Systems 2012

June 12 - 13, 2012

Beijing, China

Acceptance Rates

Overall Acceptance Rate 116 of 438 submissions, 26%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

48
Total Citations
View Citations
317
Total Downloads

Downloads (Last 12 months)7
Downloads (Last 6 weeks)0

Reflects downloads up to 16 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Jesus JSampaio A(2024)Local deadlock analysis of Simulink models based on timed behavioural patterns and theorem provingScience of Computer Programming10.1016/j.scico.2024.103113236:COnline publication date: 1-Sep-2024
https://dl.acm.org/doi/10.1016/j.scico.2024.103113
Jaulin L(2024)Integral algebra for simulating dynamical systems with interval uncertaintiesInternational Journal of Approximate Reasoning10.1016/j.ijar.2024.109353(109353)Online publication date: Dec-2024
https://doi.org/10.1016/j.ijar.2024.109353
Guo SJiang HXu ZLi XRen ZZhou ZChen RRoychoudhury ACadar CKim M(2022)Detecting Simulink compiler bugs via controllable zombie blocks mutationProceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering10.1145/3540250.3549159(1061-1072)Online publication date: 7-Nov-2022
https://dl.acm.org/doi/10.1145/3540250.3549159
Damers JJaulin LRohou S(2022)Lie symmetries applied to interval integrationAutomatica10.1016/j.automatica.2022.110502144(110502)Online publication date: Oct-2022
https://doi.org/10.1016/j.automatica.2022.110502
Jesus JSampaio A(2022)Compositional Verification of Simulink Block Diagrams Using tock-$$CSP$$ and CSP-ProverFormal Methods: Foundations and Applications10.1007/978-3-031-22476-8_6(91-108)Online publication date: 1-Dec-2022
https://doi.org/10.1007/978-3-031-22476-8_6
Sun QZhang WWang CLiu Z(2022)A Contract-Based Semantics and Refinement for SimulinkDependable Software Engineering. Theories, Tools, and Applications10.1007/978-3-031-21213-0_9(134-148)Online publication date: 11-Dec-2022
https://doi.org/10.1007/978-3-031-21213-0_9
Mancini TMari FMassini AMelatti ITronci E(2021)On checking equivalence of simulation scriptsJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2021.100640120(100640)Online publication date: Apr-2021
https://doi.org/10.1016/j.jlamp.2021.100640
Chowdhury SShrestha SJohnson TCsallner CRothermel GBae D(2020)SLEMIProceedings of the ACM/IEEE 42nd International Conference on Software Engineering10.1145/3377811.3380381(335-346)Online publication date: 27-Jun-2020
https://dl.acm.org/doi/10.1145/3377811.3380381
Bourke TBrun LPouzet M(2019)Mechanized semantics and verified compilation for a dataflow synchronous language with resetProceedings of the ACM on Programming Languages10.1145/33711124:POPL(1-29)Online publication date: 20-Dec-2019
https://dl.acm.org/doi/10.1145/3371112
Naderlinger A(2019)Harnessing Concurrency in Synchronous Block Diagrams to Parallelize Simulation on Multi-Core Hosts2019 Winter Simulation Conference (WSC)10.1109/WSC40007.2019.9004866(702-713)Online publication date: Dec-2019
https://doi.org/10.1109/WSC40007.2019.9004866
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten