0307947 - ÚI 2008 RIV US eng J - Článek v odborném periodiku
Adámek, Jiří
Verification of Software Components: Addressing Unbounded Paralelism.
[Verifikace softwarových komponent: Neomezený paralelismus.]
International Journal of Computer and Information Science. Roč. 8, č. 2 (2007), s. 300-309. ISSN 1525-9293
Grant CEP: GA AV ČR 1ET400300504
Výzkumný záměr: CEZ:AV0Z10300504
Klíčová slova: software components * formal verification * unbounded parallelism
Kód oboru RIV: JC - Počítačový hardware a software

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 of template-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 the concrete behavior model is finite-state, it forms a suitable input for verification tools.

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ý, a je proto vhodným vstupem verifikačních nástrojů.
Trvalý link: http://hdl.handle.net/11104/0160567