Abstract
A cyber-physical system (CPS) is an interactive system of continuous plants and real-time controller programs. These systems usually feature a tight relationship between the physical and computational components and exhibit strict true-concurrency with respect to time. These communication and concurrency issues have been well investigated in event-based synchronous languages but only for discrete systems. In this paper, we present an imperative-style programming language for CPS and explore an observation-oriented denotational semantics for the language. Furthermore, a set of algebraic laws that could facilitate the transformation of programs are investigated and consistency of the algebraic laws can be ensured with respect to the denotational semantics. The algebraic laws which have been established in the framework of our semantic model could greatly enhance the reliability of algebraic transformation.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Jifeng, H.: From CSP to hybrid systems. In: Roscoe, A.W. (ed.) A Classical Mind, pp. 171–189. Prentice Hall International (UK) Ltd., Hertfordshire (1994). http://dl.acm.org/citation.cfm?id=197600.197614
Henzinger, T.A.: The theory of hybrid automata. In: LICS, pp. 278–292. IEEE Computer Society (1996)
Lynch, N.A., Segala, R., Vaandrager, F.W.: Hybrid I/O Automata. Inf. Comput. 185(1), 105–157 (2003)
Benveniste, A., Bourke, T., Caillaud, B., Pouzet, M.: A hybrid synchronous language with hierarchical automata: static typing and translation to synchronous code. In: Chakraborty, S., Jerraya, A., Baruah, S.K., Fischmeister, S. (eds.) EMSOFT, pp. 137–148. ACM (2011)
Bauer, K., Schneider, K.: From synchronous programs to symbolic representations of hybrid systems. In: Johansson, K.H., Yi, W. (eds.) HSCC, pp. 41–50. ACM (2010)
Baldamus, M., Stauner, T.: Modifying Esterel concepts to model hybrid systems. Electr. Notes Theor. Comput. Sci. 65(5), 35–49 (2002)
Fritzson, P.: Modelica - a cyber-physical modeling language and the OpenModelica environment. In: IWCMC, pp. 1648–1653. IEEE (2011)
Su, W., Abrial, J.-R., Zhu, H.: Complementary methodologies for developing hybrid systems with event-b. In: Aoki, T., Taguchi, K. (eds.) ICFEM 2012. LNCS, vol. 7635, pp. 230–248. Springer, Heidelberg (2012)
Abrial, J.-R., Su, W., Zhu, H.: Formalizing hybrid systems with event-b. In: Derrick, J., Fitzgerald, J., Gnesi, S., Khurshid, S., Leuschel, M., Reeves, S., Riccobene, E. (eds.) ABZ 2012. LNCS, vol. 7316, pp. 178–193. Springer, Heidelberg (2012)
Benveniste, A., Caspi, P., Edwards, S.A., Halbwachs, N., Guernic, P.L., de Simone, R.: The synchronous languages 12 years later. Proceedings of the IEEE 91(1), 64–83 (2003)
Zhao, Y., Jifeng, H.: Towards a signal calculus for event-based synchronous languages. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol. 6991, pp. 1–13. Springer, Heidelberg (2011)
Zhao, Y., Zhu, L., Zhu, H., He, J.: A denotational model for instantaneous signal calculus. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol. 7504, pp. 126–140. Springer, Heidelberg (2012)
He, J., Xu, Q.: Advanced features of Duration Calculus and their applications in sequential hybrid programs. Formal Asp. Comput. 15(1), 84–99 (2003)
Jifeng, H., Naiyong, J.: Integrating variants of DC. In: Liu, Z., Araki, K. (eds.) ICTAC 2004. LNCS, vol. 3407, pp. 14–34. Springer, Heidelberg (2005). http://dx.doi.org/10.1007/978-3-540-31862-0_2
Li, L.: Towards a denotational semantics of timed RSL using Duration Calculus. Journal of Computer Science and Technology 16(1), 64–76 (2001). http://dx.doi.org/10.1007/BF02948854
Roscoe, A.W., Hoare, C.A.R.: The laws of Occam programming. Theor. Comput. Sci. 60, 177–229 (1988)
Maler, O., Manna, Z., Pnueli, A.: From timed to hybrid systems. In: de Bakker, J.W., Huizing, C., de Roever, W.P., Rozenberg, G. (eds.) REX 1991. LNCS, vol. 600, pp. 447–484. Springer, Heidelberg (1992)
Kapur, A., Henzinger, T.A., Manna, Z., Pnueli, A.: Prooving safety properties of hybrid systems. In: Langmaack, H., de Roever, W.-P., Vytopil, J. (eds.) FTRTFT 1994. LNCS, vol. 863, pp. 431–454. Springer, Heidelberg (1994)
Carloni, L.P., Passerone, R., Pinto, A., Angiovanni-Vincentelli, A.L.: Languages and tools for hybrid systems design. Found. Trends Electron. Des. Autom. 1(1/2), 1–193 (2006). http://dx.doi.org/10.1561/1000000001
Modelica. https://www.modelica.org/
Benveniste, A., Caillaud, B., Pouzet, M.: The fundamentals of hybrid systems modelers. In: 2010 49th IEEE Conference on Decision and Control (CDC), pp. 4180–4185 (2010)
Nikoukhah, R.: Hybrid dynamics in modelica: Should all events be considered synchronous
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, Heidelberg (2010)
Platzer, A.: Logical Analysis of Hybrid Systems - Proving Theorems for Complex Dynamics. Springer (2010)
Author information
Authors and Affiliations
Corresponding authors
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Zhu, L., Xu, Q., He, J., Zhu, H. (2015). A Formal Model for a Hybrid Programming Language. In: Naumann, D. (eds) Unifying Theories of Programming. UTP 2014. Lecture Notes in Computer Science(), vol 8963. Springer, Cham. https://doi.org/10.1007/978-3-319-14806-9_7
Download citation
DOI: https://doi.org/10.1007/978-3-319-14806-9_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-14805-2
Online ISBN: 978-3-319-14806-9
eBook Packages: Computer ScienceComputer Science (R0)