Set-Based Assumption-Guarantee Reasoning for Handling Uncertainty in Functionality and Safety Verification of Dynamic Systems
摘要
The increasing complexity of Cyber-Physical Systems (CPSs), particularly in safety-critical applications, necessitates advanced methods for design and verification. Modern CPSs must operate reliably in uncertain environments characterized by noise, external disturbances, and dynamic conditions. Addressing these challenges requires methodologies that are capable of capturing both internal system complexities and external uncertainties. Assumption-Guarantee reasoning, often expressed using temporal logics, provides a modular framework for verification. However, current temporal logics are limited in their ability to effectively handle uncertainties. This paper introduces Set-Based Temporal Logic (SBTL) as a solution to these limitations by extending traditional contract specifications to incorporate a set-based reachability analysis, which enables a more detailed representation of uncertainty and accommodates for implicit system behaviors. By integrating set-based reasoning with temporal constraints, SBTL offers a more expressive and robust specification formalism. The approach is demonstrated through simulations of a DC motor-based drive train operating in an uncertain and dynamic environment, featuring a combined state and disturbance estimator. Results highlight the enhanced robustness of the closed-loop control system, ensuring consistent disturbance reconstruction and alignment of system trajectories with desired behavior.