Abstract
Simulink is a widely used tool for modelling, simulating, and analyzing cyber-physical systems using block diagrams. Such diagrams contain both discrete-time and continuous-time blocks. To analyze complex block diagrams, a semantics to support compositional reasoning and verification is required. Contract-based modelling provides good compositional reasoning about complex systems. In this paper, we present a contract-based semantic model for Simulink to formalise the semantics of both discrete-time and continuous-time blocks. In our semantic formalisation, the semantics of a block is defined as a contract, and we define five operations on contracts, which are sequential composition, parallel composition, feedback composition, variable renaming, and variable hiding. We then define the refinement relation among the Simulink diagrams.
This work was funded in part by the Chongqing Graduate Research and Innovation Project (grant No. CYB20098), the National Natural Science Foundation of China (No. 62032019, 61732019, 61672435, 62002298), and the Capacity Development Grant of Southwest University (SWU116007).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Benveniste, A., et al.: Contracts for system design (2018)
Boström, P.: Contract-based verification of Simulink models. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol. 6991, pp. 291–306. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-24559-6_21
Boström, P., Morel, L., Waldén, M.: Stepwise development of Simulink models using the refinement calculus framework. In: Jones, C.B., Liu, Z., Woodcock, J. (eds.) ICTAC 2007. LNCS, vol. 4711, pp. 79–93. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-75292-9_6
Boström, P., Wiik, J.: Contract-based verification of discrete-time multi-rate Simulink models. Softw. Syst. Model. 15(4), 1141–1161 (2016)
Bouissou, O., Chapoutot, A.: An operational semantics for Simulink’s simulation engine. In: Wilhelm, R., Falk, H., Yi, W. (eds.) SIGPLAN/SIGBED Conference on Languages, Compilers and Tools for Embedded Systems 2012, LCTES 2012, Beijing, China, 12–13 June 2012, pp. 129–138. ACM (2012)
Bourke, T., Carcenac, F., Colaço, J., Pagano, B., Pasteur, C., Pouzet, M.: A synchronous look at the Simulink standard library. ACM Trans. Embed. Comput. Syst. 16(5s), 176:1–176:24 (2017)
Caspi, P., Curic, A., Maignan, A., Sofronis, C., Tripakis, S.: Translating discrete-time Simulink to Lustre. In: Alur, R., Lee, I. (eds.) EMSOFT 2003. LNCS, vol. 2855, pp. 84–99. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-45212-6_7
Cavalcanti, A., Clayton, P., O’Halloran, C.: Control law diagrams in Circus. In: Fitzgerald, J., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582, pp. 253–268. Springer, Heidelberg (2005). https://doi.org/10.1007/11526841_18
Cavalcanti, A., Mota, A., Woodcock, J.: Simulink timed models for program verification. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) Theories of Programming and Formal Methods. LNCS, vol. 8051, pp. 82–99. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39698-4_6
Chapoutot, A., Martel, M.: Abstract simulation: a static analysis of Simulink models. In: Chen, T., Serpanos, D.N., Taha, W. (eds.) International Conference on Embedded Software and Systems, ICESS 2009, Hangzhou, Zhejiang, P.R. China, 25–27 May 2009, pp. 83–92. IEEE Computer Society (2009)
Chen, C., Dong, J.S.: Applying timed interval calculus to Simulink diagrams. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 74–93. Springer, Heidelberg (2006). https://doi.org/10.1007/11901433_5
Chen, C., Dong, J.S., Sun, J.: A formal framework for modeling and validating Simulink diagrams. Formal Aspects Comput. 21(5), 451–483 (2009)
Dragomir, I., Preoteasa, V., Tripakis, S.: Compositional semantics and analysis of hierarchical block diagrams. In: Bošnački, D., Wijs, A. (eds.) SPIN 2016. LNCS, vol. 9641, pp. 38–56. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-32582-8_3
Foster, S., Cavalcanti, A., Canham, S., Woodcock, J., Zeyda, F.: Unifying theories of reactive design contracts. Theor. Comput. Sci. 802, 105–140 (2020)
Hoare, C.A.R.: Communicating Sequential Processes, vol. 178. Prentice-Hall, Englewood Cliffs (1985)
MathWorks: Simulink user’s guide (2021)
Meyer, B.: Applying “design by contract’’. Computer 25(10), 40–51 (1992)
Milner, R.: Communication and Concurrency, vol. 84. Prentice Hall, Englewood Cliffs (1989)
Rajhans, A., Avadhanula, S., Chutinan, A., Mosterman, P.J., Zhang, F.: Graphical modeling of hybrid dynamics with Simulink and Stateflow. In: Prandini, M., Deshmukh, J.V. (eds.) Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week), HSCC 2018, Porto, Portugal, 11–13 April 2018, pp. 247–252. ACM (2018)
Sangiovanni-Vincentelli, A., Damm, W., Passerone, R.: Taming Dr. Frankenstein: contract-based design for cyber-physical systems. Eur. J. Control 18(3), 217–238 (2012)
Ye, K., Foster, S., Woodcock, J.: Compositional assume-guarantee reasoning of control law diagrams using UTP (2018). https://eprints.whiterose.ac.uk/129640/15/Compositional_Assume_Guarantee_Reasoning_of_Control_Law_Diagrams_using_UTP_Tech_Report.pdf. Accessed 3 Apr 2022
Ye, K., Foster, S., Woodcock, J.: Compositional assume-guarantee reasoning of control law diagrams using UTP. In: Adamatzky, A., Kendon, V. (eds.) From Astrophysics to Unconventional Computation. ECC, vol. 35, pp. 215–254. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-15792-0_10
Zhou, C., Kumar, R.: Semantic translation of Simulink diagrams to input/output extended finite automata. Discret. Event Dyn. Syst. 22(2), 223–247 (2012)
Zou, L., Zhan, N., Wang, S., Fränzle, M., Qin, S.: Verifying Simulink diagrams via a hybrid Hoare logic prover. In: Ernst, R., Sokolsky, O. (eds.) Proceedings of the International Conference on Embedded Software, EMSOFT 2013, Montreal, QC, Canada, 29 September–4 October 2013, pp. 9:1–9:10. IEEE (2013)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2022 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Sun, Q., Zhang, W., Wang, C., Liu, Z. (2022). A Contract-Based Semantics and Refinement for Simulink. In: Dong, W., Talpin, JP. (eds) Dependable Software Engineering. Theories, Tools, and Applications. SETTA 2022. Lecture Notes in Computer Science, vol 13649. Springer, Cham. https://doi.org/10.1007/978-3-031-21213-0_9
Download citation
DOI: https://doi.org/10.1007/978-3-031-21213-0_9
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-21212-3
Online ISBN: 978-3-031-21213-0
eBook Packages: Computer ScienceComputer Science (R0)