State Generation in the PARMC Model Checker
- 215 Downloads
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.
KeywordsModel Check Temporal Logic Parallel Composition Reachable State Sequential Component
Unable to display preview. Download preview PDF.
- 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
- Y. Dong and C. R. Ramakrishnan. An optimizing compiler for efficient model checking. In Proceeding of FORTE/PSTV’ 99, 1999.Google Scholar
- 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.
- 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
- O. Kaser. PARMC. http://rockwood.csd.unbsj.ca/~owen/research/parmc.
- R. Milner. Communication and Concurrency. Prentice-Hall, 1989.Google Scholar
- 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
- 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
- A. Roychoudhury, C. R. Ramakrishnan, and I. V. Ramakrishnan. Justifying proofs using memo tables. In PPDP’00, pages 178–189, 2000.Google Scholar
- C. Seger. Combining functionalp rogramming and hardware verification. In ICFP’00, 2000.Google Scholar
- The XMC group. XMC v1.0.2. http://www.cs.sunysb.edu/~lmc, 2000.
- The XSB group. XSB v2.1. //www.cs.sunysb.edu/~sbprolog, 2000.