SoD-TEAM: Robust System Design Under Weak Component Assumptions

计算机与信息科学与工程理事会（CISE）计算机与网络系统（CNS）设计科学（SoD）项目提案号：0613967 P/I：皮海周系：电气与计算机工程学院：西北大学奖金：20万美元，为期24个月弱组件假设下的稳健系统设计这个项目的重点是为大型稳健系统开发一种新的“设计科学”。通常，大型健壮系统是分布式的，具有不同贡献者设计的异构组件；有些可能是遗留系统，有些可能是不受信任的第三方程序。最近Internet和联网设备（如移动电话和传感器网络）的快速开发和部署导致应用程序系统开发与传统软件工程大不相同：商业现成组件、遗留组件和不可信组件通常是这样一个系统中不可避免的组件。设计师对组件控制的减少带来了一个挑战：组件的假设越弱，构建一个可证明正确的系统甚至满足需求的系统就越困难。本项目的“设计科学”为不完美的组件提供了精确的规范，给出了不同假设下可行系统的功能极限，并提供了在弱组件假设下设计健壮系统的方法。pi期望他们严格的设计和规范理论（基于调整和扩展动作的时间逻辑——TLA——一种用单一语言表达程序及其属性的程序逻辑）将加深对系统保证和组件假设之间的关系和权衡的理解，特别是对于并发系统。这样的设计方法（例如，用于指定组件的语言和用于检查系统属性的一组工具）有助于设计更大、更安全的系统。项目经理：Anita J. La salle2006年6月21日

Directorate for Computer and Information Science and Engineering (CISE)Division Computer and Network Systems (CNS)Science of Design (SoD) ProgramProposal Number: 0613967 P/I: Hai Zhou PI's Department: Electrical and Computer Engineering Institution: Northwestern UniversityAward: $200,000 for 24 monthsTitle: "SoD TEAM: Robust System Design Under Weak Component Assumptions"This project focuses on developing a new "science of design" for large, robust systems. Typically, large-scale robust systems are distributed and reactive with heterogeneous components that may be designed by different contributors; some may be legacy systems and some may be un-trusted third-party programs. Recent rapid development and deployment of Internet and networked devices, such as cell phones and sensor networks, has resulted in application systems development that is vastly different from traditional software engineering: commercial of-the-shelf components, legacy components, and un-trusted components are generally unavoidable as components in such a system. Diminished designer-control over components poses a challenge: the weaker the component assumptions, the more difficult it is to build a provably-correct system or even a system that meets requirements. This project's "science of design" provides precise specifications for imperfect components, gives functional limits of feasible systems under different assumptions, and provides a methodology to design a robust system under weak component assumptions. The PIs anticipate that their rigorous theory of design and specification (based on adapting and extending Temporal Logic of Action -- TLA -- a program logic that expresses both programs and their properties with a single language) will deepen understanding of the relationships and trade-offs between system assurance and component-assumptions, particularly for concurrent systems. Such a design methodology (i.e., their language for specifying components and a set of tools for checking system properties) facilitate the design of larger and more secure systems. Program Manager: Anita J. La SalleDate: June 21, 2006