Take a look at the new version of this page: [ beta version ]. Tell us what you think.

ABSTRACT

We present various techniques for improving the time and space efficiency of symbolic model checking for system requirements specified as synchronous finite state machines. We used these techniques in our analysis of the system requirements specification of TCAS II, a complex aircraft collision avoidance system. They together reduce the time and space complexities by orders of magnitude, making feasible some analysis that was previously intractable. The TCAS II requirements were written in RSML, a dialect of state-charts.

REFERENCES

• 1: 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
• 2: J. J. Britt. Case study: Applying formal methods to the Traffic Alert and Collision Avoidance System (TCAS) II. In COMPASS'94, Proceedings of the 9th Annual Conference on Computer Assurance, pages 39-51, Gaithersburg, MD, USA, June/July 1994. IEEE.
• 3: M. C. Browne , E. M. Clarke , O. Grümberg, Characterizing finite Kripke structures in propositional temporal logic, Theoretical Computer Science, v.59 n.1-2, p.115-131, July 1988 [doi>10.1016/0304-3975(88)90098-9]
• 4: Randal E. Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, Aug. 1986 [doi>10.1109/TC.1986.1676819]
• 5: Randal E. Bryant, On the Complexity of VLSI Implementations and Graph Representations of Boolean Functions with Application to Integer Multiplication, IEEE Transactions on Computers, v.40 n.2, p.205-213, February 1991 [doi>10.1109/12.73590]
• 6: J. R. Burch, E. M. Clarke, D. E. Long, K. L. McMillan, and D. L. Dill. Symbolic model checking for sequential circuit verification. IEEE Transactions on Computer-Aided Design oflntegrated Circuits, 13(4):401-424, April 1994.
• 7: Gianpiero Cabodi , Paolo Camurati , Luciano Lavagno , Stefano Quer, Disjunctive partitioning and partial iterative squaring: an effective approach for symbolic traversal of large circuits, Proceedings of the 34th annual conference on Design automation, p.728-733, June 09-13, 1997, Anaheim, California, United States [doi>10.1145/266021.266355]
• 8: Gianpiero Cabodi , Paolo Camurati , Stefano Quer, Efficient State Space Pruning in Symbolic Backward Traversal, Proceedings of the1994 IEEE International Conference on Computer Design: VLSI in Computer & Processors, p.230-235, October 10-12, 1994
• 9: William Chan , Richard Anderson , Paul Beame , David Notkin, Combining Constraint Solving and Symbolic Model Checking for a Class of a Systems with Non-linear Constraints, Proceedings of the 9th International Conference on Computer Aided Verification, p.316-327, June 22-25, 1997
• 10: E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.244-263, April 1986 [doi>10.1145/5397.5399]
• 11: O. Coudert , C. Berthet , J. C. Madre, Verification of synchronous sequential machines based on symbolic execution, Proceedings of the international workshop on Automatic verification methods for finite state systems, p.365-373, February 1990, Grenoble, France
• 12: J. Crow and B. L. Di Vito. Formalizing space shuffle software requirements. In Proceedings of the ACM $IG$OFT Workshop on Formal Methods in Software Practice, pages 40-48, JaNuary 1996.
• 13: 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
• 14: Proceedings of the Joint 6th European Software Engineering Conference and 5th ACM $IG$OFT Symposium on the Foundations of Software Engineering, Zurich, Switzerland, September 1997.
• 15: Daniel Geist , Ilan Beer, Efficient Model Checking by Automated Ordering of Transition Relation Partitions, Proceedings of the 6th International Conference on Computer Aided Verification, p.299-310, June 21-23, 1994
• 16: 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]
• 17: David Harel , Amnon Naamad, The STATEMATE semantics of statecharts, ACM Transactions on Software Engineering and Methodology (TOSEM), v.5 n.4, p.293-333, Oct. 1996 [doi>10.1145/235321.235322]
• 18: Mats P. E. Heimdahl , Nancy G. Leveson, Completeness and Consistency in Hierarchical State-Based Requirements, IEEE Transactions on Software Engineering, v.22 n.6, p.363-377, June 1996 [doi>10.1109/32.508311]
• 19: Mats P. E. Heimdahl , Michael W. Whalen, Reduction and slicing of hierarchical state machines, Proceedings of the 6th European conference held jointly with the 5th ACM SIGSOFT international symposium on Foundations of software engineering, p.450-467, September 22-25, 1997, Zurich, Switzerland
• 20: Alan J. Hu , David L. Dill, Reducing BDD size by exploiting functional dependencies, Proceedings of the 30th international conference on Design automation, p.266-271, June 14-18, 1993, Dallas, Texas, United States [doi>10.1145/157485.164888]
• 21: Hiroaki Iwashita , Tsuneo Nakata , Fumiyasu Hirose, CTL model checking based on forward state traversal, Proceedings of the 1996 IEEE/ACM international conference on Computer-aided design, p.82-87, November 10-14, 1996, San Jose, California, United States
• 22: Robert P. Kurshan, Computer-aided verification of coordinating processes: the automata-theoretic approach, Princeton University Press, Princeton, NJ, 1994
• 23: 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]
• 24: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 25: Rosario Pugliese , Enrico Tronci, Automatic Verification of a Hydroelectric Power Plant, Proceedings of the Third International Symposium of Formal Methods Europe on Industrial Benefit and Advances in Formal Methods, p.425-444, March 18-22, 1996
• 26: R. K. Ranjan, A. Aziz, R. K. Brayton, B. Plessier, and C. Pixley. Efficient B DD algorithms for FSM synthesis and verification. In Proceedings of lEEF_./A CM International Workshop on Logic Synthesis, Lake Tahoe, USA, May 1995.
• 27: T. Sreemani and J. M. Atlee. Feasibility of model checking software requirements: A case study. In COMPASS'96, Proceedings of the l lth Annual Conference on ComputerAssurance, pages 77-88, Gaithersburg, MD, USA, June 1996. IEEE. '
• 28: Robert K. Brayton , Gary D. Hachtel , Alberto L. Sangiovanni-Vincentelli , Fabio Somenzi , Adnan Aziz , Szu-Tsung Cheng , Stephen A. Edwards , Sunil P. Khatri , Yuji Kukimoto , Abelardo Pardo , Shaz Qadeer , Rajeev K. Ranjan , Shaker Sarwary , Thomas R. Shiple , Gitanjali Swamy , Tiziano Villa, VIS: A System for Verification and Synthesis, Proceedings of the 8th International Conference on Computer Aided Verification, p.428-432, August 03, 1996

INDEX TERMS

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

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES

  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)

General Terms:
Algorithms, Languages, Performance, Verification

Keywords:
RSML, TCAS II, abstraction, binary decision diagrams, formal verification, partitioned transition relation, reachability analysis, statecharts, symbolic model checking, system requirements specification