Font Size: a A A

Hybrid Event-B:Modeling And Refinement Of Cyber-Physical Systems

Posted on:2019-11-08Degree:DoctorType:Dissertation
Country:ChinaCandidate:J LiuFull Text:PDF
GTID:1368330566461215Subject:Computer application technology
Abstract/Summary:PDF Full Text Request
The Cyber-Physical Systems are a new type of system with high integration and deep collaboration between the cyber world and the physical world.The Cyber-Physical Systems are the first of the eight key information technologies in the future.It has a3 C structure which deeply integrates computational intelligence,communication and control,so it enables the calculation process to be integrated with the physical process.And the systems not only contain discrete calculations,but also involve the processing of continuous physical process,forming the dynamic recombination and integration of network,control and embedded system.The Cyber-Physical Systems have capability of state perception,real-time communication,information calculation,precision control and autonomous coordination,and improve the index of the stability,reliability,robustness and efficiency of the industrial system,and promote the development of industrial economy and the comprehensive benefit of society.Because the Cyber-Physical Systems are deeply integrated into productive life,if something goes wrong,it could lead to incalculable life and property damage.Therefore,the Cyber-Physical Systems have a higher requirement for security and reliability than the general traditional systems.Because of a high degree of complexity,complexity,and higher security requirements of the Cyber-Physical Systems in design and development,the design and development of systems face a bigger challenge.How to establish a credible Cyber-Physical System is one of the problems of the world in the domestic and international,industry and academia.In the field of computer science,Event-B is considered to be an effective formalization of the development of complex systems,which have many successful case.As a widely applied development language via refinement,the Event-B language provides a complete series of mechanisms for development via refinement.However,it only supports the development of discrete systems.We used the framework of Event-B as a basis,and proposed an extension method of Event-B that can be used to construct a model and to refine continuous behaviors,as well as to prove the correctness of the model.Taking into consideration the diversity of hybrid systems,we borrowed the modeling mechanism of classical hybrid automata,and proposed a differential event to extend the machine structure of the Event-B language.The purpose was to ensure a strong modeling capability of the new modeling language that can be used in a variety of hybrid systems.Event-B proved the correctness of a model through proving a series of pre-defined proof obligation rules.Based on the correctness and consistency requirements of modeling hybrid systems,we established proof obligation rules of the new differential events.These proof obligation rules can ensure the correct development of hybrid systems.Because the differential events adopt differential equations to construct a model of continuous behaviors,we proposed a proof obligation-proving method based on differential invariants without solving the differential equations.We also integrated Rodin with KeYmaera as a support tool.Our case study on a train control system demonstrated that the proposed extension of Event-B can be used to effectively refine and develop hybrid systems.Based on theory of Event-B,we have proposed the modeling and refinement method of the Hybrid Event-B.The paper mainly proposes a comprehensive and elaboration scheme for developing the Cyber-Physical Systems about modeling,proving obligation,verification technology and verification tools.The main contents are follow as:·For the modeling requirements of the hybrid behavior in the Cyber-Physical Systems,Event-B was extended to get a new modeling language,Hybrid Event-B.In addition to modeling discrete behavior with conventional events,the language also models continuous behavior by introducing a new event type,the differential event.At the same time we inherited and learned the discrete and continuous interaction mechanism of the hybrid automaton,so as to achieve the integration of the cyber world and the physical world.The research provides a modeling method for the development of the Cyber-Physical Systems.·The proof obligations of Hybrid Event-B model have been given.The proof obligations are some presetting rules in the Hybrid Event-B,and the correctness of the model is confirmed by the proof obligations.According to Floyd assertion theory,Hoare logic and refinement theory,the obligation of invariant,reliability and refinement proof is proposed for Hybrid Event-B,which provides a correct verification basis for the development of Cyber-Physical Systems.·Proposed and demonstrated a proof of obligation based on differential invariants.Hybrid Event-B's differential events use differential equations to model continuous behavior.Using differential invariant techniques,verification obligations can be verified without solving differential equations.We use differential invariant technology in the development of refinement is a very important technical and theoretical contribution.It effectively enhances the application scope and practicality of the Cyber-Physical Systems for precision development.It also extends the application of differential invariant theory.·Explored a tool scheme of Rodin and KeYmaera.The tool is an important step in the practical development of refinement.By analyzing Rodin,it is an open interface tool platform for traditional Event-B.According to the working mechanism of the Rodin platform and the characteristics of the platform interface,the extension elements of the Hybrid Event-B are added into the Rodin platform,and the integration scheme of the KeYmaera theorem prover are proposed.the proof obligations of the differential event will be transformed to the input of the KeYmaera theorem prover,and verified the proof obligations based on differential invariants.
Keywords/Search Tags:Cyber Physical System, Hybrid systems, Hybrid Event-B, differential invariants, proof obligation, refinement development
PDF Full Text Request
Related items