Model Checking of Control-User Component-Based Parametrised Systems

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F08%3A00024313" target="_blank" >RIV/00216224:14330/08:00024313 - isvavai.cz</a>

Result on the web

—

DOI - Digital Object Identifier

—

Result language

angličtina

Original language name

Model Checking of Control-User Component-Based Parametrised Systems

Original language description

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 whichintegrates 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 publishe

Czech name

Model checking parametrizovaných komponentových systémů s kontroler-user architekturou

Czech description

V tomto článku se věnujeme kontroler-user parametrizovaným systémům, které vzniknou jako modely komponentových systémů. Navrhujeme dva algoritmy pro formální verifikaci toho, které stavy jsou v těchto systémech dosažitelné.

Type

D - Article in proceedings

CEP classification

IN - Informatics

OECD FORD branch

—

Project

Result was created during the realization of more than one project. More information in the Projects tab.

Continuities

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>Z - Vyzkumny zamer (s odkazem do CEZ)

Publication year

2008

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Article name in the collection

Lecture Notes in Computer Science (CBSE 2008)

ISBN

978-3-540-87890-2

ISSN

—

e-ISSN

—

Number of pages

17

Pages from-to

—

Publisher name

Springer Verlag

Place of publication

Germany

Event location

Karlsruhe

Event date

Jan 1, 2008

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

000261030000010