Applying Timed Interval Calculus to Simulink Diagrams

  • Chunqing Chen
  • Jin Song Dong
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4260)


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 timing analysis. In this paper, we present a systematic approach to translate Simulink diagrams to Timed Interval Calculus (TIC), a notation extending Z to support real-time system specification and verification. This work is based on the same angle chosen by Simulink and TIC where they model systems in terms of continuous time. Translated TIC specifications preserve the functional and timing aspects of the diagrams, and cover a wide range of Simulink blocks. After the translation, we can increase the design space by specifying important requirements, especially timing constraints exactly on the system or its components. Moreover, we can take advantage of TIC reasoning rules to formally verify systems with requirements, and hence elevate the design quality of Simulink.


Simulink Real-Time Specification Verification 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Adams, M.M., Clayton, P.B.: Clawz: Cost-effective formal verification for control systems. In: Lau, K.-K., Banach, R. (eds.) ICFEM 2005. LNCS, vol. 3785, pp. 465–479. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  2. 2.
    Arthan, R.D., Caseley, P., O’Halloran, C., Smith, A.: ClawZ: Control laws in Z. In: ICFEM 2000, pp. 169–176. IEEE Press, Los Alamitos (2000)Google Scholar
  3. 3.
    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)CrossRefGoogle Scholar
  4. 4.
    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)CrossRefGoogle Scholar
  5. 5.
    Dawson, J.E., Goré, R.: Machine-checking the timed interval calculus. In: Australian Joint Conference on Artificial Intelligence, pp. 95–106 (2002)Google Scholar
  6. 6.
    Fidge, C.J.: Modelling discrete behaviour in a continuous-time formalism. In: IFM 1999, pp. 170–188. Springer, Heidelberg (1999)Google Scholar
  7. 7.
    Fidge, C.J., Hayes, I.J., Mahony, B.P.: Defining differentiation and integration in Z. In: ICFEM 1998. IEEE Computer Society, Los Alamitos (1998)Google Scholar
  8. 8.
    Fidge, C.J., Hayes, I.J., Martin, A.P., Wabenhorst, A.: A set-theoretic model for real-time specification and reasoning. In: Jeuring, J. (ed.) MPC 1998. LNCS, vol. 1422, pp. 188–206. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  9. 9.
    Gupta, S., Krogh, B.H., Rutenbar, R.A.: Towards formal verification of analog designs. In: ICCAD 2004, pp. 210–217 (2004)Google Scholar
  10. 10.
    Hooman, J.: Specification and Compositional Verification of Real-Time Systems. Springer, New York (1991)zbMATHGoogle Scholar
  11. 11.
    ISO/IEC. Information Technology — Z Formal Specification Notation — Syntax, Type System and Semantics, 1st edn., 13568 (July 2002)Google Scholar
  12. 12.
    Jantsch, A., Sander, I.: Models of computation and languages for embedded system design. IEE Pro. on Comp. and Dig. Tech. 152(2), 114–129 (2005)CrossRefGoogle Scholar
  13. 13.
    Jersak, M., Cai, Y., Ziegenbein, D., Ernst, R.: A transformational approach to constraint relaxation of a time-driven simulation model. In: ISSS 2000 (2000)Google Scholar
  14. 14.
    Mahony, B.P., Hayes, I.J.: A case-study in timed refinement: A mine pump. IEEE Transactions on Software Engineering 18(9), 817–826 (1992)CrossRefGoogle Scholar
  15. 15.
    Martin, A., Fidge, C.J.: Lifting in Z. Electronic Notes in Theoretical Computer Science 42 (2001)Google Scholar
  16. 16.
    The MathWorks. Stateflow and Stateflow coder - For Complex Logic and State Diagram Modeling (2003)Google Scholar
  17. 17.
    The MathWorks. Simulink - Simulation and Model-based Design - Simulink Reference Version 6 (2004)Google Scholar
  18. 18.
    The MathWorks. Simulink - Simulation and Model-based Design - Using Simulink Version 6 (2004)Google Scholar
  19. 19.
    The MathWorks. Simulink Verification and Validation User’s Guide (March 2006)Google Scholar
  20. 20.
    Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL — A Proof Assistant for Higher-Order Logic. Springer, Heidelberg (2002)zbMATHGoogle Scholar
  21. 21.
    Pnueli, A.: Embedded systems: Challenges in specification and verification. In: Sangiovanni-Vincentelli, A.L., Sifakis, J. (eds.) EMSOFT 2002. LNCS, vol. 2491, pp. 1–14. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  22. 22.
    Sims, S., Cleaveland, R., Butts, K., Ranville, S.: Automated validation of software models. In: ASE 2001, pp. 91–96. IEEE Computer Society, Los Alamitos (2001)Google Scholar
  23. 23.
    Tiwari, A., Shankar, N., Rushby, J.: Invisible formal methods for embedded control systems. Proceedings of the IEEE 91(1), 29–39 (2003)CrossRefGoogle Scholar
  24. 24.
    Wabenhorst, A.: Induction in the timed interval calculus. Theoretical Computer Science 300(1-3), 181–207 (2003)zbMATHCrossRefMathSciNetGoogle Scholar
  25. 25.
    Wang, F.: Formal verification of timed systems: A survey and perspective. Proceedings of the IEEE 92(8), 1283–1307 (2004)CrossRefGoogle Scholar
  26. 26.
    Woodcock, J., Davies, J.: Using Z: Specification, Refinement and Proof. Prentice Hall International, Englewood Cliffs (1996)zbMATHGoogle Scholar
  27. 27.
    Zhou, C.C., Hansen, M.R.: Duration Calculus: A Formal Approach to Real-Time Systems. Springer, Heidelberg (2004)zbMATHGoogle Scholar
  28. 28.
    Zhou, C.C., Li, X.S.: A mean value calculus of durations. In: A classical mind: essays in honour of C. A. R. Hoare. Prentice-Hall International, Englewood Cliffs (1994)Google Scholar
  29. 29.
    Zhou, C.C., Ravn, A.P., Hansen, M.R.: An extended duration calculus for hybrid real-time systems. In: Hybrid Systems, pp. 36–59. Springer, Heidelberg (1993)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2006

Authors and Affiliations

  • Chunqing Chen
    • 1
  • Jin Song Dong
    • 1
  1. 1.School of ComputingNational University of Singapore 

Personalised recommendations