Constrained expressions: Adding analysis capabilities to design methods for concurrent software systems

We describe an approach to the design of concurrent software systems based on the constrained expression formalism. This formalism provides a rigorous conceptual model for the semantics of concurrent computations, thereby supporting analysis of important system properties as part of the design process. At the same time, our approach allows designers to use standard specification and design languages, rather than forcing them to deal with the formal model explicitly or directly. As a result, our approach attains the benefits of formal rigor without the associated pain of unnatural concepts or notations for its users. The conceptual model of concurrency underlying the constrained expression formalism treats the collection of possible behaviors of a concurrent system as a set of sequences of events. The constrained expression formalism provides a useful closed-form description of these sequences. We have developed algorithms for translating designs expressed in a wide variety of notations into these constrained expression descriptions. We have also developed a number of powerful analysis techniques that can be applied to these descriptions. In this paper, we describe the constrained expression formalism and these analysis techniques. We then describe the way this approach would be used in design, giving an example illustrating its use in conjunction with an Ada-like design language, and discuss present and future prospects for its automation and use.