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
关键词
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
相关论文
共 13 条
  • [11] ROBBY M, 2003, FSE 03 FDN SOFTWARE, P267
  • [12] Automated environment generation for software model checking
    Tkachuk, O
    Dwyer, MB
    Pasareanu, CS
    [J]. 18TH IEEE INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING, PROCEEDINGS, 2003, : 116 - 127
  • [13] VISSER W, 2003, AUTOMATED SOFTWARE E, V10