This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Optimizing Symbolic Model Checking for Statecharts
February 2001 (vol. 27 no. 2)
pp. 170-190

Abstract—Symbolic model checking based on binary decision diagrams is a powerful formal verification technique for reactive systems. In this paper, we present various optimizations for improving the time and space efficiency of symbolic model checking for systems specified as statecharts. We used these techniques in our analyses of the models of a collision avoidance system and a fault-tolerant electrical power distribution (EPD) system, both used on commercial aircraft. The techniques together reduce the time and space requirements by orders of magnitude, making feasible some analysis that was previously intractable. We also elaborate on the results of verifying the EPD model. The analysis disclosed subtle modeling and logical flaws not found by simulation.

[1] J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang., "Symbolic model checking: 1020states and beyond," Information and Computation, vol. 98, no. 2, pp. 142-170, June 1992.
[2] R.E. Bryant, "Graph-Based Algorithms for Boolean Function Manipulation," IEEE Trans. Computers, Vol. C-35, No. 8, Aug. 1986, pp. 667-690.
[3] W. Chan, R.J. Anderson, P. Beame, S. Burns, F. Modugno, D. Notkin, and J.D. Reese, "Model Checking Large Software Specifications," IEEE Trans. Software Eng., vol. 24, no. 7, July 1998.
[4] N.C. Levenson, M.P.E. Heimdahl, H. Hildreth, and J.D. Reese, "Requirements Specification for Process-Control Systems," IEEE Trans. Software Eng., vol. 20, no. 9, pp. 684-707, Sept. 1994.
[5] D. Harel, “Statecharts: A Visual Approach to Complex Systems,” Science of Computer Programming, Vol. 8, No. 3, pp. 231–274, 1987.
[6] C.R. Nobe and M.G. Bingle, “Model-Based Development: Five Processes Used at Boeing,” Proc. IEEE Int'l Conf. and Workshop: Eng. of Computer-Based Systems, Mar./Apr. 1998
[7] C.R. Nobe and W.E. Warner, “Lessons Learned from a Trial Application of Requirements Modeling using Statecharts,” Proc. Second Int'l Conf. Requirements Eng. (ICRE '96), pp. 86–93, Apr. 1996.
[8] W. Chan, R.J. Anderson, P. Beame, and D. Notkin, "Improving Efficiency of Symbolic Model Checking for State-Based System Requirements," M. Young, ed., ISSTA'98: Proc. ACM SIGSOFT Int'l Symp. Software Testing and Analysis, pp. 102-112,Clearwater Beach, Fla., Mar. 1998. Also published as Software Engineering Notes, vol. 23, no. 2, Mar. 1998.
[9] W. Chan, R.J. Anderson, P. Beame, D.H. Jones, D. Notkin, and W.E. Warner, “Decoupling Synchronization from Logic for Efficient Symbolic Model Checking of Statecharts,” Proc. 1999 Int'l Conf. Software Eng. (ICSE '99), pp. 142–151, May 1999.
[10] D. Harel and A. Naamad, "The STATEMATE Semantics of Statecharts," ACM Trans. Software Eng. and Methodology, vol. 5, no. 4, pp. 293-333, Oct. 1996.
[11] G. Berry and G. Gonthier, "The ESTERELSynchronous Programming Language: Design, Semantics, Implementation," Science of Computer Programming, vol. 19, no. 2, pp. 87-152, 1992.
[12] E.M. Clarke and E.A. Emerson, "Synthesis of synchronization skeletons for branching time temporal logic," Logic of Programs: Workshop, Lecture notes in Computer Science. vol. 131. Yorktown Heights, N. Y.: Springer-Verlag, May 1981.
[13] K.L. McMillan, Symbolic Model Checking. Kluwer Academic, 1993.
[14] J. Crow and B. Di Vito, “Formalizing Space Shuttle Software Requirements: Four Case Studies,” ACM Trans. Software Eng. and Methodology, vol. 7, pp. 296–332, July 1998.
[15] M.P. Heimdahl and N.G. Leveson, "Completeness and Consistency in Hierarchical State-Based Requirements," IEEE Trans. Software Eng., pp. 363-377, vol. 22, June 1996.
[16] T. Sreemani and J.M. Atlee, "Feasibility of Model Checking Software Requirements," Proc. 11th Ann. Conf. Computer Assurance (COMPASS'96),Gaithersburg, Md., June 1996.
[17] J.J. Britt, “Case Study: Applying Formal Methods to the Traffic Alert and Collision Avoidance System (TCAS II),” Proc. Ninth Ann. Conf. Computer Assurance (COMPASS '94), pp. 39–51, June/July 1994.
[18] N.G. Leveson, M.P.E. Heimdahl, and J.D. Reese, “Designing Specification Languages for Process Control Systems: Lessons Learned and Steps to the Future,” Proc. Software Eng.—ESEC/FSE '99, Seventh European Software Eng. Conf. Held Jointly with the Seventh ACM SIGSOFT Symp. Foundations of Software Eng., O. Nierstrasz and M. Lemoine, eds., pp. 127–145, Sept. 1999.
[19] L. Lamport, “What Good Is Temporal Logic?” Information Processing 83: Proc. IFIP Ninth World Computer Congress, R.E.A. Mason, ed., pp. 657–668, Sept. 1983.
[20] M.C. Browne, E.M. Clarke, and O. Grümberg, “Characterizing Finite Kripke Structures in Propositional Temporal Logic,” Theoretical Computer Science, vol. 59, pp. 115–131, July 1988.
[21] I. Beer, S. Ben-David, and A. Landver, “On-the-Fly Model Checking of RCTL Formulas,” Proc. Computer Aided Verification, 10th Int'l Conf. (CAV '98), A.J. Hu and M.Y. Vardi, eds., pp. 184–194, June/July 1998.
[22] H. Iwashita, T. Nakata, and F. Hirose, “CTL Model Checking Based on Forward State Traversal,” Proc. Int'l Conf. Computer-Aided Design (ICCAD '96), pp. 82–87, 1996.
[23] A.J. Hu and D.L. Dill, "Efficient Verification with BDDs Using Implicitly Conjoined Invariants," Courcoubetis, ed., [13], Proc. Fifth Int'l Conf. Computer Aided Verification, pp. 3-14,Elounda, Greece, 1993.
[24] J.R. Burch, E.M. Clarke, D.E. Long, K.L. McMillan, and D.L. Dill, "Symbolic Model Checking for Sequential Circuit Verification," IEEE Trans. Computer-Aided Design of Integrated Circuits, vol. 13, no. 4, pp. 401-424, Apr. 1994.
[25] D. Geist and I. Beer, “Efficient Model Checking by Automated Ordering of Transition Relation Partitions,” Proc. Sixth Int'l Conf. Computer Aided Verification (CAV '94), D.L. Dill, ed., pp. 299–310, June 1994.
[26] R.K. Ranjan, A. Aziz, R.K. Brayton, B. Plessier, and C. Pixley, “Efficient BDD Algorithms for FSM Synthesis and Verification,” Proc. IEEE/ACM Int'l Workshop Logic Synthesis, May 1995.
[27] E.M. Clarke, R. Enders, T. Filkorn, and S. Jha, “Exploiting Symmetries in Temporal Model Logic Model Checking,” Formal Methods in System Design, vol. 9, 1996.
[28] R. Alur, R.K. Brayton, T.A. Henzinger, S. Qadeer, and S.K. Rajamani, "Partial-Order Reduction in Symbolic State Space Exploration," Proc. Ninth Int'l Computer-Aided Verification Conf., pp. 340-351,Haifa, Israel, June 1997.
[29] G. Cabodi, P. Camurati, and S. Quer, “Improved Reachability Analysis of Large Finite State Machines,” Proc. Int'l Conf. Computer-Aided Design (ICCAD '96), pp. 10–14, 1996.
[30] K. Ravi and F. Somenzi, "High-Density Reachability Analysis," Proc. Int'l Conf. Computer-Aided Design (ICCAD 95), IEEE CS Press, 1995, pp. 154-158.
[31] G. Cabodi, P. Camurati, and S. Quer, “Efficient State Space Pruning in Symbolic Backward Traversal,” Proc. IEEE Int'l Conf. Computer Design: VLSI in Computers and Processors (ICCD '94), pp. 230–235, Oct. 1994.
[32] G. Cabodi, P. Camurati, L. Lavagno, and S. Quer, “Disjunctive Partitioning and Partial Iterative Squaring: An Effective Approach for Symbolic Traversal of Large Circuits,” Proc. 34th Design Automation Conf., pp. 728–733 June 1997.
[33] B. Yang, R. Simmons, R.E. Bryant, and D.R. O'Hallaron, “Optimizing Symbolic Model Checking for Invariant-Rich Models,” Proc. Computer Aided Verification, 11th Int'l Conf. (CAV '99), N. Halbwachs and D. Peled, eds., July 1999.
[34] P. Cousot and R. Cousot, "Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints," Proc. Symp. Principles of Programming Languages, 1977.
[35] E.M. Clarke, O. Grumberg, and D.E. Long, "Model Checking and Abstraction," ACM Trans. Programming Language Systems, vol. 16, no. 5, pp. 1,512-1,542, Sept. 1994.
[36] M.P.E. Heimdahl and M.W. Whalen, “Reduction and Slicing of Hierarchical State Machines,” Proc. Software Eng.—ESEC/FSE '97: Sixth European Software Eng. Conf. Held Jointly with the Fifth ACM SIGSOFT Symp. Foundations of Software Eng., M. Jazayeri and H. Schauer, eds., pp. 450–467, Sept. 1997.
[37] R. Bharadwaj and C. Heitmeyer, "Model Checking Complete Requirements Specifications Using Abstraction," Automated Software Eng. J., vol. 6, no. 1, Jan. 1999.
[38] M. Weiser, “Program Slicing,” IEEE Trans. Software Eng., vol. 10, pp. 352–357, July 1984.
[39] S. Horwitz, T. Reps, and D. Binkley, “Interprocedural Slicing Using Dependence Graphs,” ACM Trans. Programming Languages and Systems. vol. 12, no. 1, pp. 26-60, Jan. 1990.
[40] J. Chang and D. Richardson, “Static and Dynamic Specification Slicing,” Proc. Fourth Irvine Software Symp., Apr. 1994.
[41] IEEE/ACM Int'l Conf. Computer-Aided Design, Digest of Technical Papers, Nov. 1996.

Index Terms:
Formal verification, symbolic model checking, binary decision diagrams, requirements specifications, statecharts, RSML, TCAS II, partitioned transition relation, automatic abstraction, fault tolerance, avionic systems.
Citation:
William Chan, Richard J. Anderson, Paul Beame, David H. Jones, David Notkin, William E. Warner, "Optimizing Symbolic Model Checking for Statecharts," IEEE Transactions on Software Engineering, vol. 27, no. 2, pp. 170-190, Feb. 2001, doi:10.1109/32.908961
Usage of this product signifies your acceptance of the Terms of Use.