Action Language Verifier

Author

Bultan, Tevfik ; Yavuz-Kahveci, Tuba

Author_Institution

Dept. of Comput. Sci., California Univ., Santa Barbara, CA, USA

fYear

2001

fDate

26-29 Nov. 2001

Firstpage

382

Lastpage

386

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.

Keywords

binary decision diagrams; compiler generators; decidability; formal specification; program verification; specification languages; Action Language Verifier; Action Language specifications; BDD manipulator; CTL properties; Composite Symbolic Library; Presburger arithmetic manipulator; boolean types; compiler; composite symbolic representations; decidability; enumerated types; heuristics; infinite-state symbolic model checker; model checking queries; multiple variable types; reactive software systems; specification language; symbolic manipulator; unbounded integer variables; Arithmetic; Binary decision diagrams; Computer science; Formal specifications; Object oriented modeling; Software libraries; Software systems; Specification languages; Switches; Thyristors;

fLanguage

English

Publisher

ieee

Conference_Titel

Automated Software Engineering, 2001. (ASE 2001). Proceedings. 16th Annual International Conference on

ISSN

1938-4300

Print_ISBN

0-7695-1426-X

Type

conf

DOI

10.1109/ASE.2001.989834

Filename

989834