Addressing Unbounded Parallelism in Verification of Software Components

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985807%3A_____%2F06%3A00083270" target="_blank" >RIV/67985807:_____/06:00083270 - isvavai.cz</a>

Result on the web

—

DOI - Digital Object Identifier

—

Result language

angličtina

Original language name

Addressing Unbounded Parallelism in Verification of Software Components

Original language description

To use verification tools for reliability analysis of a software component, it is desirable to specify the behavior of the component by a finite-state model. This is often impossible at design time if the component practices unbounded parallelism. In that case, the behavior of the component widely depends on the environment the component is instantiated in. Unfortunately, covering all possible environments results in an infinite-state model. In this paper, we introduce a solution based on the concept oftemplate-to-model transformation: at design time, a developer describes the behavior of the component by a behavior template, which is automatically transformed into a concrete behavior model when the component is instantiated in an environment. As theconcrete behavior model is finite-state, it is a suitable input for verification tools.

Czech name

Řešení neomezeného paralelismu při verifikaci softwarových komponent

Czech description

Aby se daly použít verifikační nástroje pro analýzu spolehlivosti softwarových komponent, je nutné specifikovat chování komponent pomocí konečně-stavového modelu. To je často nemožné v době návrhu komponenty, pokud tato umožňuje neomezeně paralelní volání služeb; v takovémto případě chování komponenty silně závisí na chování prostředí, ve kterém je komponenta používána. Bohužel, snaha o zachycení chování ve všech možných prostředích zpravidla vyústí v nekonečně-stavový model. V tomto článku proto navrhujeme kompromisní řešení postavené na transformaci šablon chování v modely chování: v době návrhu komponenty je chování popsáno šablonou, která je automaticky transformována v konkrétní model chování v době použití komponenty (návrhu celé aplikace). Protože model konkrétního chování je již konečně-stavový, je vhodným vstupem pro verifikační nástroje.

Type

D - Article in proceedings

CEP classification

IN - Informatics

OECD FORD branch

—

Project

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

Continuities

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>Z - Vyzkumny zamer (s odkazem do CEZ)

Publication year

2006

Confidentiality

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

Article name in the collection

Software Engineering, Artificial Intelligence, Networking, and Parallel/Distributed Computing

ISBN

0-7695-2611-X

ISSN

—

e-ISSN

—

Number of pages

8

Pages from-to

49-56

Publisher name

IEEE Computer Society

Place of publication

Los Alamitos

Event location

Las Vegas

Event date

Jun 19, 2006

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

—