Constructing Large Complex Systems via Tractable Pairwise Composition of Software Components

该项目的目标是为大型复杂软件系统的开发提供有用和实用的方法。研究将解决将软件组件组合成具有保证正确性的大型系统的问题。状态爆炸（可能的系统行为数量与系统组件数量的指数增长）可以通过单独分析每对组件之间的相互作用来避免，而不是一次检查所有组件的相互作用。然而，这种局部方法使我们能够证明整个系统的行为符合预期。由于需要分析的行为数量要少得多，因此严格分析和验证大型系统所需的工作量大大减少。主要活动有：1。开发精确描述软件组件所需行为的技术。开发实用的方法来推理当一组组件连接起来形成一个大系统时所产生的行为。这项研究的好处是减少了创建具有可验证的正确性的实际大小的软件系统的成本。

The objective of the project is to produce useful and practicalmethods for the development of large complex software systems. Theresearch will address the problem of composing software componentsinto large systems that have guaranteed correctness properties.State-explosion (the exponential growth of the number of possiblesystem behaviors with the number of the system's components) isavoided by analyzing interactions among every pair of componentsseparately, rather than inspecting the interaction of all componentsat once. This local approach nevertheless enables us to prove thatthe overall system behaves as desired. Since the number of behaviorsthat have to be analyzed is much smaller, the amount of effort neededto rigorously analyze and verify large systems is greatly reduced.The main activities are:1. Develop techniques for the precise description of therequired behavior of a software component.2. Develop practical methods for reasoning about the behavior thatresults when a set of components are connected to form a largesystem.The benefit of this research is to reduce the cost of creatingrealistic size software systems that have demonstrable correctnessproperties.