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%3A00028432" target="_blank" >RIV/00216224:14330/08:00028432 - 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.
Czech name
—
Czech description
—

Project
<a href="/en/project/1ET400300504" target="_blank" >1ET400300504: Realistic application of formal methods in component systems</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

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

Similar results(10)