Automated Analysis of Concurrent Systems with the Constrained Expression Toolset

The constrained expression approach to analysis of concurrent software systems has several attractive features, including the facts that it can be used with a variety of design and programming languages and that it does not require a complete enumeration of the set of reachable states of the concurrent system. This paper reports on the construction of a toolset automating the main constrained expression analysis techniques and the results of experiments with that toolset. The toolset is capable of carrying out completely automated analyses of a variety of concurrent systems, starting from source code in an Ada-like design language and producing system traces displaying the properties represented by the analyst 's queries. It has been successfully used with designs that involve hundreds of concurrent processes. Research partially supported by NSF grant CCR-8806970 and ONR grant N00014-89-J1064. y Research partially supported by NSF grant CCR-8702905. z Research partially supporte..