Design, validation and verification of Hybrid Systems

Abstract

Model-based design of Cyber-physical Systems (CPSs) is a widely accepted technique that employs mathematical models in developing such systems and relies on co-simulation to understand their behavior. Co-simulation suffers from many problems, such as timing delays, skews, and race conditions. The TCP/IP-based (most commonly used) asynchronous network connection used for co-simulation makes it unsuitable for checking timing properties (written for validating controller behavior) of a CPS. In our approach to controller validation, we synthesize the controller and the plant in hardware. They are then executed synchronously on a robustly chosen lockstep, thus eliminating all the issues arising from asynchronous communication. Apart from asynchronous execution, the existing cosimulation frameworks are prone to miss level crossing detection. It is very dangerous from the aspect of safety-critical controllers. Our work provides a novel holistic Metric Interval Temporal Logic (MITL) based validation and Hardware in Loop (HIL) co-simulation framework for CPS, which handles communication delays, race conditions, skews, etc., and does level crossing detection as well. Benchmark results show that real-time MITL properties that are vacuously satisfied or violated due to co-simulation artifacts hold correctly in the proposed closed-loop validation framework. To reason about the timing correctness of any CPS model, its Worst Case Execution Time (WCET) analysis must be done. Using Linear Temporal Logic (LTL) to reason about the program’s correctness is ineffective as it does not focus on real-time reasoning for hybrid systems. In that regard, we propose real-time Hoare logic-based rules, which are based on the WCET of a system and its components. Then we do a synchronous composition of the component-level Hoare logic rule-based contracts to justify a system-level contract. This real-time contract composition and reasoning technique is the first-ever attempt in synchronous system design and verification. Overall contribution of our work solves many problems at different levels. The Hoare Logic contract-based real-time static reasoning framework helps to statically verify programs constituting a hybrid system. The hardware-software co-simulation framework helps effectively validate controller correctness while doing level-crossing detection. Finally, the solution in which the hybrid system model is realized in hardware fixes the issue of asynchronous communication.