Research On Cyber/Physical Co-Verification For CPS

Cyber-Physical Systems(CPS) tightly integrate computation and physical processes and transcend embedded system and control domains. Physical processes, usually with feedback loops, affect computations and vice versa. The cyber and physical components of CPS cooperatively deliver system functionalities and jointly contribute to properties. CPS engineering must account for the interacting and interdependent behaviors of both types of components to provide system-level property guarantees. Representative application domains of CPS include transportations, avionics, aerospace, intelligent power grid, automobiles, medical devices and other critical infrastructures.CPS are pervasive and often safety-critical, therefore, they must be highly assured. High-assurance CPS require extensive verification. Due to the inherent and ever-growing complexities, uncertain delay and the requirment of precise control, Cyber/Physical co-verification becomes more complicated. Long-term seperation research on the co-verfication has been considered as an obstacle to the development of high-assurance CPS. There is no unifying formal model for representing the implementation semantic of Cyber/Physical interface accurately. So a comprehensive co-verification framework for hierarchical verification of implementation level CPS is becoming an important issue in CPS verification theory.This dissertation proposes an approach for Cyber/Physcial co-verification. Based on the satellite attitude control system, the CPS which tightly intergate application software, execution platform and physical system is studied in detail. First, we studied the interaction mechanism between computation and physical processes. We further classify the interaction mechanism into two levels: logic interaction level and physical interaction level. The interaction between the physical system being controlled and the software implementation of control algorithms forms the logic level interaction. Accordingly, the interaction, which application software interact with physical system through execution platform, forms the physical level interaction. Secondly, we designed a co-verification model to capture computation and physical processes, as well as their concurrent executions and interactions. Thirdly, an approach is presented to Cyber/Physical co-verification using co-simulation in physcial level and formal co-verification in logic level. And we propose semi-formal verification approach based on the integration of co-simulation and formal co-verification. Finally, we have realized this approach and applied it to Table Sat which emulates in 1-degree-of-freedom the dynamics, sensing, and actuation capabilities required for satellite attitude control.The Cyber/Physcial co-verification theory is deeply studied in this dissertation, which includes the following contributions:(1) A Cyber/Physical interface model for hierarchical a verification of CPS is proposed. We define different types of interface model according to acombinatorial relationships of the A/D(Analog to Digital) and D/A(Digital to Analog) conversion periodical instants. We advocate the use of Cyber/Physical interface model for bridging multiple semantic gap between the two domains. This interface model have formal semantics, and is effecient for simulation and formal verification, and cover all Cyber/Physical behaviors described by Cyber/Physical interface model.(2) In the co-verification framework, we propose an approach to bounded model checking of Linear Temporal Logic(LTL) properties of Hybrid Automata Pushdown System(HAPS) over finite traces. Such HAPS models are suitable formal representations for Cyber/Physical co-verification, verifying software controller with controlled plant together. The core contribution is our process for constructing a HAPS by synchronizing a pushdown system that abstracts software and a hybrid automata that abstracts plant. We convert the LTL formula into a C language program, which is interleaved with the execution of the HAPS under analysis. Our approach checks both safety and liveness properties uniformly within the framework of bounded model checking through symbolic execution. We have realized this approach and applied it to several control systems. Experimental evaluation of effectiveness and efficiency is made on the approach.(3) In the co-verification framework, we propose a CPS virtualization approach based on the integration of virtual machine and physical model emulator. It enables real software, virtual hardware, and physical model to execute in a holistic virtual execution environment. To achieve high-fidelity between the real system and its virtualization, we have developed a strategy based on clock theory for synchronizing the virtual machine and the physical model emulator. To evaluate our approach, we have successfully applied it to real-world control systems. Experiments results have shown that our approach achieves high-fidelity in capturing dynamic behaviors of the entire system. This approach is promising in enabling early development of cyber components of CPS and early exploration of the synergy of cyber and physical components.(4) We propose a semi-formal verification approach based on the integration of co-simulation and formal co-verification. We analyze these simulation traces, find some critical states and assisted with formal verification under these circumstances. This online-capture offline-replay approach combines the benefits of going deeper and expore exhaustively the state space of the system. The semi-formal verification approach can be used to overcome the drawbacks of both co-simulation and formal co-verification. We have validated our approach by applying it to Table Sat. It combines advantages of formal verification and simulation. The experiment results show that our approach has major potential in verifying system level properties of complex CPS, therefore improving the high-assurance of CPS.