Analysis of distributed systems using constrained expressions (concurrent systems)
Laura K. Dillon · 1984
Due to the complexity of their tasks, developers of distributed systems would greatly benefit from automated tools to aid in the analysis of the systems they create. Ideally, these tools should be integrated in an environment providing tools to support all the activities required for developing and maintaining large, distributed software systems. Tools supporting analysis based on the constrained expression framework would make an important contribution to such an environment. The constrained expression framework is especially well-suited for use with system designs. It thus provides a basis for the development of preimplementation analysis tools. These tools would complement tools based on other distributed system analysis techniques. Due to the generality of the constrained expression framework, furthermore, analysis methods based on constrained expressions could be extended to provide common analysis methods across a number of phases in the software development process. This could be a source of valuable commonality and integration in a software development environment. In this dissertation we describe the constrained expression framework and show how it can be used to help developers of distributed software systems analyze the systems they create. We explain how constrained expressions represent the possible behaviors of a concurrent system, illustrating the generality of constrained expressions by using them with systems expressed in three fundamentally different notations. A theory for manipulating constrained expressions is presented. Based on this theory, a procedure for simplifying the constrained expression representations of SDYMOL systems is formulated. This procedure results in a constrained expression, which facilitates subsequent analysis. Algorithms for further simplifying SDYMOL reduced constrained expressions are also described. An example is presented to illustrate the simplification techniques. This example is also used to demonstrate analysis techniques, based on the constrained expression framework, that can be used to establish specific behavioral properties of a system.