A HybridUML and QdL Based Verification Method for CPS Self-Adaptability

摘要

CPS (Cyber-Physical Systems) are physical and engineered systems featuring a tight combination of computation and physical processes by communication networks. CPS are mainly applied in some critical domains, so it is very essential to ensure the correctness of CPS. Formal verification has been successfully applied in the correctness verification of CPS; however, the high theoretical level of formal modeling techniques of formal verification and the lack of visualization of formal models make it difficult to integrate formal verification with enterprise standard system development process. In this paper, we model CPS by HybridUML, an extension of UML, and then transform HybridUML model into the input language of theorem prover KeYmaera-QHP (Quantified Hybrid Program), and finally verify the QHP code with KeYmaera.