research-article

Open access

A formal framework for modeling and validating Simulink diagrams

Authors:

Jun SunAuthors Info & Claims

Formal Aspects of Computing, Volume 21, Issue 5

Pages 451 - 483

https://doi.org/10.1007/s00165-009-0108-9

Published: 01 October 2009 Publication History

Abstract

Simulink has been widely used in industry to model and simulate embedded systems. With the increasing usage of embedded systems in real-time safety-critical situations, Simulink becomes deficient to analyze (timing) requirements with high-level assurance. In this article, we apply Timed Interval Calculus (TIC), a real-time specification language, to complement Simulink with TIC formal verification capability. We elaborately construct TIC library functions to model Simulink library blocks which are used to compose Simulink diagrams. Next, Simulink diagrams are automatically transformed into TIC models which preserve functional and timing aspects. Important requirements such as timing bounded liveness can be precisely specified in TIC for whole diagrams or some components. Lastly, validation of TIC models can be rigorously conducted with a high degree of automation using a generic theorem prover. Our framework can enlarge the design space by representing environment properties to open systems, and handle complex diagrams as the analysis of continuous and discrete behavior is supported.

References

References

[1]

Adams MM, Clayton PB (2005) ClawZ: cost-effective formal verification for control systems. In: Proceedings of the 7th international conference on formal engineering methods. Springer, Heidelberg, pp 465–479

[2]

Arthan R, Caseley P, O’Halloran C, Smith A (2000) Clawz: control laws in Z. In: Proceedings of the 3rd international conference on formal engineering methods. IEEE Computer Society, Washington, pp 169–176

[3]

Butler RW (2004) Formalization of the integral calculus in the PVS theorem prover. Technical report, NASA Langley Research Center, Hampton, Virginia

[4]

Cavalcanti A, Clayton P, O’Halloran C (2005) Control law diagrams in Circus. In: Proceedings of the 13th international symposium of formal methods europe. Springer, Heidelberg, pp 253–268

[5]

Chen C, Dong JS (2006) Applying timed interval calculus to simulink diagrams. In: Proceedings of the 8th international conference on formal engineering methods. Springer, Heidelberg, pp 74–93

[6]

Chen C, Dong JS, Sun J (2007) A formal framework for modeling and verifying simulink diagrams. http://www.comp.nus.edu.sg/~chenchun/SimInTIC

[7]

Chen C, Dong JS, Sun J (2007) Machine-assisted proof support for validation beyond Simulink. In: Proceedings of the 9th international conference on formal engineering methods. Springer, Heidelberg, pp 96–115

[8]

Chen C, Dong JS, Sun J (2008) A verification system for timed interval calculus. In: Proceedings of the 30th international conference on software engineering. ACM, New York, pp 271–280

[9]

Cavalcanti A, Sampaio A, and Woodcock J A refinement strategy for Circus Formal Asp Comput 2003 15 2–3 146-181

Digital Library

[10]

Fidge CJ, Hayes IJ, Mahony BP (1998) Defining differentiation and integration in Z. In: Proceedings of the 2nd international conference on formal engineering methods. IEEE Computer Society, Washington, pp 64–73

[11]

Fidge CJ, Hayes IJ, Martin AP, Wabenhorst A (1998) A set-theoretic model for real-time specification and reasoning. In: Proceedings of the mathematics of program construction. Springer, Heidelberg, pp 188–206

[12]

Gupta S, Krogh BH, Rutenbar RA (2004) Towards formal verification of analog designs. In: proceedings of the international conference on computer-aided design. IEEE Computer Science, Washington, pp 210–217

[13]

Henzinger TA, Sifakis J (2006) The embedded systems design challenge. In Proceedings of the 14th international symposium on formal methods. Springer, Heidelberg, pp 1–15

[14]

Jersak M, Cai Y, Ziegenbein D, Ernst R (2000) A transformational approach to constraint relaxation of a time-driven simulation model. In: Proceedings of the 13th international symposium on System synthesis. IEEE Computer Society, Washington, pp 137–142

[15]

Jantsch A and Sander I Models of computation and languages for embedded system design IEE Proc Comput Digit Tech 2005 152 2 114-129

[16]

Kowalewski S, Stursberg O, Fritz M, Graf H, Hoffmann I, Preußig J, Remelhe M, Simon S, Treseler H (1999) A case study in tool-aided analysis of discretely controlled continuous systems: The two tanks problem. In: Hybrid systems V. Springer, Heidelberg, pp~163–185

[17]

Liu Y, Sun J, Dong JS (2008) An analyzer for extended compositional process algebras. In: Companion of the 30th international conference on software engineering. ACM, New York, pp 919–920

[18]

Meenakshi B, Bhatnagar A, Roy S (2006) Tool for translating simulink models into input language of a model checker. In: Proceedings of the 8th international conference on formal engineering methods. Springer, Heidelberg, pp 606–620

[19]

Muñoz C, Carreño V, Dowek G, and Butler RW Formal verification of conflict detection algorithms Int J Softw Tools Technol Transf 2003 4 3 371-380

[20]

Mahony BP, Dong JS (1998) Blending object-Z and timed CSP: an introduction to TCOZ. In: Proceedings of the 20th international conference on software engineering. IEEE Computer Society, Washington, pp 95–104

[21]

Mahony BP and Dong JS Timed communicating object Z IEEE Trans Softw Eng 2000 26 2 150-177

Digital Library

[22]

Mahony BP and Hayes IJ A case-study in timed refinement: a mine pump IEEE Trans Softw Eng 1992 18 9 817-826

Digital Library

[23]

Owre S, Rushby JM, Shankar N (1992) PVS: a prototype verification system. In: Proceedings of the 11th international conference on automated deduction. Springer, Heidelberg, pp 748–752

[24]

Pnueli A (2002) Embedded systems: challenges in specification and verification. In: Proceedings of the 2nd international conference on embedded software. Springer, Heidelberg, pp 1–14

[25]

Sims S, Cleaveland R, Butts K, Ranville S (2001) Automated validation of software models. In: Proceedings of the 16th international conference on automated software engineering. IEEE Computer Society, Washington, pp 91–96

[26]

Sun J, Liu Y, Dong JS, Wang HH (2008) Specifying and verifying event-based fairness enhanced systems. In: Proceedings of the 10th international conference on formal engineering methods. Springer, Heidelberg, pp 5–24

[27]

Tripakis S, Sofronis C, Caspi P, and Curic A Translating discrete-time Simulink to Lustre Trans Embed Comput Syst 2005 4 4 779-818

Digital Library

[28]

The MathWorks. Simulink^® 7—reference, March 2008

[29]

The MathWorks. Simulink^® 7—using Simulink, March 2008

[30]

Tiwari A, Shankar N, and Rushby JM Invisible formal methods for embedded control systems Proc IEEE 2003 91 1 29-39

[31]

Wang F Formal verification of timed systems: a survey and perspective Proc IEEE 2004 92 8 1283-1305

[32]

Woodcock J and Davies J Using Z: specification, refinement and proof 1996 Englewood Cliffs Prentice-Hall

[33]

Zhou C, Hoare CAR, and Ravn AP A calculus of durations Inf Proc Lett 1991 40 5 269-276

[34]

Zhou C, Li X (1994) A mean value calculus of durations. In: A classical mind: essays in honour of C. A. R. Hoare. Prentice-Hall International, Englewood Cliffs, pp 431–451

[35]

Zhou C, Ravn AP, Hansen MR (1993) An extended duration calculus for hybrid real-time systems. In: Hybrid systems. Springer, Heidelberg, pp 36–59

Cited By

Sun QZhang WWang CLiu Z(2023)A contract-based semantics and refinement for hybrid Simulink block diagramsJournal of Systems Architecture10.1016/j.sysarc.2023.102963143(102963)Online publication date: Oct-2023
https://doi.org/10.1016/j.sysarc.2023.102963
Zhang WSun QWang CLiu Z(2023)Towards correctness proof for hybrid Simulink block diagramsJournal of Systems Architecture: the EUROMICRO Journal10.1016/j.sysarc.2023.102922141:COnline publication date: 1-Aug-2023
https://dl.acm.org/doi/10.1016/j.sysarc.2023.102922
Zhang WSun QWang CLiu Z(2022)Proving Simulink Block Diagrams Correct via RefinementWireless Communications & Mobile Computing10.1155/2022/80158962022Online publication date: 1-Jan-2022
https://dl.acm.org/doi/10.1155/2022/8015896
Show More Cited By

Index Terms

A formal framework for modeling and validating Simulink diagrams

Index terms have been assigned to the content through auto-classification.

Recommendations

Applying timed interval calculus to simulink diagrams
ICFEM'06: Proceedings of the 8th international conference on Formal Methods and Software Engineering

Simulink has been used widely as an industry tool to model and simulate embedded systems. With increasing usage of embedded systems in real-time safety-critical situations, Simulink is deficient to cope with the requirements of high-level assurance and ...
Stateflow Diagrams in Circus

The Matlab Simulink tool is widely used to construct and analyse control law diagrams. Many have worked on techniques to enhance analysis facilities, and previously, we have considered the complementary problem of proving correctness of implementations ...
A UML Model to Simulink Model Transformation Method in the Design of Embedded Software
CIS '14: Proceedings of the 2014 Tenth International Conference on Computational Intelligence and Security

Model Driven Development is becoming the trend of embedded software development, UML and Simulink are very important modeling languages. However, UML is a semi-formal modeling language, lacking of accurate semantics, which can't validate correctness of ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Formal Aspects of Computing

Formal Aspects of Computing Volume 21, Issue 5

Oct 2009

115 pages

ISSN:0934-5043

EISSN:1433-299X

Issue’s Table of Contents

© British Computer Society 2009.

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 October 2009

Accepted: 31 December 2008

Received: 09 January 2008

Published in FAC Volume 21, Issue 5

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

32
Total Citations
View Citations
92
Total Downloads

Downloads (Last 12 months)60
Downloads (Last 6 weeks)9

Reflects downloads up to 16 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Sun QZhang WWang CLiu Z(2023)A contract-based semantics and refinement for hybrid Simulink block diagramsJournal of Systems Architecture10.1016/j.sysarc.2023.102963143(102963)Online publication date: Oct-2023
https://doi.org/10.1016/j.sysarc.2023.102963
Zhang WSun QWang CLiu Z(2023)Towards correctness proof for hybrid Simulink block diagramsJournal of Systems Architecture: the EUROMICRO Journal10.1016/j.sysarc.2023.102922141:COnline publication date: 1-Aug-2023
https://dl.acm.org/doi/10.1016/j.sysarc.2023.102922
Zhang WSun QWang CLiu Z(2022)Proving Simulink Block Diagrams Correct via RefinementWireless Communications & Mobile Computing10.1155/2022/80158962022Online publication date: 1-Jan-2022
https://dl.acm.org/doi/10.1155/2022/8015896
Preoteasa VDragomir ITripakis S(2022)The refinement calculus of reactive systemsInformation and Computation10.1016/j.ic.2021.104819285:PBOnline publication date: 1-May-2022
https://dl.acm.org/doi/10.1016/j.ic.2021.104819
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: 24-Oct-2022
https://dl.acm.org/doi/10.1007/978-3-031-21213-0_9
Gauhar ARashid AHasan OBispo JCardoso J(2021)Formal verification of Matrix based MATLAB models using interactive theorem provingPeerJ Computer Science10.7717/peerj-cs.4407(e440)Online publication date: 22-Mar-2021
https://doi.org/10.7717/peerj-cs.440
Rashid AGauhar AHasan O(2020)FASiM: A Framework for Automatic Formal Analysis of Simulink Models of Linear Analog Circuits2020 IEEE International Systems Conference (SysCon)10.1109/SysCon47679.2020.9353652(1-7)Online publication date: 24-Aug-2020
https://doi.org/10.1109/SysCon47679.2020.9353652
Viet Nguyen LMohan GWeimer JSokolsky OLee IAlur R(2020)REAFFIRM: Model-Based Repair of Hybrid Systems for Improving Resiliency2020 18th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE)10.1109/MEMOCODE51338.2020.9315153(1-12)Online publication date: 2-Dec-2020
https://doi.org/10.1109/MEMOCODE51338.2020.9315153
Dragomir IPreoteasa VTripakis S(2020)The Refinement Calculus of Reactive Systems ToolsetInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-020-00561-422:6(689-708)Online publication date: 1-Dec-2020
https://dl.acm.org/doi/10.1007/s10009-020-00561-4
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
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

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 Article

Figures

Tables

Media

View Issue’s Table of Contents