Assume-Guarantee Verification of Software Components in SOFA 2 Framework

0334355 - ÚI 2011 RIV GB eng J - Journal Article
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. E-ISSN 1751-8814
R&D Projects: GA AV ČR 1ET400300504
Grant - others:GA MŠk(CZ) 7E08004
Institutional research plan: CEZ:AV0Z10300504
Keywords : components * software verification * model checking
Subject RIV: JC - Computer Hardware ; Software
Impact factor: 0.671, year: 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.
Permanent Link: http://hdl.handle.net/11104/0179113