Specification and Generation of Environment for Model Checking of Software Components

被引：5

作者：

Parizek, Pavel ^{[1
]}

Plasil, Frantisek ^{[2
]}

机构：

[1] Charles Univ Prague, Fac Math & Phys, Dept Software Engn, Prague, Czech Republic

[2] Acad Sci Czech Republ, Inst Comp Sci, Prague, Czech Republic

来源：

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE | 2007年 / 176卷 / 02期

关键词：

Software components; behavior protocols; model checking; automated generation of environment;

D O I：

10.1016/j.entcs.2006.02.036

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

Model checking of isolated software components is inherently not possible because a component does not form a complete program with an explicit starting point. To overcome this obstacle, it is typically necessary to create an environment of the component which is the intended subject to model checking. We present our approach to automated environment generation that is based on behavior protocols [9]; to our knowledge, this is the only environment generator designed for model checking of software components. We compare it with the approach taken in the Bandera Environment Generator tool [12], designed for model checking of sets of Java classes.

引用

页码：143 / 154

页数：12