2008
Model Checking of Control-User Component-Based Parametrised Systems
MORAVCOVÁ VAŘEKOVÁ, Pavlína a Ivana ČERNÁZákladní údaje
Originální název
Model Checking of Control-User Component-Based Parametrised Systems
Název česky
Ověřování parametrizovaných komponentových systémú
Autoři
MORAVCOVÁ VAŘEKOVÁ, Pavlína a Ivana ČERNÁ ORCID
Vydání
Brno, Czech Republic, Technical report FIMU-RS-2008-06, 2008
Nakladatel
Faculty of Informatics, Masaryk University
Další údaje
Jazyk
angličtina
Typ výsledku
Audiovizuální tvorba
Obor
10201 Computer sciences, information science, bioinformatics
Stát vydavatele
Česká republika
Utajení
není předmětem státního či obchodního tajemství
Odkazy
Označené pro přenos do RIV
Ano
Kód RIV
RIV/00216224:14330/08:00028432
Organizační jednotka
Fakulta informatiky
Klíčová slova anglicky
componet systems - model checking - parametrisation
Příznaky
Mezinárodní význam
Změněno: 23. 6. 2009 17:10, prof. RNDr. Ivana Černá, CSc.
V originále
Many real component-based systems, so called Control-User systems, are composed of a stable part (control component) and a number of dynamic components of the same type (user components). Models of these systems are parametrised by the number of user components and thus potentially infinite. Model checking techniques can be used to verify only specific instances of the systems. This paper presents an algorithmic technique for verification of safety interaction properties of Control-User systems. The core of our verification method is a computation of a cutoff. If the system is proved to be correct for every number of user components lower than the cutoff then it is correct for any number of users. We present an on-the-fly model checking algorithm which integrates computation of a cutoff with the verification itself. Symmetry reduction can be applied during the verification to tackle the state explosion of the model. Applying the algorithm we verify models of several previously published component-based systems.
Česky
Mnohé komponentové systémy mají specifickou architekturu. Skládají se z fixní řídící části a (libovolného počtu) uživatelských komponent. Modely takových systémú jsou parametrizovány počtem uživatelských komponent a tedy potenciálně nekonečné. Ověřování je možné pro specifické instance systémů. Článek popisuje algoritmy pro verifikace vlasností bezpečnosti pro systémy vykazující symetrické chování.
Návaznosti
| 1ET400300504, projekt VaV |
|