Formal Analysis And Verification Of Hybrid Systems Via Co-Verification And Hybrid Relations

With the rapid development of technologies on software engineering, integrated circuit, network, and communication, the connections and interactions increasingly become much more intimate and significant between human beings and the natural world. Hybrid system, as a fundamental model combining and revealing continuous feature of natural world and discrete feature for computation, has been studied by numerous researchers in the areas ranged over mathematics, automatic control, computer science, and even biological chemistry in the last 30 years. Nowadays formal methods play an important role among numerous theories and methods on hybrid systems.In this thesis, we focus on modeling, simulation, and formal verification of hybrid systems. Current approaches available for verification of hybrid systems are unable to overcome the state-explosion problem. Usually, software tools for verification cannot give proper conclusions when we consider large-scale systems. Therefore, the correctness and safety for the corresponding models are undecid-able, the influences of theories and methods proposed from the area of hybrid systems are rather limited for industrial applications. In order to integrate exist-ing simulation and verification techniques, we propose a co-verification approach for hybrid systems. The advantage of simulation is the capability of analyzing large-scale systems. Based on the feedback of simulation we can abstract models of hybrid systems for verification, then utilize the advantages of verification on the checking of abstract models to guarantee correctness and safety for hybrid systems. Meanwhile, based on the feedback of verification, we can optimize the model for simulation and make simulation be more effective. Therefore, an efficient and reli-able procedure for the design and development of hybrid systems can be developed based on mutual feedbacks between formal verification and simulation.In addition, modeling languages for hybrid systems are also important to the widespread application of formal methods in industry. A well-structured and con-venient modeling language is easier to be accepted by designers or developers, then allowed to be applied broadly in industry. The hybrid modeling language HML which was recently proposed by Prof. HE Jifeng, is well-designed and its syntax is easier to be implemented and used for modeling hybrid systems. More-over, HML has good extensibility that is suitable for designers and developers in practical applications. In this thesis, we present inference rules in the style of Hoare triples for the formal verification of HML models. We also translate HML models into SMT (Satisfiability Modulo Theories) formulas that can be analyzed based on constraint-solving techniques, which brings about a prototype tool for the simulation and automated verification for hybrid systems.The contributions of this thesis can be summarized as follows:·Methodological ContributionWe present a feedback-advancement method for design and analysis of hybrid systems based on the analysis for advantages and disadvantages of simulation and formal verification techniques. We are able to analyze large-scale com-plex systems through simulation, but simulation is failed to cover all possible states or execution paths of a system. As a result, simulation is error-prone and always keep mistakes or bugs in the model, which brings potential risks into industrial activities and poses threats for public safety. In contrast, for-mal verification is capable of checking all possible states of a system, thus it can be used to guarantee the correctness and safety. Unfortunately, for-mal verification is unable to analyze large-scale complex systems effectively. Therefore, it is necessary to combine simulation and formal verification for the analysis of hybrid systems. Our feedback-advancement method takes the advantages of simulation and verification adequately, and also achieves com-plementation of these two techniques. As a result, the method is capable of achieving reliable design and development for large-scale complex systems based on feedbacks between simulation and verification.· Theoretic ContributionIn hybrid relation theory, the behavior of a hybrid system is expressed with constraints for three execution statuses:the constraint before the behavior starts, the constraint during its execution, and the constraint when the be- havior terminates, respectively. Inspired by the basic idea of hybrid relation theory, we integrate Hoare logic with hybrid relations, which results in a set of new inference rules for HML models. The new inference rules are inde-pendent of specific solving techniques for equations or invariants with respect to previous works. In our inference system, the inference rules constitute a framework for verification. It is free to choose established techniques when we have to deal with differential equations during the verification. The sepa-ration of mathematical solving techniques from inference rules simplifies the complexity of the rules without losing the extendibility of the framework, and we can just focus on the structures of models and the logical parts of the verification for the system behaviors.· Practical ContributionThis thesis contains plentiful case studies on hybrid systems, for instance, platform screen doors system, collision-avoidance control, and inverted pen-dulum. These case studies are used to examine theories and methods pre-sented in this thesis, meanwhile exemplify the feasibility and effectiveness. Moreover, we propose an approach for the translation of HML models to SMT formulas following the basic ideas of hybrid relation theory. Also, we develop a prototype tool for simulation and automated verification of HML models based on an SMT solver dReal, which builds a solid foundation for our future work on the development and verification of hybrid systems.