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

提案标题：PECASE：嵌入式系统设计中QoS和其他功率/性能特性的概率保证的形式化分析和验证机构：弗吉尼亚理工学院和州立大学随着微电子和微计算技术的发展，信息技术设备的种类越来越多，有两种趋势主导着当前一代的应用程序和功能。第一个趋势是在大量电器中越来越多地使用软件，这些软件赋予智能处理和决策，以管理设备响应及其与用户和环境的交互。第二个趋势是由于通信和片上网络能力的进步，这种“嵌入式智能”（在欧洲也称为环境智能）的网络化程度越来越高。这种系统中的计算越来越面向应用，并且必须对设备将被放置在从手持个人空间到人体的环境做出响应。嵌入式计算的这种便携性对系统架构的能力提出了极端的要求，以容忍不同的能源条件，通信信道条件，网络条件等。然而，也有越来越多的应用程序的各种措施，包括性能，能源和功耗和其他QoS（服务质量）属性是可预测的。系统可用性和性能可靠性也是极其重要的，因为这些系统与真实的世界过程交互，并且它们的不可用可能导致不利的甚至灾难性的后果。这项研究解决了一些重要的挑战，在嵌入式计算和网络设备的电源，能源和性能的管理的方式，使我们能够开发出接近边界的质量所取得的成果。该项目正在开发的动态电源管理（UART）（在硬件和软件层面），并通过采用正式验证，概率建模和模型检查，以及合作博弈论的技术的其他类型的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