Advertisement

State Generation in the PARMC Model Checker

  • Owen Kaser
Conference paper
  • 215 Downloads
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1990)

Abstract

The PARMC system performs modelc hecking for systems described in the XL language, a variant of CCS. Extending previous work by Dong and Ramakrishnan that compiled XL specifications into an optimized transition relation, we take their transition relation and compile it into S-code, producing instructions for a new lightweight engine S that was custom designed for PARMC. Difficult constructs are handled by the XSB logic programming engine, enabling both generality (from XSB) and speed (from S). States are maintained in a compressed representation, also improving memory utilization. Experiments were performed and showed that the anticipated speed and memory improvements were achieved.

Keywords

Model Check Temporal Logic Parallel Composition Reachable State Sequential Component 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [1]
    E. M. Clarke and E. A. Emerson. Synthesis of synchronization skeletons for branching time temporall ogic. In Workshop, Logic of Programs, number 131 in LNCS. Springer-Verlag, 1981.Google Scholar
  2. [2]
    E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finitestate concurrent systems using temporall ogic specifications. ACM Trans. Prog. Lang. Syst., 8(2):244–263, 1986.zbMATHCrossRefGoogle Scholar
  3. [3]
    Y. Dong and C. R. Ramakrishnan. An optimizing compiler for efficient model checking. In Proceeding of FORTE/PSTV’ 99, 1999.Google Scholar
  4. [4]
    Y. Dong and C. R. Ramakrishnan. Logic programming optimizations for faster modelc hecking. In Workshop on Tabulation in Parsing and Deduction (TAPD’00), 2000. http://www.cs.sunysb.edu/~cram.
  5. [5]
    E. A. Emerson. Temporal and modal logics. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 997–1072. MIT Press/Elsevier, 1990.Google Scholar
  6. [6]
  7. [7]
    O. Kaser. S-machine instructions and compilation. Technical Report TR-01-001, ASCS Dept., UNBSJ, Saint John, Canada, Jan. 2001. ftp://fundy.csd.unbsj.ca/mscs/EQUALS/tr-01-001.ps.Google Scholar
  8. [8]
    K. L. McMillan. Symbolic Model Checking. Kluwer Academic, Boston, 1993.zbMATHGoogle Scholar
  9. [9]
    R. Milner. Communication and Concurrency. Prentice-Hall, 1989.Google Scholar
  10. [10]
    Y. S. Ramakrishna, C. R. Ramakrishnan, I. V. Ramakrishnan, S. A. Smolka, T. W. Swift, and D. S. Warren. Efficient model checking using tabled resolution. In CAV’97, 1997.Google Scholar
  11. [11]
    C. R. Ramakrishnan, I. V. Ramakrishnan, S. A. Smolka, Y. Dong, X. Du, A. Roychoudhury, and V. N. Venkatakrishnan. XMC: A logic-programming-based verification toolset. In CAV’00, 2000.Google Scholar
  12. [12]
    A. Roychoudhury, C. R. Ramakrishnan, and I. V. Ramakrishnan. Justifying proofs using memo tables. In PPDP’00, pages 178–189, 2000.Google Scholar
  13. [13]
    C. Seger. Combining functionalp rogramming and hardware verification. In ICFP’00, 2000.Google Scholar
  14. [14]
    The XMC group. XMC v1.0.2. http://www.cs.sunysb.edu/~lmc, 2000.
  15. [15]
    The XSB group. XSB v2.1. //www.cs.sunysb.edu/~sbprolog, 2000.

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Owen Kaser
    • 1
  1. 1.University of New BrunswickSaint JohnCanada

Personalised recommendations