Research On ZIA Formal Model And It’s Automatic Validation Method For Hybrid Systems

At present, Real-time and Embedded systems are so widely used that to ensure its accuracy andreliability has become current research focus. MARTE is a UML modeling specifications in the fieldof Real-time and Embedded systems, which complements the insufficient ability of non-functionalproperties of UML. MARTE specification uses a graphical way to describe systems lacking of precisesemantics which makes it difficult for formal analysis and verification directly. In the developmentprocess of modern software systems, which often require us to deal with the input data of the system,as well as transitions between the states under the constraints of time, and finally give thecorresponding output data. So it is also necessary to deal with data variables. Formal methods as abasis of mathematical methods can clearly, precisely, abstractly, concisely specify and verify softwaresystem and its properties, which greatly improve the safety and reliability of the software.The paper converts MARTE model into formal model for verification to ensure softwarereliability. Firstly, we extend MARTE specification by combining MARTE with Z-language todescribe Real-time and Embedded systems with data constraints Z-MARTE. Secondly, we present aformal specification which describes real-time system with data constraints ZIA specification basedon continuous-time, and convert Z-MARTE to ZIA model based on continuous-time. When we realizemodel checking for ZIA model based on continuous-time, we realize model checking for Z-MARTE.Finally, we give the model checking algorithm of the ZIA specification based on continuous-time, andverify the method through an example, to demonstrate the feasibility and effectiveness of the methodin the article.In addition, the traditional ZIA did not characterize the probability aspect of the system.So weexpand probabilistic nature on the traditional ZIA and present a probabilistic systemspecification PZIA so that it can not only characterize the behavior and state of the system,but alsocharacterize the probabilistic nature of the system. As for traditional temporal logic like CTL andPCTL, the logic is powerful, but only reflecting the temporal properties. To address these limitations,in this work we propose a new, formal language to express performance queries, while retaining theability to express temporal properties. Then we give a checking algorithm for performance queries ofprobabilistic systems.