Verifying temporal properties of non-linear hybrid systems, such as embedded control and mixed-signal systems, is currently one of the hardest challenges in verification research. In practice, these systems are "verified" using simulations. Nevertheless, extensive simulation is well known to be inadequate for guaranteeing safety. Harmful defects often remain undetected. These defects may manifest themselves during deployment as rare events with a tiny, but non-zero chance of occurrence.
This project investigates stochastic verification techniques for embedded and mixed-signal systems based on rare event simulations. Rare event simulations have been used successfully in areas such as mathematical finance, reliability theory and queuing theory for analyzing events in stochastic models with vanishing probabilities. This work adapts ideas from rare event simulations and extreme value theory to detect property violations in non-linear hybrid systems. Furthermore, our research revisits fundamental concepts such as the Boolean semantics of temporal logics. It investigates real-valued metric semantics of temporal logics, which generalize the standard true-false interpretation over simulation traces.
The research program is expected to yield useful tools for verifying embedded and mixed-signal systems. These tools can be readily integrated inside model-based development environments. As a result, the techniques that are being investigated will be directly applicable to embedded control and mixed-signal systems to improve the reliability of the designs. Additionally, the research outcomes are being included in course curricula centered on the application of semi-formal testing techniques to various software/hardware engineering applications for undergraduate as well as graduate students.
Nowadays, embedded computing devices can be found in a variety of new systems that interact with the physical world. Automobiles, locomotives, aerospace systems, medical devices, manufacturing systems and robotics are all prime examples of such systems which are usually referred to as Cyber-Physical Systems (CPS). The benefits of embedding computational intelligence in our critical infrastructure and devices are overwhelming: improved levels of system efficiency, safety, cost reduction, customization and usability. However, smart devices are becoming a reality through complex software and hardware. As the embedded intelligence increases so does the complexity of the software/hardware. As the complexity of the software/hardware increases so do the design and programming errors. CPS pose an additional challenge over traditional software/hardware based systems. That is, humans cannot easily predict how the complex software/hardware interacts with the physical environment. In addition, the few existing methods that can automatically synthesize or analyze a CPS currently have only shown their value on academic problems and they do not scale to industrial size systems. The consequences are ominous. Both the automotive and the medical device industries issue multiple software/hardware-related recalls on a yearly basis. Many of these recalls can lead to life threatening situations. Examples range from cruise control systems that do not disengage under certain operating conditions to infusion pumps that may overdose patients. Our collaborative research with the University of Colorado at Boulder has developed an innovative testing and verification framework that specifically targets complex CPS. Our guiding principle is that safety critical systems must always be conforming to a set of formal correctness requirements on the function of the system. The elicitation of formal requirements can also assist on the early detection of conflicting functional requirements. The enabling theory for our verification framework is the notion of robustness of functional requirements that we have developed. The theory of robustness has enabled us to convert the verification problem into a minimization problem where we search for the least robust system behavior. The overview of our approach is presented in the accompanying figure. Our verification framework has been applied to a number of challenging problems from the automotive, medical device and mixed-signal industries. In collaboration with Toyota engineers, we demonstrated that our framework can detect design and tuning errors in challenge problems posed 10 years ago by Ford. Our work on medical pumps for insulin infusion has demonstrated the value of our approach on both analysis and synthesis of insulin infusion schedules for patients. The latter work also sets the foundations for personalized model-based diabetes management. Our tools are publicly available at the web-site https://sites.google.com/a/asu.edu/s-taliro/ under General Public License. Therefore, they can be directly utilized by other academic and industrial groups on a variety of different applications.
