SoD-TEAM: Robust System Design Under Weak Component Assumptions

计算机与信息科学与工程部计算机与网络系统(CSIS)设计科学(SoD)计划建议编号：0613967 P/I：海州皮系：西北大学电气与计算机工程学院奖项：24个月200,000美元标题：“SoD团队：弱组件假设下的稳健系统设计”这个项目致力于为大型、稳健的系统发展一门新的“设计科学”。通常，大规模健壮的系统是分布式的，并与可能由不同贡献者设计的异类组件反应；一些可能是遗留系统，一些可能是不受信任的第三方程序。最近互联网和网络设备(如手机和传感器网络)的快速发展和部署导致了与传统软件工程截然不同的应用系统开发：商业现成组件、遗留组件和不可信组件通常不可避免地成为此类系统中的组件。设计者对组件的控制减少带来了挑战：组件假设越弱，就越难构建可证明是正确的系统，甚至是满足要求的系统。该项目的“设计科学”提供了对不完美部件的精确规范，给出了不同假设下可行系统的功能极限，并提供了一种在弱部件假设下设计鲁棒系统的方法。PI期望他们严格的设计和规范理论(基于改编和扩展时态动作逻辑--TLA--一种用单一语言表达程序及其属性的程序逻辑)将加深对系统保证和组件假设之间的关系和权衡的理解，特别是对于并发系统。这种设计方法(即，它们用于指定组件的语言和一套用于检查系统属性的工具)有助于设计更大和更安全的系统。项目经理：Anita J.La SalleDate：2006年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