Model checking of hierarchical state machines

ABSTRACT

Model checking is emerging as a practical tool for detecting logical errors in early stages of system design. We investigate the model checking of hierarchical (nested) systems, i.e. finite state machines whose states themselves can be other machines. This nesting ability is common in various software design methodologies and is available in several commercial modeling tools. The straightforward way to analyze a hierarchical machine is to flatten it (thus, incurring an exponential blow up) and apply a model checking tool on the resulting ordinary FSM. We show that this flattening can be avoided. We develop algorithms for verifying linear time requirements whose complexity is polynomial in the size of the hierarchical machine. We address also the verification of branching time requirements and provide efficient algorithms and matching lower bounds.

REFERENCES

• 1: L. Apfelbaum. Automated functional test generation. In Proc. IEEE Autotestcon Conference, 1995.
• 2: Orna Bernholtz , Moshe Y. Vardi , Pierre Wolper, An Automata-Theoretic Approach to Branching-Time Model Checking (Extended Abstract), Proceedings of the 6th International Conference on Computer Aided Verification, p.142-155, June 21-23, 1994
• 3: Grady Booch , James Rumbaugh , Ivar Jacobson, The Unified Modeling Language user guide, Addison Wesley Longman Publishing Co., Inc., Redwood City, CA, 1999
• 4: 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
• 5: 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
• 6: Edmund M. Clarke , E. Allen Emerson, Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic, Logic of Programs, Workshop, p.52-71, May 01, 1981
• 7: Edmund M. Clarke , Robert P. Kurshan, Computer-aided verification, IEEE Spectrum, v.33 n.6, p.61-67, June 1996 [doi>10.1109/6.499951]
• 8: Edmund M. Clarke , Jeannette M. Wing, Formal methods: state of the art and future directions, ACM Computing Surveys (CSUR), v.28 n.4, p.626-643, Dec. 1996 [doi>10.1145/242223.242257]
• 9: C. Courcoubetis , M. Vardi , P. Wolper , M. Yannakakis, Memory-efficient algorithms for the verification of temporal properties, Formal Methods in System Design, v.1 n.2-3, p.275-288, Oct. 1992 [doi>10.1007/BF00121128]
• 10: Doron Drusinsky , David Harel, On the power of bounded concurrency I: finite automata, Journal of the ACM (JACM), v.41 n.3, p.517-539, May 1994 [doi>10.1145/176584.176587]
• 11: Bell Labs Design Automation. FormalCheck, wwx.bell-labs.com/formalcheck.
• 12: A.R. Flora-Holmquist, J.D. O'Grady, and M.G. Staskauskas. Telecommunications softnwe design using virtual finite state machines. Proc. Intl. Switching Symposium (ISS.95), pp. 103-107, 1995.
• 13: 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]
• 14: G.J. Holzmann. Early fault detection tools. Sofrloare Concepts and Tools 17(2):63-69, 1996.
• 15: 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]
• 16: G.J. Holzmann, D. A. Peled, M. H. Redberg. Design tools for for requirements engineering. Bell Labs Technical Journal, 2( l):S6-95,1997.
• 17: Ivar Jacobson, Object-oriented software engineering, ACM Press, New York, NY, 1991
• 18: F. Jahanian , A. K.-L. Mok, A graph-theoretic approach for timing analysis and its implementation, IEEE Transactions on Computers, v.36 n.8, p.961-975, Aug. 1987 [doi>10.1109/TC.1987.5009519]
• 19: Nancy G. Leveson , Mats Per Erik Heimdahl , Holly Hildreth , Jon D. Reese, Requirements Specification for Process-Control Systems, IEEE Transactions on Software Engineering, v.20 n.9, p.684-707, September 1994 [doi>10.1109/32.317428]
• 20: ITU-T Recommendation 2.120. Message Sequence Chart (MSC). 1996.
• 21: A. Pnueli. The temporal logic of programs. In Proc. of the 18th IEEE Symposium on Foundations of Computer Science, pages 46-77,1977.
• 22: Jean-Pierre Queille , Joseph Sifakis, Specification and verification of concurrent systems in CESAR, Proceedings of the 5th Colloquium on International Symposium on Programming, p.337-351, April 06-08, 1982
• 23: James Rumbaugh , Michael Blaha , William Premerlani , Frederick Eddy , William Lorensen, Object-oriented modeling and design, Prentice-Hall, Inc., Upper Saddle River, NJ, 1991
• 24: E. Rudolph, J. Grabowski, P. Graubmann. Tutorial on Message Sequence Charts (MSC'96). FORTE/PSTV'96,1996.
• 25: Bran Selic , Garth Gullekson , Paul T. Ward, Real-time object-oriented modeling, John Wiley & Sons, Inc., New York, NY, 1994
• 26: M.Y. Vardi and P. Wolper. An automatatheoretic approach to automatic program verification. Proc. of the First IEEE Symp. on Logic in Computer Science, pp. 332-344, 1986.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Model checking

Additional Classification:
  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.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Temporal logic

  G. Mathematics of Computing
  G.4 MATHEMATICAL SOFTWARE
      Subjects: Algorithm design and analysis

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