kirancodes.me
To Proof Maintenance & Beyond!
ASE 2001

Action Language Verifier

Tevfik Bultan, Tuba Yavuz-Kahveci

DOI 10.1109/ase.2001.989834dblp

Abstract

Action Language is a specification language for reactive software systems. We present the Action Language Verifier which consists of: 1) a compiler that converts Action Language specifications to composite symbolic representations, and 2) an infinite-state symbolic model checker which verifies (or falsifies) CTL properties of Action Language specifications. Our symbolic manipulator (Composite Symbolic Library) combines a BDD manipulator (for boolean and enumerated types) and a Presburger arithmetic manipulator (for integers) to handle multiple variable types. Since we allow unbounded integer variables, model checking queries become undecidable. We present several heuristics used by the Action Language Verifier to achieve convergence.

BibTeX
@inproceedings{Bultan-YavuzKahveci:ASE01,
  author    = {Tevfik Bultan and
               Tuba Yavuz{-}Kahveci},
  title     = {Action Language Verifier},
  booktitle = {ASE},
  pages     = {382--386},
  publisher = {{IEEE} Computer Society},
  year      = {2001},
}

Related papers