Verification of Software Components: Addressing Unbounded Paralelism
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985807%3A_____%2F07%3A00307947" target="_blank" >RIV/67985807:_____/07:00307947 - isvavai.cz</a>
Result on the web
—
DOI - Digital Object Identifier
—
Alternative languages
Result language
angličtina
Original language name
Verification of Software Components: Addressing Unbounded Paralelism
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 forms a suitable input for verification tools.
Czech name
Verifikace softwarových komponent: Neomezený paralelismus
Czech description
Pro analýzu komponent verifikačními nástroji je vhodné popsat chování komponenty pomocí konečně-stavového modelu. To je vsak často nemožné v době návrhu komponenty, pokud tato používá neomezený paralelismus. V tomto případe totiž chování komponenty závisí na prostředí, ve kterém je komponenta používána, a pokrytí všech možných prostředí pak vede k nekonečně-stavovému modelu. V tomto článku navrhujeme řešení tohoto problému založené na myšlence transformace šablony chování na konkrétní model (template-to-model transformation): v době návrhu komponenty je chování popsáno tzv. šablonou chování, která je automaticky transformována v konkrétní model ve chvíli, kdy je komponenta nasazena v konkrétním prostředí. Tento konkrétní model je již konečně-stavový, aje proto vhodným vstupem verifikačních nástrojů.
Classification
Type
J<sub>x</sub> - Unclassified - Peer-reviewed scientific article (Jimp, Jsc and Jost)
CEP classification
JC - Computer hardware and software
OECD FORD branch
—
Result continuities
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)
Others
Publication year
2007
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Name of the periodical
International Journal of Computer and Information Science
ISSN
1525-9293
e-ISSN
—
Volume of the periodical
8
Issue of the periodical within the volume
2
Country of publishing house
US - UNITED STATES
Number of pages
10
Pages from-to
300-309
UT code for WoS article
—
EID of the result in the Scopus database
—