Behavioral Type Checking of Architectural Components Based on Assumptions

A critical challenge faced by the developer of a software system is to understand whether the system's components correctly integrate. While type theory has provided substantial help in detecting and preventing errors in mismatched static properties, much work remains in the area of dynamics. In particular, components make assumptions about their behavioral interaction with other components, but currently we have only limited ways in which to state those assumptions and to analyze those assumptions for correctness. We have begun to formulate a method that addresses this problem. The method operates at the architectural level so that behavioral integration errors, such as deadlock, can be revealed early in development. For each component, a specification is given both of its own interaction behavior and of the assumptions that it makes about the interaction behavior of the external context in which it expects to operate. We have defined an algorithm that, given such specifica..