Design, validation and verification of Hybrid Systems

Show simple item record

dc.contributor.advisor Malik, Avinash
dc.contributor.advisor Roop, Partha
dc.contributor.author Sood, Surinder
dc.date.accessioned 2023-11-15T23:36:51Z
dc.date.available 2023-11-15T23:36:51Z
dc.date.issued 2023 en
dc.identifier.uri https://hdl.handle.net/2292/66575
dc.description.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.
dc.publisher ResearchSpace@Auckland en
dc.relation.ispartof PhD Thesis - University of Auckland en
dc.rights Items in ResearchSpace are protected by copyright, with all rights reserved, unless otherwise indicated.
dc.rights.uri https://researchspace.auckland.ac.nz/docs/uoa-docs/rights.htm en
dc.rights.uri http://creativecommons.org/licenses/by-nc-sa/3.0/nz/
dc.title Design, validation and verification of Hybrid Systems
dc.type Thesis en
thesis.degree.grantor The University of Auckland en
thesis.degree.level Doctoral en
thesis.degree.name PhD en
dc.date.updated 2023-11-13T02:14:51Z
dc.rights.holder Copyright: The author en
dc.rights.accessrights http://purl.org/eprint/accessRights/OpenAccess en


Files in this item

Find Full text

This item appears in the following Collection(s)

Show simple item record

Share

Search ResearchSpace


Browse

Statistics