Checking subsystem safety properties in compositional reachability analysis
- 23 December 2002
- proceedings article
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 144-154
- https://doi.org/10.1109/icse.1996.493410
Abstract
The software architecture of a distributed program can be represented by an hierarchical composition of subsystems, with interacting processes at the leaves of the hierarchy. Compositional reachability analysis has been proposed as a promising automated method to derive the overall behavior of a distributed program in stages, based on its architecture. The method is particularly suitable for the analysis of programs which are subject to evolutionary change. When a program evolves, only behavior of those subsystems affected by the change need be re-evaluated. The method however has a limitation. The properties available for analysis are constrained by the set of actions that remain globally observable. The properties of subsystems, may not be analyzed. We extend the method to check safety properties of subsystems which may contain actions that are not globally observable. These safety properties can still be checked in the framework of compositional reachability analysis. The extension is supported by augmenting finite-state machines with a special undefined state /spl pi/. The state is used to capture possible violation of the safety properties specified by software developers. The concepts are illustrated using a gas station system as a case study.Keywords
This publication has 14 references indexed in Scilit:
- Compositional model checkingPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- An integrated method for effective behaviour analysis of distributed systemsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Compositional reachability analysis of finite-state distributed systems with user-specified constraintsPublished by Association for Computing Machinery (ACM) ,1995
- Data flow analysis for verifying properties of concurrent programsACM SIGSOFT Software Engineering Notes, 1994
- Enhancing compositional reachability analysis with context constraintsPublished by Association for Computing Machinery (ACM) ,1993
- Coverage Preserving Reduction Strategies for Reachability AnalysisPublished by Elsevier ,1992
- Automated analysis of concurrent systems with the constrained expression toolsetIEEE Transactions on Software Engineering, 1991
- Compositional reachability analysis using process algebraPublished by Association for Computing Machinery (ACM) ,1991
- Debugging Ada Tasking ProgramsIEEE Software, 1985
- A general-purpose algorithm for analyzing concurrent programsCommunications of the ACM, 1983