Hybrid Modeling Language Hyml And Its Formal Semantics

Cyber-Physical Systems (CPS) are autonomous physical entities which are integrat-ed with the ability of sensing and communication. With the continuous development of computer science and IT industry, the application of CPS are diversely expanded, rang-ing from the large scale nuclear plants and chemical processes to embedded healthcare systems and self-piloting automobiles. Any tiny error in these applications may threat-en people’s life and lead to great loss, especially in some safety critical systems. The heterogenous nature of CPS and tight interaction among the components make the devel-opment of CPS even harder.In Computer Science, the theory of programming and algebraic approach can be used to develop correct software product but only for discrete systems. The control the-ory communities are devoted to the continuous physical world but seldom pay attention to the computing side. As to CPS, the first step is that we should put all the elements in one unified framework and give a reconsideration about the integration of different components.In this paper, we present a new modeling language HyML used for specifying and programming of CPS. Inspired by the unifying theory of programming, we investigate the observational-oriented denotational semantics and algebraic semantics and prove the consistency of algebraic laws with respect to the denotational semantics. The normal form of the hybrid program is explored and in the transformation process the structure of program is greatly reduced. The decomposition of hybrid program via the algebraic laws are illustrated as well. Our approach illustrates the importance of algebraic approach in the unifying theory of programming and also makes contribution to the development of the theory of programming languages for complex systems.The main contribution of this paper includes:·We propose a new modeling language HyMLfor CPS.It can be used to model the heterogenous components of CPS and the interaction among them. The novel guard structure unifies the interaction among heterogenous components of CPS.·We present the algebraic semantics and denotational semantics of HyML respec-tively and prove the consistency of algebraic semantics with respect to the deno-tational semantics, which enhances the reliability of program transformation via algebraic laws.·We explore the applications of algebraic approach on the development of trust- worthy CPS. The corresponding normal forms are investigated and all programs can be algebraically reduced to normal forms. We also propose a coarse-grained framework of program decomposition based on algebraic laws, which can be used to decompose the program into physical program and controller program.