Constructing Large Complex Systems via Tractable Pairwise Composition of Software Components

点击翻译按钮获取中文摘要

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.