Three approximation techniques for ASTRAL symbolic model checking of infinite state real-time systems

Abstract

ASTRAL is a high-level formal specification language for real-time systems. It has structuring mechanisms that allow one to build modularized specifications of complex real-time systems with layering. Based upon the ASTRAL symbolic model checler reported in [13], three approximation techniques to speed-up the model checking process for use in debugging a specification are presented. The techniques are random walk, partial image and dynamic environment generation. Ten mutation tests on a railroad crossing benchmark are used to compare the performance of the techniques applied separately and in combination. The test results are presented and analyzed.

BibTeX

@inproceedings{Dang-Kemmerer:ICSE00,
  author    = {Zhe Dang and
               Richard A. Kemmerer},
  title     = {Three approximation techniques for {ASTRAL} symbolic model checking of infinite state real-time systems},
  booktitle = {ICSE},
  pages     = {345--354},
  publisher = {{ACM}},
  year      = {2000},
}

Three approximation techniques for ASTRAL symbolic model checking of infinite state real-time systems

Abstract

Related papers