zbMATH — the first resource for mathematics

Stepwise development of Simulink models using the refinement calculus framework. (English) Zbl 1147.68826
Jones, Cliff B. (ed.) et al., Theoretical aspects of computing – ICTAC 2007. 4th international colloquium, Macau, China, September 26–28, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-75290-5/pbk). Lecture Notes in Computer Science 4711, 79-93 (2007).
Summary: Simulink is a popular tool for model-based development of control systems. However, due to the complexity caused by the increasing demand for sophisticated controllers, validation of Simulink models is becoming a more difficult task. To ensure correctness and reliability of large models, it is important to be able to reason about model parts and their interactions. This paper provides a definition of contracts and refinement using the action system formalism. Contracts enable abstract specifications of model parts, while refinement offers a framework to reason about correctness of implementation of contracts, as well as composition of model parts. An example is provided to illustrate system development using contracts and refinement.
For the entire collection see [Zbl 1143.68007].

68U20 Simulation (MSC2010)
68Q60 Specification and verification (program logics, model checking, etc.)
93B40 Computational methods in systems theory (MSC2010)
ClawZ; JML; Simulink
Full Text: DOI