Verification of Cyber-Physical Systems Based on Differential-Algebraic Temporal Dynamic Logic

摘要

Differential temporal dynamic logic (dTL) is an approach for specifying and verifying properties of cyber-physical systems (CPS) and it can handle with temporal behaviors for CPS. The hybrid programs (HP), as operating model of dTL, only contain differential equations that can be solved in polynomial arithmetic, which results that dTL can only specify and verify CPS of simple dynamics. However, differential-algebraic dynamic logic (DAL) solves the problem through the introduction of differential invariants, but lacks verification capabilities for properties with temporality. This paper combines the advantages of dTL and DAL, and proposes differential-algebraic temporal dynamic logic (DATL). We have achieved the following results: a trace semantics for differential-algebraic programs (DAP), four new rules based on the rules of dTL and DAL, a proof of the soundness of the new rules, and the specification and verification of safety of aircraft collision avoidance system with DATL. Our theory together with a case study demonstrates that DATL overcomes the constraints that differential equations must be solvable in polynomial arithmetic and can be used to specify and verify temporal properties of CPS.