Demo Abstract: BACHOL - Modeling and Verification of Cyber-Physical Systems Online

As most of the CPS systems are working in open environment, many control parameters used in the systems are generated online. The exact values of these parameters are unpredictable offline in advance. This causes the behavior of the CPS model has high nondeterminism and can not be verified by model checking in the design phase. To overcome this problem, we proposed that the modeling and verification of CPS system should be conducted online and focus on the system´s time-bounded behavior in short-run future. In this demo, we present a tool BACHOL which can handle the online modeling and verification of parametric linear hybrid automata. We use a simulation of a state-of-the-art train control system to show how BACHOL can be deployed online to predict error before it happen, and strengthen the reliability of the system.