Specification and Generation of Environment for Model Checking of Software Components

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F07%3A00005151" target="_blank" >RIV/00216208:11320/07:00005151 - isvavai.cz</a>

Alternative codes found

RIV/67985807:_____/07:00090204

Result on the web

—

DOI - Digital Object Identifier

—

Result language

angličtina

Original language name

Specification and Generation of Environment for Model Checking of Software Components

Original language description

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 componentwhich is the intended subject to model checking. We present our approach to automated environment generation that is based on behavior protocols; 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, designed for model checking of sets of Java classes.

Czech name

Specifikace a generování prostředí pro model checking softwarových komponent

Czech description

Model checking izolovaných softwarových komponent není možný, protože komponenta netvoří kompletní program s explicitním místem začátku. Pro řešení této překážky je obvykle nutné vytvořit prostředí pro komponentu, kterou chceme ověřovat. Prezentujeme nášpřístup ke automatickému generování prostředí, který je založen na protokolech chování. Podle našich znalostí je toto jediný generátor prostředí navržený pro model checking softwarových komponent. Srovnáváme to s přístupem implementovaným v nástroji Bandera Environment Generator, který je určen pro model checking množin tříd v jazyce Java.

Type

J_x - Unclassified - Peer-reviewed scientific article (Jimp, Jsc and Jost)

CEP classification

JC - Computer hardware and software

OECD FORD branch

—

Project

<a href="/en/project/1ET400300504" target="_blank" >1ET400300504: Realistic application of formal methods in component systems</a><br>

Continuities

Z - Vyzkumny zamer (s odkazem do CEZ)

Publication year

2007

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Name of the periodical

Electronic Notes in Theoretical Computer Science

ISSN

1571-0661

e-ISSN

—

Volume of the periodical

176

Issue of the periodical within the volume

Neuveden

Country of publishing house

US - UNITED STATES

Number of pages

12

Pages from-to

143-154

UT code for WoS article

—

EID of the result in the Scopus database

—