Tracta : an environment for analysing the behaviour of distributed systems
Dimitra Giannakopoulou, Jeff Kramer, Shing-Chi Cheung · 1997
Particular emphasis needs to be placed on the integration of analysis techniques with other software development activities, to form a complete environment for the design and construction of distributed systems. We have addressed this problem by using a compositional approach to analysis. The software architecture of a distributed program is represented by a hierarchical composition of subsystems, with interacting processes at the leaves of the hierarchy. Compositional reachability analysis (CRA) exploits the compositional hierarchy to incrementally construct the overall behaviour of the system from that of its subsystems. In the Tracta CRA approach, both processes and properties reflecting system specifications are modelled as state-machines. Property state machines are also composed into the system. and violations are detected on the global graph obtained. The method is supported by an automated tool implemented in C++ and rzwming on Unix.