Incremental Online Verification Of Dynamic Cyber-Physical Systems

Periodically online verification has been widely recognized as a practical and promising method to handle the non-deterministic and unpredictable behavior of dynamic CPS systems. However, it is a challenge to keep the online verification of CPS systems finishing quickly in time to give enough time for the running system to respond, if any error is detected. Nevertheless, the problems under verification for each cycle are highly similar to each other. Most of the differences are caused by run-time factors like changing of parameters' values or the reorganization of active components in the system. Under this investigation, this paper presents an incremental verification technique for online verification of CPS systems. A method is given to distinguish the differences between the problem under verification and the previous verified problem. Then, by reusing the problem space of the previous verified problem as a warm-start base, the modified part can be introduced into the base, which can be solved incrementally and efficiently. A set of case studies on a real-case train control system is presented in this paper to demonstrate the performance of the incremental online verification technique.