Analysis of recursive state machines

ABSTRACT

Recursive state machines (RSMs) enhance the power of ordinary state machines by allowing vertices to correspond either to ordinary states or to potentially recursive invocations of other state machines. RSMs can model the control flow in sequential imperative programs containing recursive procedure calls. They can be viewed as a visual notation extending Statecharts-like hierarchical state machines, where concurrency is disallowed but recursion is allowed. They are also related to various models of pushdown systems studied in the verification and program analysis communities.After introducing RSMs and comparing their expressiveness with other models, we focus on whether verification can be efficiently performed for RSMs. Our first goal is to examine the verification of linear time properties of RSMs. We begin this study by dealing with two key components for algorithmic analysis and model checking, namely, reachability (Is a target state reachable from initial states?) and cycle detection (Is there a reachable cycle containing an accepting state?). We show that both these problems can be solved in time O(nθ²) and space O(nθ), where n is the size of the recursive machine and θ is the maximum, over all component state machines, of the minimum of the number of entries and the number of exits of each component. From this, we easily derive algorithms for linear time temporal logic model checking with the same complexity in the model. We then turn to properties in the branching time logic CTL*, and again demonstrate a bound linear in the size of the state machine, but only for the case of RSMs with a single exit node.

REFERENCES

• 1: Alur, R., Etessami, K., and Madhusudan, P. 2004. A temporal logic of nested calls and returns. In Proceedings of the 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'04), volume 2988 of LNCS, pages 467--481. Springer.
• 2: Rajeev Alur , Kousha Etessami , Mihalis Yannakakis, Analysis of Recursive State Machines, Proceedings of the 13th International Conference on Computer Aided Verification, p.207-220, July 18-22, 2001
• 3: Alur, R., Torre, S. L., and Madhusudan, P. 2003a. Modular strategies for recursive game graphs. In Proceedings of TACAS, volume 2619 of LNCS, pages 363--378.
• 4: Alur, R., Torre, S. L., and Madhusudan, P. 2003b. Modular strategies for infinite games on recursive graphs. In Proceedings of CAV'03, volume 2725 of LNCS, pages 67--79.
• 5: Rajeev Alur , Mihalis Yannakakis, Model checking of hierarchical state machines, ACM Transactions on Programming Languages and Systems (TOPLAS), v.23 n.3, p.273-303, May 2001 [doi>10.1145/503502.503503]
• 6: Henrik Reif Andersen, Model checking and boolean graphs, Theoretical Computer Science, v.126 n.1, p.3-30, April 11, 1994 [doi>10.1016/0304-3975(94)90266-6]
• 7: Thomas Ball , Sriram K. Rajamani, Bebop: A Symbolic Model Checker for Boolean Programs, Proceedings of the 7th International SPIN Workshop on SPIN Model Checking and Software Verification, p.113-130, August 30-September 01, 2000
• 8: Michael Benedikt , Patrice Godefroid , Thomas W. Reps, Model Checking of Unrestricted Hierarchical State Machines, Proceedings of the 28th International Colloquium on Automata, Languages and Programming,, p.652-666, July 08-12, 2001
• 9: Grady Booch , James Rumbaugh , Ivar Jacobson, The Unified Modeling Language user guide, Addison Wesley Longman Publishing Co., Inc., Redwood City, CA, 1999
• 10: Ahmed Bouajjani , Javier Esparza , Oded Maler, Reachability Analysis of Pushdown Automata: Application to Model-Checking, Proceedings of the 8th International Conference on Concurrency Theory, p.135-150, July 01-04, 1997
• 11: Ahmed Bouajjani , Javier Esparza , Tayssir Touili, A generic approach to the static analysis of concurrent programs with procedures, Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.62-73, January 15-17, 2003, New Orleans, Louisiana, USA
• 12: Balakrishnan, G. and Reps, T. 2004. Analyzing memory accesses in x86 executables. In Proceedings of the International Conference on Compiler Construction (CC'04), volume 2985 of LNCS, pages 5--23. Springer.
• 13: Olaf Burkart , Bernhard Steffen, Model Checking for Context-Free Processes, Proceedings of the Third International Conference on Concurrency Theory, p.123-137, August 24-27, 1992
• 14: Olaf Burkart , Bernhard Steffen, Model checking the full modal mu-calculus for infinite sequential processes, Theoretical Computer Science, v.221 n.1-2, p.251-270, June 28, 1999 [doi>10.1016/S0304-3975(99)00034-1]
• 15: Chatterjee, K., Ma, D., Majumdar, R., Zhao, T., Henzinger, T. A., and Palsberg, J. 2003. Stack size analysis for interrupt-driven programs. In Proceedings of the 10th Static Analysis Symposium, pages 109--126.
• 16: Hao Chen , David Wagner, MOPS: an infrastructure for examining security properties of software, Proceedings of the 9th ACM conference on Computer and communications security, November 18-22, 2002, Washington, DC, USA [doi>10.1145/586110.586142]
• 17: Cousot, P. and Cousot, R. 1977. Static determination of dynamic properties of recursive procedures. In IFIP Conference on Formal Description of Programming Concepts, St-Andrews, N.B., CA, E.J. Neuhold (Ed.), pages 237--277, St-Andrews, N.B., Canada.
• 18: Didier Caucal , Roland Monfort, On the transition graphs of automata and grammars, Proceedings of the 16rd International Workshop on Graph-Theoretic Concepts in Computer Science, p.311-337, June 20-22, 1990
• 19: Emerson, A. 1990. Modal and temporal logic. In Handbook of Theoretical Computer Science, Volume B, pages 995--1072, MIT Press.
• 20: Emerson, A. and Lei, C. 1986. Efficient model-checking in fragments of the propositional mu-calculus. In LICS 98, pages 267--278.
• 21: Javier Esparza , David Hansel , Peter Rossmanith , Stefan Schwoon, Efficient Algorithms for Model Checking Pushdown Systems, Proceedings of the 12th International Conference on Computer Aided Verification, p.232-247, July 15-19, 2000
• 22: Etessami, K. 2004. Analysis of recursive game graphs using data flow equations. In 5th International Conference on Verification, Model Checking, and Abstract Interpretation, volume 2937 of LNCS, pages 282--296. Springer.
• 23: Finkel, A., Willems, B., and Wolper, P. 1997. A direct symbolic approach to model checking pushdown systems. In Infinity'97 Workshop, volume 9 of Electronic Notes in Theoretical Computer Science.
• 24: GrammaTech, Inc. 2000. CodeSurfer System. “http://www.grammatech.com/products/ codesurfer/”.
• 25: David Harel, Statecharts: A visual formalism for complex systems, Science of Computer Programming, v.8 n.3, p.231-274, June 1, 1987 [doi>10.1016/0167-6423(87)90035-9]
• 26: Nevin Heintze , David McAllester, On the Cubic Bottleneck in Subtyping and Flow Analysis, Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science, p.342, June 29-July 02, 1997
• 27: Susan Horwitz , Thomas Reps , David Binkley, Interprocedural slicing using dependence graphs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.12 n.1, p.26-60, Jan. 1990 [doi>10.1145/77606.77608]
• 28: Horwitz, S., Reps, T., Bricker, T., and Rosay, G. 1997. Wisconsin Program-Slicing Tool. “http://www.cs.wisc.edu/wpis/slicing_tool/”.
• 29: Thomas Reps , Susan Horwitz , Mooly Sagiv , Genevieve Rosay, Speeding up slicing, Proceedings of the 2nd ACM SIGSOFT symposium on Foundations of software engineering, p.11-20, December 06-09, 1994, New Orleans, Louisiana, United States
• 30: David Melski , Thomas W. Reps, Interprocedural Path Profiling, Proceedings of the 8th International Conference on Compiler Construction, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS'99, p.47-62, March 22-28, 1999
• 31: David Melski , Thomas Reps, Interconvertibility of a class of set constraints and context-free-language reachability, Theoretical Computer Science, v.248 n.1-2, p.29-98, October 2000 [doi>10.1016/S0304-3975(00)00049-9]
• 32: Reps, T. 1998. Program analysis via graph reachability. Info. Soft. Tech. 40(11--12), 701--726.
• 33: Thomas Reps , Susan Horwitz , Mooly Sagiv, Precise interprocedural dataflow analysis via graph reachability, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.49-61, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199462]
• 34: Thomas Reps , Genevieve Rosay, Precise interprocedural chopping, Proceedings of the 3rd ACM SIGSOFT symposium on Foundations of software engineering, p.41-52, October 12-15, 1995, Washington, D.C., United States
• 35: Reps, T., Schwoon, S., and Jha, S. 2003. Weighted pushdown systems and their application to interprocedural dataflow analysis. In Proceedings of the 10th Static Analysis Symposium, pages 189--213.
• 36: Mooly Sagiv , Thomas Reps , Susan Horwitz, Precise interprocedural dataflow analysis with applications to constant propagation, Theoretical Computer Science, v.167 n.1-2, p.131-170, Oct. 30, 1996
• 37: Schwoon, S. 2002. Moped System. “http://www.fmi.uni-stuttgart.de/szs/tools/moped/”.
• 38: Schwoon, S., Reps, T., and Jha, S. 2003. Weighted PDS Library. “http://www.fmi. uni-stuttgart.de/szs/tools/wpds/”.
• 39: Schwoon, S., Jha, S., Reps, T., and Stubblebine, S. 2003. On generalized authorization problems. In Proceedings of the 16th Computer Section Foundations Workshop, pages 202--218.
• 40: Ball, T. and Rajamani, S. 2000. SLAM Toolkit. “http://research.microsoft.com/slam/”.
• 41: Sharir, M. and Pnueli, A. 1981. Two approaches to interprocedural data flow analysis. In Program Flow Analysis: Theory and Applications, S.S. Muchnick and N.D. Jones (eds.), Prentice-Hall, Englewood Cliffs, NJ, pages 189--234.
• 42: Jeffrey D. Ullman, Principles of database and knowledge-base systems, Vol. I, Computer Science Press, Inc., New York, NY, 1988
• 43: Valiant, L. G. 1975. General context-free recognition in less than cubic time. J. Comput. Syst. Sci. 10, 308--315.
• 44: Moshe Y Vardi , Pierre Wolper, Automata-Theoretic techniques for modal logics of programs, Journal of Computer and System Sciences, v.32 n.2, p.183-221, April 1986 [doi>10.1016/0022-0000(86)90026-7]
• 45: Igor Walukiewicz, Pushdown processes: games and model-checking, Information and Computation, v.164 n.2, p.234-263, Jan. 29, 2001 [doi>10.1006/inco.2000.2894]
• 46: Mihalis Yannakakis, Graph-theoretic methods in database theory, Proceedings of the ninth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, p.230-242, April 02-04, 1990, Nashville, Tennessee, United States [doi>10.1145/298514.298576]
• 47: W. A. Woods, Transition network grammars for natural language analysis, Communications of the ACM, v.13 n.10, p.591-606, Oct. 1970 [doi>10.1145/355598.362773]
• 48: WPDS++: 2004. A C++ Library for Weighted Pushdown Systems, University of Wisconsin.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.2 Design Tools and Techniques
          Subjects: State diagrams

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Formal methods

  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.1 Models of Computation
          Subjects: Automata (e.g., finite, push-down, resource-bounded)
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

General Terms:
Algorithms, Verification

Keywords:
Software verification, context-free languages, model checking, program analysis, pushdown automata, recursive state machines, temporal logic