Verification of Software Components: Addressing Unbounded Paralelism

0307947 - ÚI 2008 RIV US eng J - Journal Article
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
R&D Projects: GA AV ČR 1ET400300504
Institutional research plan: CEZ:AV0Z10300504
Keywords : software components * formal verification * unbounded parallelism
Subject RIV: JC - Computer Hardware ; 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ů.
Permanent Link: http://hdl.handle.net/11104/0160567