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

Project: Research project

Project Details


Verifying temporal properties of non-linear hybrid systems is currently one of the hardest challenges in verication research. Yet, common examples of non-linear models arising from mixed-signal systems, and embedded control systems are non-linear and complex. In practice, these systems are \veried" by exhaustive simulation, guided by coverage metrics such as node, branch and modied condition/decision (MC/DC) coverages. 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 failure. We propose to investigate verication techniques for embedded and mixed-signal systems based on rare event simulations. Rare event simulations have been used successfully in areas such as mathematical nance, reliability theory and queuing theory for analyzing events in stochastic models with vanishing probabilities, typically 10..7 or lower. The proposed work will adapt ideas from rare event simulations to formulate approaches for nding bugs (property violations) in non-linear hybrid systems, as well as estimating aggregate system properties such as throughput, response time and delays without bias and with high condence [93]. Likewise, ideas from extreme value theory [18] can be used to provide worst-case estimates of quantities such as delays, response times, throughput and variable ranges. Applying these ideas to verication requires us to revisit fundamental denitions of concepts such as the semantics of temporal logics. Therefore, we will investigate metric semantics of temporal logics that generalize the standard true=false interpretation of these formulas over simulation traces. Furthermore, existing metric semantics for continuous traces are computationally expensive. The proposed work will investigate eciently computable metrics for discrete, continuous and hybrid system traces for guiding the simulation process [19]. } .
Effective start/end date8/1/107/31/13


  • National Science Foundation (NSF): $239,319.00

Fingerprint Explore the research topics touched on by this project. These labels are generated based on the underlying awards/grants. Together they form a unique fingerprint.