Research On Hybrid Modeling Language For Periodic Controllers

A hybrid system is a dynamic system consisting of continuous and discrete dynamics.The continuous part usually simulates the interaction of the physical environment,while the discrete part usually simulates the operation of the control system.The combination of computation and control can lead to very complex system designs,so they are often found in aerospace,automotive industry and factory automation designs.So far,several formal modeling approaches have been used in hybrid systems: hybrid automata,hybrid Petri nets,Modelica,Zelus,etc.For the formal verification of hybrid systems,a variety of tools are available,such as Hy Tech,PHAVer,d/dt,Space Ex,Flow*,Julia Reach,etc.The common feature of these modeling languages and verification tools is that they focus mainly on modeling hybrid systems at the macro level of abstraction.In the cyber-physical fusion system,the controller is widely designed as a mode-based periodic module for controlling physical equipment.This system can be modeled as a hybrid system,that is,a real-time controller program and an interactive continuous object that obeys dynamic laws.Embedded software and its operating environment have the characteristics of high complexity and unpredictability.This requires that the modeling language must have the ability to describe different components of the system and the environment,and it can engrave the picture to the model characteristics of the embedded software,and at the same time have Composability and the ability to express multiple modes of interaction.At present,many languages about cycle control solve the previous problems,but only focus on discrete-time dynamic systems and lack interaction with the physical world.In order to realize real-time perception of external physical objects and the environment,reliable information transmission,and precise dynamic control For goals such as coordination and coordination,the proposed language needs to be able to model discrete control logic and continuous physical changes,and describe the interaction between them,so as to better carry out correct and accurate verification and analysis.To facilitate the modeling and analysis of periodic hybrid control systems in aerospace and smart cities,this paper proposes a Hierarchical Hybrid Modeling Language(HHML)for periodic controllers,which consists of a two-layer structure,a pattern abstraction layer and a module control flow layer.The former supports the modeling of hybrid systems at the abstraction level,while the latter is used to describe the behavior of modules,so that the description and design of physical and control processes of hybrid systems can be placed in a unified formal framework through this language.In addition,the introduction of operational semantics can help developers to avoid the duality of natural languages to understand this language,and it can also be used for formal analysis.Hybrid automata transformation rules for formal verification provide a solid theoretical basis for the analysis,design,reasoning and verification of hybrid systems.Finally,the effectiveness of our proposed approach is verified by using the lunar lander as an example.The main contributions of this article are:(1)Hybrid modeling language design for embedded software: develop a hybrid modeling language that can formally and uniformly describe the control behavior of embedded software and the physical environment in which it runs.(2)Semantic theory of hybrid modeling language: Study the operational semantics of the modeling language,and provide a solid semantic theoretical foundation for the design,analysis and verification of embedded software.(3)Translation rules of hybrid modeling language: Study how to convert the model built by HHML into hybrid automata,and then into the hybrid system verification tool,so that the properties of the built model can be verified.