Enhancing compositional reachability analysis with context constraints

ABSTRACT

Compositional techniques have been proposed for traditional reachability analysis in order to introduce modularity and to control the state explosion problem. While modularity has been achived, state explosion is still a problem. Indeed, this problem may even be exacerbated as a locally minimised subsystem may contain many states and transitions forbidden by its context or environments. This paper presents a method to alleviate this problem effectively by including context constraints in local subsystem minimisation. The global behaviour generated using the method is observationally equivalent to that generated by compositional reachability analysis without the inclusion of context constraints.Context constraints, specified as interface processes, are restrictions imposed by the environment on subsystem behaviour. The minimisation produces a simplified machine that describes the behaviour of the subsystem constrained by its context. This machine can also be used as a substitute for the original subsystem in the subsequent steps of the compositional reachability analysis. Interface processes capturing context constraints can be specified by users or automatically constructd using a simple algorithm. The concepts in the paper are illustrated with a clients/server system.

REFERENCES

• 1: Gregory R. Andrews, Paradigms for process interaction in distributed programs, ACM Computing Surveys (CSUR), v.23 n.1, p.49-90, March 1991 [doi>10.1145/103162.103164]
• 2: CCITT Red Book. Integrated Services Digital Network (ISDN) Recommendation, Study Group XVIII, Vol. III, fascicle 111.5, (1984).
• 3: S.C. Cheung and J. Kramer. Contextual Analysis for Subsystems in Concurrent Programs, Technical Report, DoC 93/16, Imperial College of Science, Technology and Medicine, June 1993.
• 4: S.C. Cheung and J. Kramer. Enhancing Compositional Analysis with Interfaces, Technical Report, DoC 1993/13, Imperial College of Science, Technology and Medicine, April 1993.
• 5: Shing-Chi Cheung , Jeff Kramer, Tractable Flow Analysis for Anomaly Detection in Distributed Programs, Proceedings of the 4th European Software Engineering Conference on Software Engineering, p.283-300, September 13-17, 1993
• 6: E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite state concurrent system using temporal logic specifications: a practical approach, Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.117-126, January 24-26, 1983, Austin, Texas [doi>10.1145/567067.567080]
• 7: 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
• 8: Limor Fix , Nissim Francez , Orna Grumberg, Program composition and modular verification, Proceedings of the 18th international colloquium on Automata, languages and programming, p.93-114, June 1991, Madrid, Spain
• 9: Carlo Ghezzi , Mehdi Jazayeri , Dino Mandrioli, Fundamentals of software engineering, Prentice-Hall, Inc., Upper Saddle River, NJ, 1991
• 10: 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
• 11: 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
• 12: David Harel, On visual formalisms, Communications of the ACM, v.31 n.5, p.514-530, May 1988 [doi>10.1145/42411.42414]
• 13: C. A. R. Hoare, Communicating sequential processes, Prentice-Hall, Inc., Upper Saddle River, NJ, 1985
• 14: Sören Holmström, Hennessy-Milner Logic with Recursion as a Specification Language, and a Refinement Calculus based on It, Proceedings of the BCS-FACS Workshop on Specification and Verification of Concurrent Systems, p.294-330, July 06-08, 1988
• 15: John E. Hopcroft , Jeffrey D. Ullman, Introduction To Automata Theory, Languages, And Computation, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1990
• 16: J. Kemppainen, M. Levanto, A. Valmari, et. al. "ARA" Puts Advanced Reachability Analysis Techniques Together. In Proc. 5th Nordic Workshop on Programming Environment Research, Programming Environment Research, Tampere University of Technology, Tampere, Finland, January 1992, pp. 233-257.
• 17: J. Kramer, J. Magee, K. Ng, et. al. The System Architect's Assistant for Design and Construction of Distributed Systems, In Proc, 4th IEEE Workshop on Future Trends of Distributed Computing Systems, Lisbon, September 1993.
• 18: H. Krumm, Projections of the reachability graph and environment models, Proceedings of the international workshop on Automatic verification methods for finite state systems, p.89-96, February 1990, Grenoble, France
• 19: K. G. Larsen , R. Milner, Verifying a protocol using relativized bisimulation, 14th International Colloquium on Automata, languages and programming, p.126-135, July 1987, Karlsruhe, Germany
• 20: K. G. Larsen, Compositional theories based on an operational semantics of contexts, Proceedings on Stepwise refinement of distributed systems: models, formalisms, correctness, p.487-518, May 1990, Mook, The Netherlands
• 21: 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
• 22: R. Milner, Communication and concurrency, Prentice-Hall, Inc., Upper Saddle River, NJ, 1989
• 23: James Lyle Peterson, Petri Net Theory and the Modeling of Systems, Prentice Hall PTR, Upper Saddle River, NJ, 1981
• 24: M. Pezz&, R.N. Taylor and M. Young. Graph Models for Reachability Analysis of Concurrent Programs, Technical Report, Software Engineering Research Centre, Department of Computer Science, Purdue University, May 1993.
• 25: 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
• 26: K.K. Sabnani, A.M. Lapone and M.U. Uyar. An Algorithmic Procedure for Checking Safety Properties of Protocols. IEEE Transactions on Communications 37,9 (September 1989), 940-948.
• 27: Scott Allen Smolka, Analysis of communicating finite-state processes, 1984
• 28: Dirk Taubner, Finite representations of CCS and TCSP programs by automata and Petri nets, Springer-Verlag New York, Inc., New York, NY, 1989
• 29: R.N. Taylor. Complexity of Analyzing the Synchronization Structure of Concurrent Programs. Acts Informatica 19 (1983), 57-84.
• 30: 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]
• 31: A. Valmari. Compositional State Space Generation, Technical Report, A- 1991-5, Department of Computer Science, University of Helsinki, Finland, October 1991.
• 32: A. Valmari. Alleviating State Explosion during Verification of Behavioral Equivalence, Technical Report, A-1992, Department of Computer Science, University of Helsinki, Finland, August 1992.
• 33: 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]
• 34: W.J. Yeh and M. Young. Hierarchical Tracing of Concurrent Programs. In Proc. 3rd Irvine Soflware Symposium (1SS'93), Irvine, California, April 1993.
• 35: Pamela Zave, A Compositional Approach to Multiparadigm Programming, IEEE Software, v.6 n.5, p.15-25, September 1989 [doi>10.1109/52.35586]

INDEX TERMS

Primary Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES

Additional Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES

General Terms:
Algorithms, Design, Measurement, Performance, Theory