Safety-critical decision-making often necessitates operating within complex and uncertain environments, typically characterized as partially-observable Multi-Agent Systems (MAS). Effective decision-making in these settings demands a profound understanding of the environment and accurate representation and quantification of epistemic uncertainty due to informational deficits. This uncertainty representation must reflect prior knowledge and dynamically integrate observational data. While Version Space Learning (VSL) offers a framework for set-based uncertainty representation, prior methods often depend on under-approximation of the actual version space, which falls short in safety-critical applications. We introduce a model checking-based VSL framework to enhance uncertainty representation and context-awareness in such applications. Our approach employs network of timed automata (NTA) to model the MAS environment, capturing its mechanisms and prior knowledge efficiently. The inherent non-determinism of timed automata facilitates an over-approximation of the actual version space, ensuring all plausible hypotheses are considered. We further refine the parameter ranges of the NTA using proof traces, optimizing the use of observational data. In a medical diagnosis case study, our framework identified a missing rule in a traditional rule-based system and provided interpretable and scalable results, demonstrating our method’s ability to improve decision-making accuracy and manage complex scenarios effectively.

The increasing demands for system complexity and robustness have prompted the integration of temporal logic into Multi-Agent Reinforcement Learning (MARL) to address tasks with non-Markovian properties. However, incorporating non-Markovian properties introduces additional computational complexities, as agents are required to integrate historical data into their decision-making process. Also, optimizing strategies within a multi-agent environment presents significant challenges due to the exponential growth of the state space with the number of agents. In this study, we introduce an innovative hierarchical MARL framework that synthesizes temporal equilibrium strategies through parity games and subsequently encodes them as individual reward machines for MARL coordination. More specifically, we reduce the strategy synthesis problem into an emptiness problem concerning parity games with optimized states and transitions. Following this synthesis step, the temporal equilibrium strategy is decomposed into individual reward machines for decentralized MARL. Theoretical proofs are provided to verify the consistency of the Nash equilibrium between the parallel composition of decomposed strategies and the original strategy. Empirical evidence confirms the efficacy of the proposed synthesis technique, showcasing its ability to reduce state space compared to the state-of-the-art tool. Furthermore, our study highlights the superior performance of the distributed MARL paradigm over centralized approaches when deploying decomposed strategies.

As autonomous vehicles (AVs) become more common on public roads, their interaction with human-driven vehicles (HVs) in mixed traffic is inevitable. This requires new control strategies for AVs to handle the unpredictable nature of HVs. This study focused on safe control in mixed-vehicle platoons consisting of both AVs and HVs, particularly during longitudinal car-following scenarios. We introduce a novel model that combines a conventional first-principles model with a Gaussian process (GP) machine learning-based model to better predict HV behavior. Our results showed a significant improvement in predicting HV speed, with a 35.64% reduction in the root mean square error compared with the use of the first-principles model alone. We developed a new control strategy called GP-MPC, which uses the proposed HV model for safer distance management between vehicles in the mixed platoon. The GP-MPC strategy effectively utilizes the capacity of the GP model to assess uncertainties, thereby significantly enhancing safety in challenging traffic scenarios, such as emergency braking scenarios. In simulations, the GP-MPC strategy outperformed the baseline MPC method, offering better safety and more efficient vehicle movement in mixed traffic.

Driving is a social activity which involves endless interactions with other agents on the road. Failing to locate these agents and predict their possible future actions may result in serious safety hazards. Traditionally, the responsibility for avoiding these safety hazards is solely on the drivers. With improved sensor quantity and quality, modern ADAS systems are able to accurately perceive the location and speed of other nearby vehicles and warn the driver about potential safety hazards. However, accurately predicting the behavior of a driver remains a challenging problem. In this paper, we propose a framework in which behavioral models of drivers (Digital Behavioral Twins) are shared among connected cars to predict potential future actions of neighboring vehicles, therefore improving the safety of driving. We provide mathematical formulations of models of driver behavior and the environment, and discuss challenging problems during model construction and risk analysis. We also demonstrate that our digital twins framework can accurately predict driver behaviors and effectively prevent collisions using a case study in a virtual driving simulation environment.

In this paper, we survey recent progress in CyberCardia project, a CPS Frontier project funded by the National Science Foundation. The CyberCardia project will lead to significant advances in the state of the art for system verification and cardiac therapies based on the use of formal methods and closed-loop control and verification. The animating vision for the work is to enable the development of a true in silico design methodology for medical devices that can be used to speed the development of new devices and to provide greater assurance that their behavior matches designer intentions, and to pass regulatory muster more quickly so that they can be used on patients needing their care. The acceleration in medical-device innovation achievable as a result of the CyberCardia research will also have long-term and sustained societal benefits, as better diagnostic and therapeutic technologies enter into the practice of medicine more quickly.

Ventricular Fibrillation is a disorganized electrical excitation of the heart that results in inadequate blood flow to the body. It usually ends in death within a minute. A common way to treat the symptoms of fibrillation is to implant a medical device, known as an Implantable Cardioverter Defibrillator (ICD), in the patient's body. Model-based verification can supply rigorous proofs of safety and efficacy. In this paper, we build a hybrid system model of the human heart+ICD closed loop, and show it to be a STORMED system, a class of o-minimal hybrid systems that admit finite bisimulations. In general, it may not be possible to compute the bisimulation. We show that approximate reachability can yield a finite simulation for STORMED systems, and that certain compositions respect the STORMED property. The results of this paper are theoretical and motivate the creation of concrete model checking procedures for STORMED systems.

Software-based control of life-critical embedded systems has become increasingly complex, and to a large extent has come to determine the safety of the human being. For example, implantable cardiac pacemakers have over 80,000 lines of code which are responsible for maintaining the heart within safe operating limits. As firmware-related recalls accounted for over 41% of the 600,000 devices recalled in the last decade, there is a need for rigorous model-driven design tools to generate verified code from verified software models. To this effect, we have developed the UPP2SF model-translation tool, which facilitates automatic conversion of verified models (in UPPAAL) to models that may be simulated and tested (in Simulink/Stateflow). We describe the translation rules that ensure correct model conversion, applicable to a large class of models. We demonstrate how UPP2SF is used in the model-driven design of a pacemaker whose model is (a) designed and verified in UPPAAL (using timed automata), (b) automatically translated to Stateflow for simulation-based testing, and then (c) automatically generated into modular code for hardware-level integration testing of timing-related errors. In addition, we show how UPP2SF may be used for worst-case execution time estimation early in the design stage. Using UPP2SF, we demonstrate the value of integrated end-to-end modeling, verification, code-generation and testing process for complex software-controlled embedded systems.

Model-Driven Design (MDD) of cyber-physical systems advocates for design procedures that start with formal modeling of the real-time system, followed by the model's verification at an early stage. The verified model must then be translated to a more detailed model for simulation-based testing and finally translated into executable code in a physical implementation. As later stages build on the same core model, it is essential that models used earlier in the pipeline are valid approximations of the more detailed models developed downstream. The focus of this effort is on the design and development of a model translation tool, UPP2SF, and how it integrates system modeling, verification, model-based WCET analysis, simulation, code generation and testing into an MDD based framework. UPP2SF facilitates automatic conversion of verified timed automata-based models (in UPPAAL) to models that may be simulated and tested (in Simulink/State flow). We describe the design rules to ensure the conversion is correct, efficient and applicable to a large class of models. We show how the tool enables MDD of an implantable cardiac pacemaker. We demonstrate that UPP2SF preserves behaviors of the pacemaker model from UPPAAL to State flow. The resultant State flow chart is automatically converted into C and tested on a hardware platform for a set of requirements.

The design of bug-free and safe medical device software is challenging, especially in complex implantable devices that control and actuate organs in unanticipated contexts. Safety recalls of pacemakers and implantable cardioverter defibrillators between 1990 and 2000 affected over 600 000 devices. Of these, 200 000 or 41% were due to firmware issues and their effect continues to increase in frequency. There is currently no formal methodology or open experimental platform to test and verify the correct operation of medical device software within the closed-loop context of the patient. To this effect, a real-time virtual heart model (VHM) has been developed to model the electrophysiological operation of the functioning and malfunctioning (i.e., during arrhythmia) heart. By extracting the timing properties of the heart and pacemaker device, we present a methodology to construct a timed-automata model for functional and formal testing and verification of the closed-loop system. The VHM's capability of generating clinically relevant response has been validated for a variety of common arrhythmias. Based on a set of requirements, we describe a closed-loop testing environment that allows for interactive and physiologically relevant model-based test generation for basic pacemaker device operations such as maintaining the heart rate, atrial-ventricle synchrony, and complex conditions such as pacemaker-mediated tachycardia. This system is a step toward a testing and verification approach for medical cyber-physical systems with the patient in the loop.

Designing bug-free medical device software is challenging, especially in complex implantable devices that may be used in unanticipated contexts. Safety recalls of pacemakers and implantable cardioverter defibrillators due to firmware problems between 1990 and 2000 affected over 200, 000 devices. This encompasses 41% of the devices recalled and continues to increase in frequency. There is currently no formal methodology or open experimental platform to validate and verify the correct operation of medical device software. To this effect, a real-time Virtual Heart Model (VHM) has been developed to model the electrophysiological operation of the functioning (i.e. during normal sinus rhythm) and malfunctioning (i.e. during arrhythmia) heart. We present a methodology to construct a timed-automata model by extracting timing properties of the heart. The platform employs functional and formal interfaces for validation and verification of implantable cardiac devices. We demonstrate the VHM is capable of generating clinically-relevant response to intrinsic (i.e. premature stimuli) and external (i.e. artificial pacemaker) signals for a variety of common arrhythmias. By connecting the VHM with a pacemaker model, we are able to pace and synchronize the heart during the onset of irregular heart rhythms. The VHM has also been implemented on a hardware platform for closed-loop experimentation with existing and virtual medical devices. This integrated functional and formal device design approach has potential to help expedite medical device certification for safe operation.

Designing bug-free medical device software is difficult, especially in complex implantable devices that may be used in unanticipated contexts. In the 20-year period from 1985 to 2005, the US Food and Drug Administration's (FDA) Maude database records almost 30,000 deaths and almost 600,000 injuries from device failures [8]. There is currently no formal methodology or open experimental platform to validate and verify the correct operation of medical device software. To this effect, a real-time Virtual Heart Model (VHM) has been developed to model the electrophysiological operation of the functioning (i.e. during normal sinus rhythm) and malfunctioning (i.e. during arrhythmia) heart. We present a methodology to extract timing properties of the heart to construct a timed-automata model. The platform exposes functional and formal interfaces for validation and verification of implantable cardiac devices. We demonstrate the VHM is capable of generating clinically-relevant response to intrinsic (i.e. premature stimuli) and external (i.e. artificial pacemaker) signals for a variety of common arrhythmias. By connecting the VHM with a pacemaker model, we are able to pace and synchronize the heart during the onset of irregular heart rhythms. The VHM has been implemented on a hardware platform for closed-loop experimentation with existing and virtual medical devices. The VHM allows for exploratory electrophysiology studies for physicians to evaluate their diagnosis and determine the appropriate device therapy. This integrated functional and formal device design approach will potentially help expedite medical device certification for safer operation.