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

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

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