Checking safety properties using compositional reachability analysis

ABSTRACT

The software architecture of a distributed program can be represented by a hierarchical composition of subsystems, with interacting processes at the leaves of the hierarchy. Compositional reachability analysis (CRA) is a promising state reduction technique which can be automated and used in stages to derive the overall behavior of a distributed program based on its architecture. CRA is particularly suitable for the analysis of programs that are subject to evolutionary change. When a program evolves, only the behaviors of those subsystems affected by the change need be reevaluated. The technique however has a limitation. The properties available for analysis are constrained by the set of actions that remain globally observable. Properties involving actions encapsulated by subsystems may therefore not be analyzed. In this article, we enhance the CRA technique to check safety properties which may contain actions that are not globally observable. To achieve this, the state machine model is augmented with a special trap state labeled as &pgr;. We propose a scheme to transform, in stages, a property that involves hidden actions to one that involves only globally observable actions. The enhanced technique also includes a mechanism aiming at reducing the debugging effort. The technique is illustrated using a gas station system example.

REFERENCES

• 1: ALPERN, B. AND SCHNEIDER, F. B. 1985. Defining liveness. Inf. Process. Lett. 21, 4 (Oct.), 181-185.
• 2: Richard J. Anderson , Paul Beame , Steve Burns , William Chan , Francesmary Modugno , David Notkin , Jon D. Reese, Model checking large software specifications, Proceedings of the 4th ACM SIGSOFT symposium on Foundations of software engineering, p.156-166, October 16-18, 1996, San Francisco, California, United States
• 3: George S. Avrunin , Ugo A. Buy , James C. Corbett , Laura K. Dillon , Jack C. Wileden, Automated Analysis of Concurrent Systems with the Constrained Expression Toolset, IEEE Transactions on Software Engineering, v.17 n.11, p.1204-1222, November 1991 [doi>10.1109/32.106975]
• 4: BHARADWAJ, R. AND HEITMEYER, C. 1997. Model checking complete requirements specifications using abstraction. Rep. NRL/MR/5540-97-7999. Information Technology Division, Naval Research Laboratory, Washington, DC.
• 5: BROY, M. AND JAHNICHEN, S. 1993. Korrekte Software durch formale Methoden. Technische Universitat Berlin, Berlin, Germany.
• 6: CHEUNG, K. H. 1998. Compositional analysis of complex distributed systems. Ph.D. Dissertation. Department of Computer Science, Hong Kong University of Science and Technology, Hong Kong.
• 7: S. C. Cheung , J. Kramer, Enhancing compositional reachability analysis with context constraints, Proceedings of the 1st ACM SIGSOFT symposium on Foundations of software engineering, p.115-125, December 08-10, 1993, Los Angeles, California, United States
• 8: Shing Chi Cheung , J. Kramer, Tractable Dataflow Analysis for Distributed Systems, IEEE Transactions on Software Engineering, v.20 n.8, p.579-593, August 1994 [doi>10.1109/32.310668]
• 9: S. C. Cheung , J. Kramer, Compositional reachability analysis of finite-state distributed systems with user-specified constraints, Proceedings of the 3rd ACM SIGSOFT symposium on Foundations of software engineering, p.140-150, October 12-15, 1995, Washington, D.C., United States
• 10: Shing C. Cheung , Jeff Kramer, Checking subsystem safety properties in compositional reachability analysis, Proceedings of the 18th international conference on Software engineering, p.144-154, March 25-29, 1996, Berlin, Germany
• 11: Shing Chi Cheung , Jeff Kramer, Context constraints for compositional reachability analysis, ACM Transactions on Software Engineering and Methodology (TOSEM), v.5 n.4, p.334-377, Oct. 1996 [doi>10.1145/235321.235323]
• 12: Shing Chi Cheung , Dimitra Giannakopoulou , Jeff Kramer, Verification of liveness properties using compositional reachability analysis, Proceedings of the 6th European conference held jointly with the 5th ACM SIGSOFT international symposium on Foundations of software engineering, p.227-243, September 22-25, 1997, Zurich, Switzerland
• 13: E. Clarke , D. Long , K. McMillan, Compositional model checking, Proceedings of the Fourth Annual Symposium on Logic in computer science, p.353-362, June 1989, Pacific Grove, California, United States
• 14: James C. Corbett, Evaluating Deadlock Detection Methods for Concurrent Software, IEEE Transactions on Software Engineering, v.22 n.3, p.161-180, March 1996 [doi>10.1109/32.489078]
• 15: James C. Corbett , George S. Avrunin, Using integer programming to verify general safety and liveness properties, Formal Methods in System Design, v.6 n.1, p.97-123, Jan. 1995 [doi>10.1007/BF01384316]
• 16: Matthew B. Dwyer , Lori A. Clarke, Data flow analysis for verifying properties of concurrent programs, Proceedings of the 2nd ACM SIGSOFT symposium on Foundations of software engineering, p.62-75, December 06-09, 1994, New Orleans, Louisiana, United States
• 17: Matthew B. Dwyer , Vicki Carr , Laura Hines, Model checking graphical user interfaces using abstractions, Proceedings of the 6th European conference held jointly with the 5th ACM SIGSOFT international symposium on Foundations of software engineering, p.244-261, September 22-25, 1997, Zurich, Switzerland
• 18: Carlo Ghezzi , Mehdi Jazayeri , Dino Mandrioli, Fundamentals of software engineering, Prentice-Hall, Inc., Upper Saddle River, NJ, 1991
• 19: Dimitra Giannakopoulou , Jeff Kramer , Shing Chi Cheung, Behaviour Analysis of Distributed Systems Using the Tracta Approach, Automated Software Engineering, v.6 n.1, p.7-35, January 1999 [doi>10.1023/A:1008645800955]
• 20: Patrice Godefroid, Using Partial Orders to Improve Automatic Verification Methods, Proceedings of the 2nd International Workshop on Computer Aided Verification, p.176-185, June 18-21, 1990
• 21: Patrice Godefroid , Pierre Wolper, Using Partial Orders for the Efficient Verification of Deadlock Freedom and Safety Properties, Proceedings of the 3rd International Workshop on Computer Aided Verification, p.332-342, July 01-04, 1991
• 22: Susanne Graf , Bernhard Steffen, Compositional Minimization of Finite State Systems, Proceedings of the 2nd International Workshop on Computer Aided Verification, p.186-196, June 18-21, 1990
• 23: HELMBOLD, D. AND LUCKHAM, D. 1985. Debugging Ada tasking programs. IEEE Softw. 2, 2 (Mar.), 47-57.
• 24: C. A. R. Hoare, Communicating sequential processes, Prentice-Hall, Inc., Upper Saddle River, NJ, 1985
• 25: Gerard J. Holzmann, Design and validation of computer protocols, Prentice-Hall, Inc., Upper Saddle River, NJ, 1990
• 26: Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, v.23 n.5, p.279-295, May 1997 [doi>10.1109/32.588521]
• 27: Gerard J. Holzmann , Patrice Godefroid , Didier Pirottin, Coverage Preserving Reduction Strategies for Reachability Analysis, Proceedings of the IFIP TC6/WG6.1 Twelth International Symposium on Protocol Specification, Testing and Verification XII, p.349-363, June 22-25, 1992
• 28: Grégory Duval, Specification and verification of an object request broker, Proceedings of the 20th international conference on Software engineering, p.43-52, April 19-25, 1998, Kyoto, Japan
• 29: KEMPPAINEN, J., LEVANTO, M., VALMARI, A., AND CLEGG, M. 1992. "ARA" puts advanced reachability analysis techniques together. In Proceedings of the 5th Nordic Workshop on Programming Environment Research (Tampere, Finland, Jan.). 233-257.
• 30: Formal Development of Reactive Systems - Case Study Production Cell, January 1995
• 31: Douglas L. Long , Lori A. Clarke, Task interaction graphs for concurrency analysis, Proceedings of the 11th international conference on Software engineering, p.44-52, May 1989, Pittsburgh, Pennsylvania, United States [doi>10.1145/74587.74592]
• 32: Jeff Magee , Naranker Dulay , Susan Eisenbach , Jeff Kramer, Specifying Distributed Software Architectures, Proceedings of the 5th European Software Engineering Conference, p.137-153, September 25-28, 1995
• 33: MAGEE, J., DULAY, N., AND KRAMER, J. 1994. Regis: A constructive development environment for distributed programs. Distrib. Syst. Eng. 1, 5, 304-312.
• 34: Jawahar Malhotra , Robert M. Shapiro , Scott A. Smolka , Alessandro Giacalone, Winston: A Toll for Hierarchical Design and Simulation of Concurrent Systems, Proceedings of the BCS-FACS Workshop on Specification and Verification of Concurrent Systems, p.140-152, July 06-08, 1988
• 35: Zohar Manna , Amir Pnueli, Temporal verification of reactive systems: safety, Springer-Verlag New York, Inc., New York, NY, 1995
• 36: Rajesh Mascarenhas , Dinkar Karumuri , Ugo Buy , Robert Kenyon, Modeling and analysis of a virtual reality system with time Petri nets, Proceedings of the 20th international conference on Software engineering, p.33-42, April 19-25, 1998, Kyoto, Japan
• 37: Stephen P. Masticola , Barbara G. Ryder, A model of Ada programs for static deadlock detection in polynomial times, Proceedings of the 1991 ACM/ONR workshop on Parallel and distributed debugging, p.97-107, May 20-21, 1991, Santa Cruz, California, United States
• 38: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 39: R. Milner, Communication and concurrency, Prentice-Hall, Inc., Upper Saddle River, NJ, 1989
• 40: MILNER, R., PARROW, J., AND WALKER, D. 1989. A calculus of mobile processes Part I and II. University of Edinburgh, Edinburgh, UK.
• 41: Gleb Naumovich , George S. Avrunin , Lori A. Clarke , Leon J. Osterweil, Applying static analysis to software architectures, Proceedings of the 6th European conference held jointly with the 5th ACM SIGSOFT international symposium on Foundations of software engineering, p.77-93, September 22-25, 1997, Zurich, Switzerland
• 42: NG, K., KRAMER, J., MAGEE, J., AND DULAY, N. 1996. A visual approach to distributed programming. In Tools and Environments for Parallel and Distributed Systems. Kluwer Academic Publishers, Hingham, MA, 7-31.
• 43: Kurt M. Olender , Leon J. Osterweil, Cecil: A Sequencing Constraint Language for Automatic Static Analysis Generation, IEEE Transactions on Software Engineering, v.16 n.3, p.268-280, March 1990 [doi>10.1109/32.48935]
• 44: Robert Paige , Robert E. Tarjan, Three partition refinement algorithms, SIAM Journal on Computing, v.16 n.6, p.973-989, December 1, 1987 [doi>10.1137/0216062]
• 45: James Lyle Peterson, Petri Net Theory and the Modeling of Systems, Prentice Hall PTR, Upper Saddle River, NJ, 1981
• 46: Mauro Pezzè , Richard N. Taylor , Michal Young, Graph models for reachability analysis of concurrent programs, ACM Transactions on Software Engineering and Methodology (TOSEM), v.4 n.2, p.171-213, April 1995 [doi>10.1145/210134.210180]
• 47: Alexander Moshe Rabinovich, Checking Equivalences Between Concurrent Systems of Finite Agents (Extended Abstract), Proceedings of the 19th International Colloquium on Automata, Languages and Programming, p.696-707, July 13-17, 1992
• 48: John H. Reif , Scott A. Smolka, Data flow analysis of distributed communicating processes, International Journal of Parallel Programming, v.19 n.1, p.1-30, Feb. 1990 [doi>10.1007/BF01407862]
• 49: SABNANI, K. K., LAPONE, A. M., AND UYAR, M. 1989. An algorithmic procedure for checking safety properties of protocols. IEEE Trans. Commun. 37, 9 (Sept.), 940-948.
• 50: TAI, K. C. AND KOPPOL, P.V. 1993a. Hierarchy-based incremental reachability analysis of communication protocols. In Proceedings of the IEEE International Conference on Network Protocols (San Francisco, CA, Oct.). IEEE Press, Piscataway, NJ, 318-325.
• 51: Kuo-Chung Tai , Pramod V. Koppol, An incremental approach to reachability analysis of distributed programs, Proceedings of the 7th international workshop on Software specification and design, December 06-07, 1993, Redondo Beach, California
• 52: Richard N. Taylor, A general-purpose algorithm for analyzing concurrent programs, Communications of the ACM, v.26 n.5, p.361-376, May 1983 [doi>10.1145/69586.69587]
• 53: Antti Valmari, Stubborn sets for reduced state generation, Proceedings on Advances in Petri nets 1990, p.491-515, March 1991
• 54: VALMARI, A. 1992. Alleviating state explosion during verification of behavioural equivalence. Department of Computer Science, University of Helsinki, Helsinki, Finland.
• 55: Antti Valmari , Jukka Kemppainen , Matthew Clegg , Mikko Levanto, Putting Advanced Reachability Analysis Techniques Together: the "ARA" Tool, Proceedings of the First International Symposium of Formal Methods Europe on Industrial-Strength Formal Methods, p.597-616, April 19-23, 1993
• 56: YEH, W. J. 1993. Controlling state explosion in reachability analysis. Tech. Rep. SERC-TR-147-P. Software Engineering Research Center (SERC) Laboratory, Purdue University, West Lafayette, IN.
• 57: Wei Jen Yeh , Michal Young, Compositional reachability analysis using process algebra, Proceedings of the symposium on Testing, analysis, and verification, p.49-59, October 08-10, 1991, Victoria, British Columbia, Canada [doi>10.1145/120807.120812]
• 58: YEH, W. g. AND YOUNG, M. 1993. Hierarchical tracing of concurrent programs. Tech. Rep. SERC-TR-137-P. Software Engineering Research Center (SERC) Laboratory, Purdue University, West Lafayette, IN.
• 59: Michal Young , Richard N. Taylor , David L. Levine , Kari A. Nies , Debra Brodbeck, A concurrency analysis tool suite for Ada programs: rationale, design, and preliminary experience, ACM Transactions on Software Engineering and Methodology (TOSEM), v.4 n.1, p.65-106, Jan. 1995 [doi>10.1145/201055.201080]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
          Subjects: Methodologies (e.g., object-oriented, structured)

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.9 Management
          Subjects: Software quality assurance (SQA)

General Terms:
Design, Theory, Verification

Keywords:
compositional reachability analysis, distributed systems, model checking, safety properties, static analysis