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

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

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

Addressing Unbounded Parallelism in Verification of Software Components

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 is a suitable input for verification tools.

Název v anglickém jazyce

Addressing Unbounded Parallelism in Verification of Software Components

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 is a suitable input for verification tools.

Druh

D - Stať ve sborníku

CEP obor

IN - Informatika

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í

2006

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 statě ve sborníku

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

ISBN

0-7695-2611-X

ISSN

—

e-ISSN

—

Počet stran výsledku

8

Strana od-do

49-56

Název nakladatele

IEEE Computer Society

Místo vydání

Los Alamitos

Místo konání akce

Las Vegas

Datum konání akce

19. 6. 2006

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—