Software Model Checking Based on Game Semantics and CSP

被引：0

作者：

Dimovski, Aleksandar ^{[1
]}

Lazic, Ranko ^{[1
]}

机构：

[1] Univ Warwick, Dept Comp Sci, Coventry CV4 7AL, England

来源：

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE | 2005年 / 128卷 / 06期

基金：

英国工程与自然科学研究理事会;

关键词：

Software model checking; Game semantics; CSP process algebra; FDR refinement checker;

D O I：

10.1016/j.entcs.2005.04.007

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

We present an approach for software model checking based on game semantics and CSP. Open program fragments are compositionally modelled as CSP processes which represent their game semantics. This translation is performed by a prototype compiler. Observational equivalence and verification of properties are checked by traces refinement using the FDR tool. The effectiveness of our approach is evaluated on several examples.

引用

页码：105 / 125

页数：21

共 15 条

[1]

Abramsky S, 2004, LECT NOTES COMPUT SC, V2988, P421

[2]

Abramsky S., 2001, ALGORITHMIC GAME SEM

[3]

Abramsky S., 1997, LINEARITY SHARING ST

[4]

Appel A. W., 2002, MODERN COMPILER IMPL

[5] The SLAM project: Debugging system software via static analysis [J].

Ball, T ;

Rajamani, SK .

ACM SIGPLAN NOTICES, 2002, 37 (01) :1-3

[6]

Clarke EM., 2001, MODEL CHECKING

[7]

Dimovski A., 2004, LNCS

[8]

Farias A, 2004, LECT NOTES COMPUT SC, V2999, P108

[9]

Formal Systems (Europe) Ltd, 2000, FAIL DIV REF FDR2 MA

[10] The regular-language semantics of second-order idealized ALGOL [J].

Ghica, DR ;

McCusker, G .

THEORETICAL COMPUTER SCIENCE, 2003, 309 (1-3) :469-502

← 1 2 →