SHF: Small: Collaborative Research: Statistical Techniques for Verifying Temporal Properties of Embedded and Mixed-Signal Systems

University Of Colorado At Boulder, Boulder CO

Investigators

Abstract

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.