Verifikace softwarových komponent: Neomezený paralelismus

Kód výsledku v 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>

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

Verification of Software Components: Addressing Unbounded Paralelism

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Verification of Software Components: Addressing Unbounded Paralelism

Popis výsledku anglicky

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.

Druh

J_x - Nezařazeno - Článek v odborném periodiku (Jimp, Jsc a Jost)

CEP obor

JC - Počítačový hardware a software

OECD FORD obor

—

Projekt

<a href="/cs/project/1ET400300504" target="_blank" >1ET400300504: Realistická aplikace formálních metod v komponentových systémech</a><br>

Návaznosti

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

Rok uplatnění

2007

Kód důvěrnosti údajů

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

Název periodika

International Journal of Computer and Information Science

ISSN

1525-9293

e-ISSN

—

Svazek periodika

8

Číslo periodika v rámci svazku

2

Stát vydavatele periodika

US - Spojené státy americké

Počet stran výsledku

10

Strana od-do

300-309

Kód UT WoS článku

—

EID výsledku v databázi Scopus

—