Počet záznamů: 1

Assume-Guarantee Verification of Software Components in SOFA 2 Framework

  1. 1.
    0334355 - UIVT-O 2011 RIV GB eng J - Článek v odborném periodiku
    Parízek, P. - Plášil, František
    Assume-Guarantee Verification of Software Components in SOFA 2 Framework.
    [Verifikace softwarových komponent ve frameworku SOFA 2 způsobem assume-guarantee.]
    IET Software. Roč. 4, č. 3 (2010), s. 210-221 ISSN 1751-8806
    Grant CEP: GA AV ČR 1ET400300504
    Grant ostatní: GA MŠk(CZ) 7E08004
    Výzkumný záměr: CEZ:AV0Z10300504
    Klíčová slova: components * software verification * model checking
    Kód oboru RIV: JC - Počítačový hardware a software
    Impakt faktor: 0.671, rok: 2010

    A key problem in compositional model checking of software systems is that typical model checkers accept only closed systems (runnable programs) and therefore a component cannot be model-checked directly. A typical solution is to create an artificial environment for the component such that composition of them forms a runnable program that can be model-checked. While it is possible to create a universal environment that performs all possible sequences and interleavings of calls of the component’s methods, for practical purposes it is sufficient to capture in this way just the use of the component in a particular software system – this idea is expressed by the paradigm of assume-guarantee reasoning. In this paper, we present our approach to assume-guarantee-based verification of software systems in the context of the SOFA 2 component framework.

    Klíčový problém v modulárním model checkingu softwarových systémů je to, že typické model checkery akceptují pouze uzavřené systémy (spustitelné programy) a proto není možné použít model checking na komponentu přímo. Typické řešení je vytvoření umělého prostředí pro komponentu tak, že jejich složení tvoří spustitelný program, který může být ověřen pomocí model checkingu. Přestože je možné vytvořit univerzální prostředí, které provádí všechny možné sekvence a proložení volání metod komponenty, pro praktické účely stačí zachytit jen použití komponenty v konkrétním softwarovém systému - tato myšlenka je vyjádřena paradigmatem assume-guarantee. V tomto článku prezentujeme náš přístup k verifikaci softwarových systémů podle paradigmatu assume-guarantee v kontextu komponentového frameworku SOFA 2. Poskytujeme přehled našeho přístupu ke konstrukci umělého prostředí pro verifikaci SOFA 2 komponent implementovaných v jazyce Java s model checkerem Java PathFinder.
    Trvalý link: http://hdl.handle.net/11104/0179113