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

嵌入式控制、混合信号系统等非线性混合系统的时序特性是当前验证研究的难点之一。在实践中，这些系统使用模拟进行“验证”。然而，广泛的模拟是众所周知的，是不足以保证安全。有害的缺陷往往未被发现。这些缺陷可能会在部署过程中表现为具有微小但非零发生机会的罕见事件。本项目研究基于罕见事件模拟的嵌入式和混合信号系统的随机验证技术。稀有事件模拟已经成功地应用于金融数学、可靠性理论和排队论等领域，用于分析具有消失概率的随机模型中的事件。这项工作采用了稀有事件模拟和极值理论的思想来检测非线性混合系统中的属性侵犯。此外，我们的研究重温基本概念，如布尔语义的时间逻辑。它研究了时态逻辑的实值度量语义，将标准的真假解释推广到仿真轨迹上，研究计划有望为验证嵌入式和混合信号系统提供有用的工具。这些工具可以很容易地集成到基于模型的开发环境中。因此，正在研究的技术将直接适用于嵌入式控制和混合信号系统，以提高设计的可靠性。此外，研究成果被列入课程课程集中在半正式测试技术的应用，以各种软件/硬件工程应用的本科生以及研究生。

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.