Generic tools for verifying concurrent systems

被引:15
作者
Cleaveland, R [1 ]
Sims, ST
机构
[1] SUNY Stony Brook, Dept Comp Sci, Stony Brook, NY 11794 USA
[2] React Syst Inc, Falls Church, VA 22046 USA
基金
美国国家科学基金会;
关键词
specification; verification; model checking; operational semantics; process algebra; verification tools;
D O I
10.1016/S0167-6423(01)00033-8
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
Despite the enormous strides made in automatic verification technology over the past decade and a half, tools such as model checkers remain relatively underused in the development of software. One reason for this is that the bewildering array of specification and verification formalisms complicates the development and adoption by users of relevant tool support. This paper proposes a remedy to this state of affairs in the case of finite-state concurrent systems by describing an approach to developing customizable yet efficient verification tools. (C) 2002 Elsevier Science B.V. All rights reserved.
引用
收藏
页码:39 / 47
页数:9
相关论文
共 37 条
[1]  
ALUR R, 1996, LECT NOTES COMPUTER, V1102
[2]  
[Anonymous], 1997, DISTRIBUTED SYSTEMS
[3]   THE ESTEREL SYNCHRONOUS PROGRAMMING LANGUAGE - DESIGN, SEMANTICS, IMPLEMENTATION [J].
BERRY, G ;
GONTHIER, G .
SCIENCE OF COMPUTER PROGRAMMING, 1992, 19 (02) :87-152
[4]   A practical approach to implementing real-time semantics [J].
Bhat, G ;
Cleaveland, R ;
Lüttgen, G .
ANNALS OF SOFTWARE ENGINEERING, 1999, 7 :127-155
[5]   Efficient model checking via the equational mu-calculus [J].
Bhat, G ;
Cleaveland, R .
11TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 1996, :304-312
[6]  
Bhat G., 1996, LNCS, V1055, P107, DOI [10.1109/LICS.1996.561358, DOI 10.1109/LICS.1996.561358]
[7]   TRANSFORMATIONAL DESIGN AND IMPLEMENTATION OF A NEW EFFICIENT SOLUTION TO THE READY SIMULATION PROBLEM [J].
BLOOM, B ;
PAIGE, R .
SCIENCE OF COMPUTER PROGRAMMING, 1995, 24 (03) :189-220
[8]  
BLOOM B, 1995, LECT NOTES COMPUTER, V939, P16
[9]  
BLOOM B, 1988, 15TH P ACM POPL, P229
[10]  
BREBNER G, COMMUNICATION