Abstract
Matlab Simulink™ is a member of a class of visual languages that are used for modeling and simulating physical and cyber-physical system. A Simulink model consists of blocks with input and output ports connected using links that carry signals. We provide a contract-based type system of Simulink with annotations and dimensions/units associated with ports and links. These contract types can capture invariants on signals as well as relations between signals. We define a contract-based verifier that checks the well formedness of Simulink blocks with respect to these contracts. This verifier generates proof obligations that are solved by SRI’s Yices solver for satisfiability modulo theories (SMT). This translation can be used to detect basic type errors and violation of contracts, demonstrate counterexamples, generate test cases, or prove the absence of contract-based type errors. Our work is an initial step toward the symbolic analysis of Matlab Simulink models.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
Adams MM, Clayton Philip B (2005) ClawZ Cost-effective formal verification for control systems. In: Kung-Kiu L, Richard B (eds) 7th international conference on formal engineering methods, ICFEM, Manchester, UK, 1–4 November, proceedings of lecture notes in computer science, vol 3785. Springer, Manchester, pp 465–479
Aditya K, Rajeev A, Franjo I, Ramesh S, Sriram S, Shashidhar KC (2009) Generating and analyzing symbolic traces of Simulink/Stateflow models. In: 21st CAV, Grenoble, France, June 26–July 2, 2009, LNCS vol 5643. Springer, France, pp 430–445
Bertrand M (1997) Design by contract: making object-oriented programs that work. In: TOOLS 1997: 25th international conference on technology of object-oriented languages and systems, 24–28 November 1997, Melbourne, Australia, vol 25, p 360
Bhatt D, Hickman S, Schloegel K, Oglesby D (2007) An approach and tool for test generation from model-based functional requirements. In: Proceedings of the 1st international workshop on aerospace software engineering, Minneapolis, USA, 21–22. May
Bruno D, de Moura L (2006) A fast linear-arithmetic solver for DPLL(T). In: 18th CAV 2006, Seattle, WA, USA, 17-20 August, Lecture notes in computer science, vol 4144. Springer, Berlin, pp 81–94
Chen C, Dong JS, Sun J 0001 (2009) A formal framework for modeling and validating simulink diagrams. Formal Asp Comput 21(5):451–483
Chutinan A, Krogh B (2003) Computational techniques for hybrid system verification. IEEE Trans Autom Control 48(1): 64–75
de Alfaro L, Henzinger TA (2001) Interface automata. SIGSOFT Softw Eng Notes 26(5): 109–120
de Alfaro L, Henzinger TA (2001) Interface automata. In: Proceedings of the 8th European software engineering conference held jointly with 9th ACM SIGSOFT international symposium on Foundations of software engineering. ESEC/FSE-9, Vienna, Austria. ACM, New York, pp 109–120, ISBN: 1-58113-390-1
Eric A, David C, Victor L, Jan-Willem M, Ryu S, Steele GL Jr, Tobin-Hochstadt S (2005) The Fortress language specification, version 0.618. Technical report, Sun Microsystems, Inc, San Antonio
Fränzle M, Herde C (2007) Hysat: an efficient proof engine for bounded model checking of hybrid systems. Form Methods Syst Des 30(3): 179–198
Hayes IJ, Mahony BP (1995) Using units of measurement in formal specifications. Formal Asp Comput 7(3): 329–347
Kennedy AJ (1996) Programming languages and dimensions. PhD thesis, University of Cambridge, 1996. Published as University of Cambridge Computer Laboratory Technical Report No. 391
Kennedy AJ (1997) Relational parametricity and units of measure. In: The 24th ACM POPL ’97, January 1997, pp 442–455
Man-Kit LJ, Thomas M, Edward LA, Elizabeth L, Charles S, Stavros T, Ben L (2009) Scalable semantic annotation using lattice-based ontologies. In: 12th international conference on model driven engineering languages and systems, October 2009. ACM/IEEE, New York, pp 393–407 (recipient of the MODELS 2009 Distinguished Paper Award)
Michael WW, Cofer DD, Miller SP, Krogh BH, Storm W (2007) Integration of formal analysis into a model-based software development process (2007) In: Stefan L, Pedro M (eds) FMICS, Lecture notes in computer science, vol 4916. Springer, Berlin, pp 68–84
Novak GS (1995) Conversion of units of measurement. IEEE TSE 21(8): 651–661
Owre S, Rushby J, Shankar N, von Henke F (1995) Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Trans Softw Eng 21(2): 107–125
Rajeev A, Aditya K, Ramesh S, Shashidhar KC (2008) Symbolic analysis for improving simulation coverage of Simulink/Stateflow models. In: Proceedings of the 8th ACM & EMSOFT 2008, Atlanta, USA, 19–24 October. ACM, New York, pp 89–98
Reactive Systems. Model based testing and validation with Reactis, Reactive Systems inc., http://www.reactive-systems.com
Rushby J, de Moura L, Hamon G (2004) Generating efficient test sets for Matlab/Stateflow designs. Task 33b report for Cooperative Agreement NCC-1-377 with Honeywell Tucson and NASA Langley Research Center, Computer Science Laboratory, SRI International, Menlo Park, CA, May 2004
Tripakis S, Lickly B, Henzinger T, Edward LA (2009) On relational interfaces. In: Embedded software (EMSOFT’09), October 2009
Tripakis S, Sofronis C, Caspi P, Curic A (2005) Translating discrete-time simulink to Lustre. ACM Trans Embed Comput Syst (TECS) 4(4): 779–818
Open Access
This article is distributed under the terms of the Creative Commons Attribution Noncommercial License which permits any noncommercial use, distribution, and reproduction in any medium, provided the original author(s) and source are credited.
Author information
Authors and Affiliations
Corresponding author
Additional information
This research was supported by NSF Grant CSR-EHCS(CPS)-0834810 and NASA Cooperative Agreement NNX08AY53A.
Rights and permissions
Open Access This is an open access article distributed under the terms of the Creative Commons Attribution Noncommercial License (https://creativecommons.org/licenses/by-nc/2.0), which permits any noncommercial use, distribution, and reproduction in any medium, provided the original author(s) and source are credited.
About this article
Cite this article
Roy, P., Shankar, N. SimCheck: a contract type system for Simulink. Innovations Syst Softw Eng 7, 73–83 (2011). https://doi.org/10.1007/s11334-011-0145-4
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11334-011-0145-4