Abstract
Simulink is widely used by engineers to provide graphical specifications of control laws; its frequent use to specify safety-critical systems has motivated work on formal modelling and analysis of Simulink diagrams. The work that we present here is complementary: it targets verification of implementations by providing a refinement-based model. We use CircusTime, a timed version of the Circus notation that combines Z, CSP, and Morgan’s refinement calculus with a time model, and which is firmly based on Hoare & He’s Unifying Theories of Programming. We present a modelling approach that formalises the simulation time model that is routinely used for analysis. It is distinctive in that we use a refinement-based notation and capture functionality, concurrency, and time. The models produced in this way, however, are not useful for program verification, due to an idealised simulation time model; therefore, we describe how such models can be used to construct more realistic models. This novel modelling approach caters for assumptions about the programming environment, and clearly establishes the relationship between the simulation and implementation models.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Arthan, R., Caseley, P., O’Halloran, C.M., Smith, A.: ClawZ: Control laws in Z. In: Proceedings of the 3rd IEEE International Conference on Formal Engineering Methods, ICFEM 2000, York, September 4-7, pp. 169–176. IEEE Computer Society, IEEE Press (2000)
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)
Cavalcanti, A., Clayton, P., O’Halloran, C.: Control law diagrams in Circus. In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582, pp. 253–268. Springer, Heidelberg (2005)
Cavalcanti, A.L.C., Clayton, P., O’Halloran, C.: From control law diagrams to Ada via Circus. Formal Aspects of Computing 23(4), 465–512 (2011)
Cavalcanti, A.L.C., Woodcock, J.C.P., Dunne, S.: Angelic nondeterminism in the Unifying Theories of Programming. Formal Aspects of Computing 18(3), 288–307 (2006)
Chen, C., Dong, J.S., Sun, J.: A formal framework for modeling and validating Simulink diagrams. Formal Aspects of Computing 21(5), 451–484 (2009)
Denney, E., Fischer, B.: Generating customized verifiers for automatically generated code. In: Smaragdakis, Y., Siek, J.G. (eds.) Proceedings of the 7th International Conference on Generative Programming and Component Engineering, GPCE 2008, Nashville, October 19-23, pp. 77–88. ACM (2008)
Feliachi, A., Gaudel, M.-C., Wolff, B.: Isabelle/Circus: A process specification and verification environment. In: Joshi, R., Müller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol. 7152, pp. 243–260. Springer, Heidelberg (2012)
Feliachi, A., Wolff, B., Gaudel, M.-C.: Isabelle/Circus. Archive of Formal Proofs (2012), http://afp.sourceforge.net/entries/Circus.shtml
Giese, H., Hirsch, M.: Modular verification of safe online-reconfiguration for proactive components in mechatronic UML. In: Bruel, J.-M. (ed.) MoDELS 2005. LNCS, vol. 3844, pp. 67–78. Springer, Heidelberg (2006)
Graf, S., Gérard, S., Haugen, Ø., Ober, I., Selic, B.: Modelling and analysis of real time and embedded systems – Using UML. In: Kühne, T. (ed.) MoDELS 2006. LNCS, vol. 4364, pp. 126–130. Springer, Heidelberg (2007)
Hoare, C.A.R.: Communicating Sequential Processes. Series in Computer Science. Prentice Hall International (1986)
Hoare, C.A.R., He, J.: Unifying Theories of Programming. Series in Computer Science. Prentice Hall (1998)
Jersak, M., Ziegenbein, D., Wolf, F., Richter, K., Ernst, R., Cieslog, F., Teich, J., Strehl, K., Thiele, L.: Embedded system design using the SPI Workbench. In: Proceedings of the 3rd International Forum on Design Languages (2000)
Joshi, A., Heimdahl, M.P.E.: Model-based safety analysis of Simulink models using SCADE Design Verifier. In: Winther, R., Gran, B.A., Dahll, G. (eds.) SAFECOMP 2005. LNCS, vol. 3688, pp. 122–135. Springer, Heidelberg (2005)
Kirsch, C.M., Sanvido, M.A.A., Henzinger, T.A., Pree, W.: A Giotto-based helicopter control system. In: Sangiovanni-Vincentelli, A.L., Sifakis, J. (eds.) EMSOFT 2002. LNCS, vol. 2491, pp. 46–60. Springer, Heidelberg (2002)
The MathWorks, Inc., Simulink, http://www.mathworks.com/products/simulink
Morgan, C.C.: Programming from Specifications, 2nd edn. Prentice Hall (1994)
Mota, A.C., Sampaio, A.C.A.: Model-checking CSP-Z: strategy, tool support and industrial application. Science of Computer Programming 40, 59–96 (2001)
Oliveira, M.V.M., Cavalcanti, A.L.C., Woodcock, J.C.P.: A UTP semantics for Circus. Formal Aspects of Computing 21(1-2), 3–32 (2009)
Oliveira, M., Cavalcanti, A., Woodcock, J.: Unifying theories in ProofPower-Z. Formal Aspects of Computing 25(1), 133–158 (2013)
Reed, G.M., Roscoe, A.W.: A timed model for communicating sequential processes. Theoretical Computer Science 58, 249–261 (1988)
Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice Hall Series in Computer Science (1998)
Schneider, S.: Concurrent and Real-time Systems: The CSP Approach. Wiley (2000)
Sherif, A., He, J.: Towards a time model for Circus. In: George, C., Miao, H. (eds.) ICFEM 2002. LNCS, vol. 2495, pp. 613–624. Springer, Heidelberg (2002)
Sherif, A., et al.: A framework for specification and validation of real-time systems using Circus actions. In: Liu, Z., Araki, K. (eds.) ICTAC 2004. LNCS, vol. 3407, pp. 478–493. Springer, Heidelberg (2005)
Sherif, A., Cavalcanti, A.L.C., He, J., Sampaio, A.C.A.: A process algebraic framework for specification and validation of real-time systems. Formal Aspects of Computing 22(2), 153–191 (2010)
Woodcock, J., Cavalcanti, A.: A concurrent language for refinement. In: Butterfield, A., Strong, G., Pahl, C. (eds.) 5th Irish Workshop on Formal Methods, IWFM 2001, Dublin, July 16-17, BCS, Workshops in Computing (2001)
Woodcock, J., Cavalcanti, A.: The semantics of Circus. In: Bert, D., et al. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272, pp. 184–203. Springer, Heidelberg (2002)
Woodcock, J.C.P., Davies, J.: Using Z—Specification, Refinement, and Proof. Prentice-Hall (1996)
Zeyda, F., Cavalcanti, A.: Mechanised Translation of Control Law Diagrams into Circus. In: Leuschel, M., Wehrheim, H. (eds.) IFM 2009. LNCS, vol. 5423, pp. 151–166. Springer, Heidelberg (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Cavalcanti, A., Mota, A., Woodcock, J. (2013). Simulink Timed Models for Program Verification. In: Liu, Z., Woodcock, J., Zhu, H. (eds) Theories of Programming and Formal Methods. Lecture Notes in Computer Science, vol 8051. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39698-4_6
Download citation
DOI: https://doi.org/10.1007/978-3-642-39698-4_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-39697-7
Online ISBN: 978-3-642-39698-4
eBook Packages: Computer ScienceComputer Science (R0)