SoD-TEAM: Robust System Design Under Weak Component Assumptions

计算机和信息科学与工程局（CISE）计算机和网络系统（CNS）设计科学（SoD）计划提案编号： 0613967 P/I： 海洲皮部： 电气与计算机工程学院：西北大学 $200，000 24个月标题： “特别行动小组：弱组件假设下的鲁棒系统设计“该项目的重点是为大型鲁棒系统开发一种新的“设计科学”。 通常情况下，大型健壮系统是分布式的，并与可能由不同贡献者设计的异构组件反应;一些可能是遗留系统，一些可能是不受信任的第三方程序。最近互联网和网络设备（如手机和传感器网络）的快速发展和部署，导致了应用系统开发与传统软件工程有很大不同：商业现成组件，遗留组件和不可信组件通常不可避免地成为这样一个系统中的组件。设计者对组件的控制力下降带来了挑战：组件假设越弱，构建可证明正确的系统甚至满足需求的系统就越困难。该项目的“设计科学”为不完美的组件提供了精确的规格，在不同的假设下给出了可行系统的功能限制，并提供了一种方法来设计一个强大的系统在弱组件的假设。PI预计，他们严格的设计和规范理论（基于调整和扩展动作的时间逻辑- TLA -一种用单一语言表达程序及其属性的程序逻辑）将加深对系统保证和组件假设之间的关系和权衡的理解，特别是对于并发系统。这种设计方法（即，它们用于指定组件的语言和用于检查系统属性的一组工具）促进了更大和更安全的系统的设计。项目经理：Anita J. La Salle日期：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