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

Virginia Polytechnic Institute And State University, Blacksburg VA

Investigators

Abstract

Proposal Title: PECASE: Formal Analysis and Validation of Probabilistic Guarantees on QoS and other Power/Performance Characteristics in Embedded Systems Design Institution: Virginia Polytechnic Institute and State University As 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