Action Language Verifier

被引：15

作者：

Bultan, T ^{[1
]}

Yavuz-Kahveci, T ^{[1
]}

机构：

[1] Univ Calif Santa Barbara, Dept Comp Sci, Santa Barbara, CA 93106 USA

来源：

16TH ANNUAL INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING (ASE 2001), PROCEEDINGS | 2001年

关键词：

D O I：

10.1109/ASE.2001.989834

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

Action Language is a specification language for reactive software systems. In this paper 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.

引用

页码：382 / 386

页数：5

共 12 条

[1]

[Anonymous], MODEL CHECKING

[2]

BOIGELOT B, 1994, LECT NOTES COMPUTER, V818, P55, DOI DOI 10.1007/3-540-58179-0_

[3] Composite model-checking: Verification with type-specific symbolic representations [J].

Bultan, T ;

Gerber, R ;

League, C .

ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY, 2000, 9 (01) :3-50

[4]

Bultan T., 2000, Proceedings of the 2000 International Conference on Software Engineering. ICSE 2000 the New Millennium, P335, DOI 10.1109/ICSE.2000.870424

[5] Model-checking concurrent systems with unbounded integer variables: Symbolic representations, approximations, and experimental results [J].

Bultan, T ;

Gerber, R ;

Pugh, W .

ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1999, 21 (04) :747-789

[6]

Cousot P., 1977, P 4 ACM SIGACT SIGPL, DOI DOI 10.1145/512950.512973

[7]

Cousot P., 1978, POPL 1978, V84, P97, DOI DOI 10.1145/512760.512770

[8]

Halbwachs N., 1994, LNCS, V864

[9] STATECHARTS - A VISUAL FORMALISM FOR COMPLEX-SYSTEMS [J].

HAREL, D .

SCIENCE OF COMPUTER PROGRAMMING, 1987, 8 (03) :231-&

[10]

Heitmeyer C. L., 1996, ACM Transactions on Software Engineering and Methodology, V5, P231, DOI 10.1145/234426.234431

← 1 2 →