Static checking of system behaviors using derived component assumptions

A critical challenge faced by the developer of a software system is to unde rstand whether the system's components correctly integrate. While type theo ry has provided substantial help in detecting and preventing errors in mism atched static properties, much work remains in the area of dynamics. In par ticular, components make assumptions about their behavioral interaction wit h other components, but currently we have only limited ways in which to sta te those assumptions and to analyze those assumptions for correctness. We h ave formulated a method that begins to address this problem. The method ope rates at the architectural level so that behavioral integration errors, suc h as deadlock, can be revealed early and at a high level. For each componen t, a specification is given of its interaction behavior. From this specific ation, assumptions that the component makes about the corresponding interac tion behavior of the external context are automatically derived. We have de fined an algorithm that performs compatibility checks between finite repres entations of a component's context assumptions and the actual interaction b ehaviors of the components with which it is intended to interact. A configu ration of a system is possible if and only if a successful way of matching actual behaviors with assumptions can be found. The state-space complexity of this algorithm is significantly less than that of comparable approaches, and in the worst case, the time complexity is comparable to the worst case of standard reachability analysis.