Online Modeling And Verification Of Dynamic Behavior For Cyber- Physical Systems

In Safety-Critical field, such as train control, aviation, aerospace and medical treatment, Cyber-Physical Systems have high quality safety requirement. While Test and Simulation are not able to ensure that systems have no error, how to guarantee systems security by using formal modeling and verification is a focus problem in the related field.In the dynamic real-time Cyber-Physical Systems, there are large number of real-time parameters, so it is difficult to describe state space. Traditional static model check-ing becomes very hard in this situation. To solve the problem, related scholars proposed Online Verification. When systems are on running-time, parameters are constantly up-dated and also available, it makes use of the feature to build model and do verification periodically aimed at a short period of systems behavior.While, by some experiments on the train control system, which is a typical Cyber-Physical System, this paper find that there are two problems in the actual application of online verification. On the one hand, traditional assembly-line online verification design can not completely cover the cycles of systems, at the same time it does not consider the timeliness problem. On the other hand, the computing power of actual equipments onboard is limited, meanwhile some aspects like multi trains and multi tasks bring efficiency problem. In order to solve the above two problems, to guarantee the reliability and the efficiency of the online verification, this paper do the following work:1. We propose a multi-trigger online modeling and verification method of com-plete cycles for Cyber-Physical Systems. We take train control system as example, analyze the verification coverage problem and the timeliness problem. Then discuss several important parameters of online verification and put forward a series of rules which should meet in the design process. After theoretical analysis of the rules, pro-pose the multi-trigger online modeling and verification method under the guide of the rules. Moreover, this paper design three scenes to show the necessity and correctness of the method.2. We propose a distributed online verification framework. By analyzing of the Linux Virtual Server technology, propose a distributed online verification framework combining the characteristics of online verification itself. The framework considers s-calability, reliability, and transparency. It contains configuration module, load schedul-ing module, background calculation module and shared storage area. Based on the framework, this paper make a implement on the cloud platform and conduct some effi-ciency experiments on the platform.3. Cooperating with Beijing Jiaotong University, we design and implement the online verification module on the national engineering center of rail transportation op-eration control system of CBTC simulation platform. Through analyzing mechanism of Yizhuang line, build formalized model. Then unify interface of equipments onboard and do a series of processing like zone translation and curves calculation to the parame-ters. Moveover, construct a periodical verification background packaged by packaging the verification tool SpaceEx. After deploying the verification module on the console of simulation platform, design a scene to show the validation of the online verification module.