PECASE: Formal Analysis and Validation of Probabilistic Guarantees on QoS and other Power/Performance Characteristics in Embedded Systems Design

PECASE：嵌入式系统设计中 QoS 和其他功耗/性能特征的概率保证的形式分析和验证

• 批准号: 0237947
• 负责人: Sandeep Shukla
• 金额: --
• 依托单位: Virginia Polytechnic Institute and State University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2003
• 资助国家: 美国
• 起止时间: 2003-01-15 至 2009-12-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0237947&HistoricalAwards=false
• 关键词: PECASE; Formal; Analysis; Validation; Probabilistic

Proposal Title: PECASE: Formal Analysis and Validation of Probabilistic Guarantees on QoS and other Power/Performance Characteristics in Embedded Systems DesignInstitution: Virginia Polytechnic Institute and State UniversityAs micro-electronic and micro-computing advances proliferate to a large class of information technology appliances, there are two trends dominating the current generation of applications and capabilities. The first trend is increasing use of software in a large number of appliances that imparts intelligent processing and decision making to manage device response and its interaction with the user and the environment. The second trend is increased networking of this "embedded intelligence" (also called ambient intelligence in Europe) due to advances in communication and on-chip networking capabilities. Computing in such systems is increasingly application-oriented and must be responsive to the environment in which the device will be placed from hand-held, personal spaces to the human body. This portability of embedded computing places extreme demands on the ability of the system architectures to tolerate varying energy source conditions, communication channel conditions, network conditions, etc. Yet, there is also an increasing need for the application to be predictable on various measures including performance, energy and power consumption and other QoS (Quality of Service) properties. System availability and performance reliability are also extremely important as these systems interact with real world processes and their unavailability may lead to adverse or even disastrous consequences. This research addresses some of the important challenges in the management of the power, energy and performance of embedded computing and networked devices in ways that allows us to develop close bounds on the quality of results achieved. This project is developing fundamental technical advances in the state of the art in dynamic power management (DPM) (at both hardware and software levels), and other types of QoS predictability by employing techniques from formal verification, probabilistic modeling and model checking, and cooperative game theory. The educational part of this project aims at building embedded systems engineering as a sub-discipline of Computer Engineering at Virginia Tech, as well as on popularizing the research results through demonstration of the techniques to more tangible engineering examples. For example, the tools developed may be used for high-way traffic modeling, analysis and controller synthesis for traffic maintenance. Such demonstrations (with appropriate animation) are being developed to illustrate the power of formal and mathematical modeling of complex systems to K12 level students and attract them to engineering. In this project techniques for analysis of strategies and protocols employed in embedded computing systems for resource management are being investigated. The tools being developed will allow formal validation of probabilistic guarantees on performance, energy expenditure and QoS. The project also applies existing tools (whenever possible) for formal analysis to achieve the goals of predictability of such measures. In particular, the following types of questions are being dealt with. (a) How to analyze and compare power/performance characteristics of multiple competing strategies without having to resort to expensive simulation based methods? (b) How to formally verify probabilistically quantified guarantees on the measures of interest? (c) How to guide designers of embedded system in choosing between alternative possible strategies to achieve some performance goals? (d) How to formally analyze network protocols, using energy models of the

提案标题：PECASE：嵌入式系统设计中对服务质量和其他功率/性能特性概率保证的形式分析和验证机构：弗吉尼亚理工学院和州立大学随着微电子和微计算的进步激增到一大类信息技术设备，有两种趋势主导着当前一代应用程序和功能。第一个趋势是在大量设备中越来越多地使用软件，这些软件赋予智能处理和决策以管理设备响应及其与用户和环境的交互。第二个趋势是，由于通信和芯片联网能力的进步，这种“嵌入式智能”(在欧洲也称为环境智能)的联网增加。这种系统中的计算越来越面向应用，并且必须对设备将从手持个人空间放置到人体的环境做出响应。嵌入式计算的这种可移植性对系统体系结构容忍变化的能源条件、通信信道条件、网络条件等的能力提出了极端要求。然而，也越来越需要应用程序在包括性能、能量和功率消耗以及其他服务质量(Quality Of Service)属性的各种度量上是可预测的。系统可用性和性能可靠性也非常重要，因为这些系统与现实世界的流程交互，它们的不可用可能会导致不利的甚至灾难性的后果。这项研究解决了嵌入式计算和网络设备的电源、能源和性能管理中的一些重要挑战，使我们能够对所取得的结果的质量进行严格的限制。该项目通过使用形式验证、概率建模和模型检验以及合作博弈论的技术，在动态功率管理(DPM)(硬件和软件级别)和其他类型的服务质量可预测性方面发展最先进的技术进步。该项目的教育部分旨在将嵌入式系统工程作为弗吉尼亚理工大学计算机工程的一个子学科，并通过向更多有形的工程实例演示技术来普及研究成果。例如，开发的工具可用于高速公路交通建模、分析和控制器综合，以进行交通维护。这样的演示(用适当的动画)是为了向K12水平的学生说明复杂系统的形式和数学建模的力量，并吸引他们学习工程学。在本项目中，正在研究用于分析嵌入式计算系统中用于资源管理的策略和协议的技术。正在开发的工具将允许对性能、能源消耗和服务质量的概率保证进行正式验证。该项目还(尽可能)使用现有工具进行正式分析，以实现这类措施的可预测性目标。特别是，正在处理以下类型的问题。(A)如何在不必诉诸昂贵的基于模拟的方法的情况下分析和比较多种竞争战略的功率/性能特征？(B)如何正式核实对利息计量的概率量化担保？(C)如何指导嵌入式系统的设计者在可选的策略中进行选择，以实现一些性能目标？(D)如何使用网络协议的能量模型形式化分析网络协议