Cyber-physical Systems (CPS): Internet of Things (IoT), Fog Computing, Autonomous Vehicles, Human-Machine Collaboration, Medical Devices and Smart Grids
Formal Methods: SMT, Reachability Analysis, Model Checking, Temporal Logic, Automata Theory
Control Theory: Lyapunov Stability, Input-to-Output Stability, Correct-by-Construction Controller Synthesis
System Analysis: Safety, Security, Robustness and Resilience Analysis
Big Data Analytics: Machine learning, AI, Data-driven control and verification, Interpretable Machine Learning
Reachability analysis is a process of computing the set of states that a system can reach from an initial region. A system is safe when the set of its reachable states does not intersect with the unsafe region in the state-space. Thus, reachability analysis has become an essential technique for ensuring the safety of emerging systems like CPSs. However, computing the reachable states of CPSs is a very difficult problem, as these systems are most often nonlinear, and their state-space is uncountably infinite...
Close Loop Verification of Implantable Cardiac Devices
The main project objective is to develop a framework for the formal verification of ICD control software. Several goals have been outlined to meet this objective: (1) identify clinical data sets that provide adjudicated signals (i.e. identification of arrhythmia onset and classification by a physician) and that are compatible with the ICD control software; (2) develop numerical simulations that provide a method of generating self-adjudicated signals compatible with the ICD control software; (3) develop an ICD control-software model based on key temporal and frequency signal properties to perform arrhythmia detection and classification (e.g. VT/supra vs. VT/VF in the ventricle); and (4) apply verification techniques to the ICD model such as open-loop sensitivity analysis and closed-loop specificity analysis that will quantitatively assess rates of inappropriate ICD shocking...
An Implantable Cardioverter Defibrillator (ICD) is a medical device used for the detection of potentially fatal cardiac arrhythmias and their treatment through the delivery of electrical shocks intended to restore normal heart rhythm. ICD software features a number of programmable parameters, that, if wrongly configured, can result in unnecessary therapy, which are painful, and damage the cardiac tissue, and even worse can prevent required therapy, leading to sudden cardiac death. An ICD reprogramming attack is one that alters the device’s parameters to induce miss-classification and inappropriate therapy...
Simplex for CPS
Simplex is highly reliable and dependable software architecture for process control system. The architecture, illustrated in the figure below, consists of two versions of a controller, called the advanced controller (AC) and baseline controller (BC), sometimes known as recovery controller, and a physical plant. The advanced controller is designed for high performance and is in control of the plant in normal operating conditions. However, certification that AC keeps the plant state within a prescribed safety region may be infeasible, due to its complexity or, because an accurate model of it is unavailable for analysis. In contrast, the baseline controller is certified...