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.