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

SHF：小型：协作研究：验证嵌入式和混合信号系统时间特性的统计技术

• 批准号: 1016994
• 负责人: Sriram Sankaranarayanan
• 金额: $ 24.96万
• 依托单位: University of Colorado at Boulder
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2010
• 资助国家: 美国
• 起止时间: 2010-08-01 至 2014-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1016994&HistoricalAwards=false
• 关键词: SHF; Small; Collaborative; Research; Statistical

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.

验证嵌入式控制和混合信号系统等非线性混合系统的时间特性是目前验证研究中最困难的挑战之一。在实践中，这些系统通过模拟“验证”。然而，广泛的模拟并不足以保证安全。有害的缺陷通常不会被发现。这些缺陷可能在部署期间表现为很少发生的事件，发生的几率很小，但不是零。本项目研究基于罕见事件模拟的嵌入式和混合信号系统的随机验证技术。罕见事件模拟已成功地应用于数学金融、可靠性理论和排队论等领域，用于分析具有消失概率的随机模型中的事件。本文采用罕见事件模拟和极值理论的思想来检测非线性混合系统的属性违逆。此外，我们的研究回顾了基本概念，如时间逻辑的布尔语义。研究了时间逻辑的实值度量语义，推广了仿真轨迹上的标准真假解释。该研究计划有望为验证嵌入式和混合信号系统提供有用的工具。这些工具可以很容易地集成到基于模型的开发环境中。因此，正在研究的技术将直接适用于嵌入式控制和混合信号系统，以提高设计的可靠性。此外，研究成果被包括在以半正式测试技术应用于各种软件/硬件工程应用为中心的课程课程中，面向本科生和研究生。