TY - GEN
T1 - Incremental Online Verification of Dynamic Cyber-Physical Systems
AU - Bu, Lei
AU - Xing, Shaopeng
AU - Ren, Xinyue
AU - Yang, Yang
AU - Wang, Qixin
AU - Li, Xuandong
PY - 2019/5/14
Y1 - 2019/5/14
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85066610296&partnerID=8YFLogxK
U2 - 10.23919/DATE.2019.8715003
DO - 10.23919/DATE.2019.8715003
M3 - Conference article published in proceeding or book
AN - SCOPUS:85066610296
T3 - Proceedings of the 2019 Design, Automation and Test in Europe Conference and Exhibition, DATE 2019
SP - 782
EP - 787
BT - Proceedings of the 2019 Design, Automation and Test in Europe Conference and Exhibition, DATE 2019
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 22nd Design, Automation and Test in Europe Conference and Exhibition, DATE 2019
Y2 - 25 March 2019 through 29 March 2019
ER -