Skip to main content
SpringerLink
Log in

Towards a UTP Semantics for Modelica

  • Conference paper
  • First Online:
Unifying Theories of Programming (UTP 2016)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10134))

Included in the following conference series:

Abstract

We describe our work on a UTP semantics for the dynamic systems modelling language Modelica. This is a language for modelling a system’s continuous behaviour using a combination of differential-algebraic equations and an event-handling system. We develop a novel UTP theory of hybrid relations, inspired by Hybrid CSP and Duration Calculus, that is purely relational and provides uniform handling of continuous and discrete variables. This theory is mechanised in our Isabelle implementation of the UTP, Isabelle/UTP, with which we verify some algebraic properties. Finally, we show how a subset of Modelica models can be given semantics using our theory. When combined with the wealth of existing UTP theories for discrete system modelling, our work enables a sound approach to heterogeneous semantics for Cyber-Physical systems by leveraging the theory linking facilities of the UTP.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    http://www.3ds.com/products-services/catia/products/dymola.

  2. 2.

    http://www.wolfram.com/system-modeler/.

  3. 3.

    http://www.maplesoft.com/products/maplesim/.

  4. 4.

    https://www.openmodelica.org/.

  5. 5.

    Notice that in the general case ICs for DAE systems may actually involve derivatives \(\underline{\dot{v}}_i\) of \(\underline{v}_i\) [25]. Modelica supports the general case and sophisticated algorithms for finding consistent ICs from “guess” values exist [2, 24]. However, numerical/symbolic methods for solving IVPs is not within the scope of our current work. Hence, we only consider less general ICs and presume that consistent ICs are provided.

  6. 6.

    See https://github.com/isabelle-utp/utp-main/tree/shallow.

  7. 7.

    Our Isabelle/UTP theory development, including all omitted proofs, is available at http://www.cs.york.ac.uk/~simonf/utp2016.

  8. 8.

    An Integrated Tool-chain for Model-based Design of Cyber-Physical Systems. EU H2020 grant agreement 644047. http://into-cps.au.dk/.

References

  1. Åkesson, J., Ekman, T., Hedin, G.: Implementation of a Modelica compiler using JastAdd attribute grammars. Sci. Comput. Program. 75(1–2), 21–38 (2010). Special Issue on ETAPS 2006 and 2007 Workshops on Language Descriptions, Tools, and Applications (LDTA 2006 and 2007)

    Article  MathSciNet  MATH  Google Scholar 

  2. Bachmann, B., Aronsson, P., Fritzson, P.: Robust initialization of differential algebraic equation. In: 5th International Modelica Conference, Austria, September 2006

    Google Scholar 

  3. Blanchette, J.C., Bulwahn, L., Nipkow, T.: Automatic proof and disproof in Isabelle/HOL. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) FroCoS 2011. LNCS (LNAI), vol. 6989, pp. 12–27. Springer, Berlin (2011). doi:10.1007/978-3-642-24364-6_2

    Chapter  Google Scholar 

  4. Cavalcanti, A., Woodcock, J.: A tutorial introduction to CSP in unifying theories of programming. In: Cavalcanti, A., Sampaio, A., Woodcock, J. (eds.) PSSE 2004. LNCS, vol. 3167, pp. 220–268. Springer, Berlin (2006). doi:10.1007/11889229_6

    Chapter  Google Scholar 

  5. 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, Berlin (2012). doi:10.1007/978-3-642-27705-4_20

    Chapter  Google Scholar 

  6. Fidge, C.J.: Modelling discrete behaviour in a continuous-time formalism. In: Araki, K., Galloway, A., Taguchi, K. (eds.) Proceedings of the 1st International Conference on Integrated on Integrated Formal Methods, pp. 170–188. Springer, Heidelberg (1999)

    Google Scholar 

  7. Fleuriot, J.D.: On the mechanization of real analysis in Isabelle/HOL. In: Aagaard, M., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol. 1869, pp. 145–161. Springer, Berlin (2000). doi:10.1007/3-540-44659-1_10

    Chapter  Google Scholar 

  8. FMI development group. Functional mock-up interface for model exchange and co-simulation, 2.0 (2014). https://www.fmi-standard.org

  9. Foster, S., Miyazawa, A., Woodcock, J., Cavalcanti, A., Fitzgerald, J., Larsen, P.: An approach for managing semantic heterogeneity in systems of systems engineering. In: Proceedings of the 9th International Conference on Systems of Systems Engineering. IEEE (2014)

    Google Scholar 

  10. Foster, S., Zeyda, F., Woodcock, J.: Isabelle/UTP: a mechanised theory engineering framework. In: Naumann, D. (ed.) UTP 2014. LNCS, vol. 8963, pp. 21–41. Springer, Cham (2015). doi:10.1007/978-3-319-14806-9_2

    Google Scholar 

  11. Harrison, J.: A HOL theory of euclidean space. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 114–129. Springer, Berlin (2005). doi:10.1007/11541868_8

    Chapter  Google Scholar 

  12. Harwood, W., Cavalcanti, A., Woodcock, J.: A theory of pointers for the UTP. In: Fitzgerald, J.S., Haxthausen, A.E., Yenigun, H. (eds.) ICTAC 2008. LNCS, vol. 5160, pp. 141–155. Springer, Berlin (2008). doi:10.1007/978-3-540-85762-4_10

    Chapter  Google Scholar 

  13. Hayes, I.J., Dunne, S.E., Meinicke, L.: Unifying theories of programming that distinguish nontermination and abort. In: Bolduc, C., Desharnais, J., Ktari, B. (eds.) MPC 2010. LNCS, vol. 6120, pp. 178–194. Springer, Berlin (2010). doi:10.1007/978-3-642-13321-3_12

    Chapter  Google Scholar 

  14. He, J.: From CSP to hybrid systems. In: Roscoe, A.W. (ed.) A Classical Mind: Essays in Honour of C.A.R. Hoare, pp. 171–189. Prentice Hall (1994)

    Google Scholar 

  15. He, J.: HRML: a hybrid relational modelling language. In: IEEE International Conference on Software Quality, Reliability and Security, QRS 2015, August 2015

    Google Scholar 

  16. Henzinger, T.A.: The theory of hybrid automata, pp. 278–292. IEEE (1996)

    Google Scholar 

  17. Hoare, T.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)

    MATH  Google Scholar 

  18. Hoare, T., He, J.: Unifying Theories of Programming. Prentice-Hall, Englewood Cliffs (1998)

    MATH  Google Scholar 

  19. Huffman, B., Kunčar, O.: Lifting and transfer: a modular design for quotients in Isabelle/HOL. In: Gonthier, G., Norrish, M. (eds.) CPP 2013. LNCS, vol. 8307, pp. 131–146. Springer, Cham (2013). doi:10.1007/978-3-319-03545-1_9

    Chapter  Google Scholar 

  20. Kågedal, D., Fritzson, P.: Generating a Modelica compiler from natural semantics specifications. In: Proceedings of 1998 Summer Computer Simulation Conference, SCSC 1998 (1998)

    Google Scholar 

  21. Liu, J., Lv, J., Quan, Z., Zhan, N., Zhao, H., Zhou, C., Zou, L.: A calculus for hybrid CSP. In: Ueda, K. (ed.) APLAS 2010. LNCS, vol. 6461, pp. 1–15. Springer, Berlin (2010). doi:10.1007/978-3-642-17164-2_1

    Chapter  Google Scholar 

  22. Modelica Association. Modelica - A Unified Object-Oriented Language for Systems Modeling - Version 3.3 Revision 1. Standard Specification, July 2014

    Google Scholar 

  23. Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Berlin (2002)

    MATH  Google Scholar 

  24. Ochel, L.A., Bachmann, B.: Initialization of equation-based hybrid models within OpenModelica. In: 5th International Workshop on Equation-Based Object-Oriented Modeling Languages and Tools, Nottingham, UK, pp. 97–103, April 2013

    Google Scholar 

  25. Pantelides, C.: The consistent initialization of differential-algebraic systems. SIAM J. Sci. Stat. Comput. 9(2), 213–231 (1988)

    Article  MathSciNet  MATH  Google Scholar 

  26. Perna, J.I., Woodcock, J.: UTP semantics for handel-C. In: Butterfield, A. (ed.) UTP 2008. LNCS, vol. 5713, pp. 142–160. Springer, Berlin (2010). doi:10.1007/978-3-642-14521-6_9

    Chapter  Google Scholar 

  27. Platzer, A.: Logical Analysis of Hybrid Systems. Springer, Heidelberg (2010)

    Book  MATH  Google Scholar 

  28. Satabin, L., Colao, J., Andrieu, O., Pagano, B.: Towards a formalized Modelica subset. In: 11th International Modelica Conference, September 2015

    Google Scholar 

  29. Thiele, B., Knoll, A., Fritzson, P.: Towards qualifiable code generation from a clocked synchronous subset of modelica. Model. Identif. Control 36(1), 23–52 (2015)

    Article  Google Scholar 

  30. Wei, K., Woodcock, J., Cavalcanti, A.: Circus Time with reactive designs. In: Wolff, B., Gaudel, M.-C., Feliachi, A. (eds.) UTP 2012. LNCS, vol. 7681, pp. 68–87. Springer, Berlin (2013). doi:10.1007/978-3-642-35705-3_3

    Chapter  Google Scholar 

  31. Zhao, H., Yang, M., Zhan, N., Gu, B., Zou, L., Chen, Y.: Formal verification of a descent guidance control program of a lunar lander. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 733–748. Springer, Cham (2014). doi:10.1007/978-3-319-06410-9_49

    Chapter  Google Scholar 

  32. Zhou, C., Hansen, M.R.: Chopping a point. In: Proceedings of 7th BCS-FACS Refinement Workshop. Springer, Heidelberg (1996)

    Google Scholar 

  33. Zhou, C., Hoare, C.A.R., Ravn, A.P.: A calculus of durations. Inf. Process. Lett. 40(5), 269–276 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  34. Chaochen, Z., Ji, W., Ravn, A.P.: A formal description of hybrid systems. In: Alur, R., Henzinger, T.A., Sontag, E.D. (eds.) HS 1995. LNCS, vol. 1066, pp. 511–530. Springer, Berlin (1996). doi:10.1007/BFb0020972

    Chapter  Google Scholar 

  35. Chaochen, Z., Ravn, A.P., Hansen, M.R.: An extended duration calculus for hybrid real-time systems. In: Grossman, R.L., Nerode, A., Ravn, A.P., Rischel, H. (eds.) HS 1991–1992. LNCS, vol. 736, pp. 36–59. Springer, Berlin (1993). doi:10.1007/3-540-57318-6_23

    Chapter  Google Scholar 

  36. Zhu, H., Yang, F., He, J.: Generating denotational semantics from algebraic semantics for event-driven system-level language. In: Qin, S. (ed.) UTP 2010. LNCS, vol. 6445, pp. 286–308. Springer, Berlin (2010). doi:10.1007/978-3-642-16690-7_15

    Chapter  Google Scholar 

  37. Zou, L., Zhan, N., Wang, S., Fränzle, M.: Formal verification of simulink/stateflow diagrams. In: Finkbeiner, B., Pu, G., Zhang, L. (eds.) ATVA 2015. LNCS, vol. 9364, pp. 464–481. Springer, Cham (2015). doi:10.1007/978-3-319-24953-7_33

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of York, York, UK

    Simon Foster, Ana Cavalcanti & Jim Woodcock

  2. PELAB, Linköping University, Linköping, Sweden

    Bernhard Thiele

Authors
  1. Simon Foster
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Bernhard Thiele
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Ana Cavalcanti
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Jim Woodcock
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Simon Foster .

Editor information

Editors and Affiliations

  1. London South Bank University, London, United Kingdom

    Jonathan P. Bowen

  2. East China Normal University, Shanghai, China

    Huibiao Zhu

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Foster, S., Thiele, B., Cavalcanti, A., Woodcock, J. (2017). Towards a UTP Semantics for Modelica. In: Bowen, J., Zhu, H. (eds) Unifying Theories of Programming. UTP 2016. Lecture Notes in Computer Science(), vol 10134. Springer, Cham. https://doi.org/10.1007/978-3-319-52228-9_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-52228-9_3

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-52227-2

  • Online ISBN: 978-3-319-52228-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation