Towards a UTP semantics for Modelica. (English) Zbl 1483.68053
Bowen, Jonathan P. (ed.) et al., Unifying theories of programming. 6th international symposium, UTP 2016, Reykjavik, Iceland, June 4–5, 2016. Revised selected papers. Cham: Springer. Lect. Notes Comput. Sci. 10134, 44-64 (2017).
Summary: 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.
For the entire collection see [Zbl 1355.68010].
For the entire collection see [Zbl 1355.68010].
MSC:
| 68N15 | Theory of programming languages |
| 68Q55 | Semantics in the theory of computing |
| 68V20 | Formalization of mathematics in connection with theorem provers |
| 93-10 | Mathematical modeling or simulation for problems pertaining to systems and control theory |
| 93C30 | Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems) |
Software:
Isabelle; Isabelle/HOL; Sledgehammer; Lifting; Circus; Isabelle/UTP; Transfer; Isabelle/Circus; Handel-CReferences:
| [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) · Zbl 1187.68139 · doi:10.1016/j.scico.2009.07.003 |
| [2] | Bachmann, B., Aronsson, P., Fritzson, P.: Robust initialization of differential algebraic equation. In: 5th International Modelica Conference, Austria, September 2006 |
| [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 · Zbl 1348.68214 · doi:10.1007/978-3-642-24364-6_2 |
| [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 · doi:10.1007/11889229_6 |
| [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 · doi:10.1007/978-3-642-27705-4_20 |
| [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) · Zbl 0963.68121 |
| [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 · Zbl 0974.68186 · doi:10.1007/3-540-44659-1_10 |
| [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) · doi:10.1109/SYSOSE.2014.6892473 |
| [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 · Zbl 1457.68061 · doi:10.1007/978-3-319-14806-9_2 |
| [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 · Zbl 1152.68520 · doi:10.1007/11541868_8 |
| [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 · Zbl 1161.68388 · doi:10.1007/978-3-540-85762-4_10 |
| [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 · Zbl 1286.68079 · doi:10.1007/978-3-642-13321-3_12 |
| [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) |
| [15] | He, J.: HRML: a hybrid relational modelling language. In: IEEE International Conference on Software Quality, Reliability and Security, QRS 2015, August 2015 |
| [16] | Henzinger, T.A.: The theory of hybrid automata, pp. 278–292. IEEE (1996) · Zbl 0959.68073 · doi:10.1109/LICS.1996.561342 |
| [17] | Hoare, T.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985) · Zbl 0637.68007 |
| [18] | Hoare, T., He, J.: Unifying Theories of Programming. Prentice-Hall, Englewood Cliffs (1998) · Zbl 1005.68036 |
| [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 · Zbl 1426.68284 · doi:10.1007/978-3-319-03545-1_9 |
| [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) |
| [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 · doi:10.1007/978-3-642-17164-2_1 |
| [22] | Modelica Association. Modelica - A Unified Object-Oriented Language for Systems Modeling - Version 3.3 Revision 1. Standard Specification, July 2014 |
| [23] | Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Berlin (2002) · Zbl 0994.68131 |
| [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 |
| [25] | Pantelides, C.: The consistent initialization of differential-algebraic systems. SIAM J. Sci. Stat. Comput. 9(2), 213–231 (1988) · Zbl 0643.65039 · doi:10.1137/0909014 |
| [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 · Zbl 1286.68035 · doi:10.1007/978-3-642-14521-6_9 |
| [27] | Platzer, A.: Logical Analysis of Hybrid Systems. Springer, Heidelberg (2010) · Zbl 1211.68412 · doi:10.1007/978-3-642-14509-4 |
| [28] | Satabin, L., Colao, J., Andrieu, O., Pagano, B.: Towards a formalized Modelica subset. In: 11th International Modelica Conference, September 2015 · doi:10.3384/ecp15118637 |
| [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) · doi:10.4173/mic.2015.1.3 |
| [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 · Zbl 1452.68057 · doi:10.1007/978-3-642-35705-3_3 |
| [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 · doi:10.1007/978-3-319-06410-9_49 |
| [32] | Zhou, C., Hansen, M.R.: Chopping a point. In: Proceedings of 7th BCS-FACS Refinement Workshop. Springer, Heidelberg (1996) |
| [33] | Zhou, C., Hoare, C.A.R., Ravn, A.P.: A calculus of durations. Inf. Process. Lett. 40(5), 269–276 (1991) · Zbl 0743.68097 · doi:10.1016/0020-0190(91)90122-X |
| [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 · doi:10.1007/BFb0020972 |
| [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 · doi:10.1007/3-540-57318-6_23 |
| [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 · Zbl 1309.68025 · doi:10.1007/978-3-642-16690-7_15 |
| [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 · Zbl 1471.68159 · doi:10.1007/978-3-319-24953-7_33 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
