Modeling And Verification Of Safety-Critical Hybrid Systems

It is an important scientific problem that how to model and verify safety-critical hybrid systems.However,the actualities are as follows: there lacks a guide to obtain safety property;the popular formal language LUSTRE does not support modeling continuous behaviors;the high complexity of the system makes verifition impossible because of state explosion problem.These problems have made it difficult to develop safety-critical hybrid systems with higher security.This dissertation focuses on solving the problems above.The solution starts from analyzing requirements specification,and a normalize process is proposed for the purpose of formal verification.The main contributions of the dissertation are as follows:(1)A framework of modeling and verifying safety-critical hybrid systems is proposed.The framework takes a requirement as starting point,and covers the process of requirement modeling,requirement decomposing,design modeling,and verification implementation.It proposes a solution of obtaining the components that formal verification requires.(2)Two projection based decomposing methods for requirement problems are proposed.Both of them take the advantage of problem frames approach,and obtain projection dimension from sub-requirements or variable constraints.This results in decreasing the complexity of modeling safety-critical hybrid systems.(3)A hybrid modeling language Hybrid LUSTRE is defined.The language is based on synchronous modeling language LUSTRE and combines the time model of hybrid automata.The formal syntax and semantic are proposed,so that it can describe the continuous behaviors of physical world,and model hybrid systems.(4)A guide of verifying safety-critical hybrid system is proposed.The guide takes the advantage of the framework,and optimizes it to make the verification more efficient.The methods proposed in this dissertation have been successfully used in a real industrial application of train control system,and make the modeling and verification very successful.Following the framework can decrease the time cost of verification about 20%,and increase the scale of the systems that can be verified.The application is the first time that the safety-critical module of a project level Zone Controller being verified.