Model Checking of Control-User Component-Based Parametrised Systems

MORAVCOVÁ VAŘEKOVÁ, Pavlína and Ivana ČERNÁ. Model Checking of Control-User Component-Based Parametrised Systems. In Lecture Notes in Computer Science 5282. Germany: Springer Verlag, 2008, p. 146-162. ISBN 978-3-540-87890-2.

Basic information

• Original name: Model Checking of Control-User Component-Based Parametrised Systems
• Name in Czech: Model checking parametrizovaných komponentových systémů s kontroler-user architekturou
• Authors: MORAVCOVÁ VAŘEKOVÁ, Pavlína (203 Czech Republic, guarantor) and Ivana ČERNÁ (203 Czech Republic).
• Edition: Germany, Lecture Notes in Computer Science 5282, p. 146-162, 17 pp. 2008.
• Publisher: Springer Verlag

Other information

• Original language: English
• Type of outcome: Proceedings paper
• Field of Study: 10201 Computer sciences, information science, bioinformatics
• Country of publisher: Germany
• Confidentiality degree: is not subject to a state or trade secret
• RIV identification code: RIV/00216224:14330/08:00024313
• Organization unit: Faculty of Informatics
• ISBN: 978-3-540-87890-2
• UT WoS: 000261030000010
• Keywords in English: parametrised systems; formal verification; Client-Server systems; component-based system analysis
• Tags: Client-Server systems, component-based system analysis, formal verification, parametrised systems
• Tags: International impact, Reviewed

Abstract

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.

Abstract (in Czech)

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é.

Links

• MSM0021622419, plan (intention): Name: Vysoce paralelní a distribuované výpočetní systémy

Investor: Ministry of Education, Youth and Sports of the CR, Highly Parallel and Distributed Computing Systems

• 1ET400300504, research and development project: Name: Realistická aplikace formálních metod v komponentových systémech

Investor: Academy of Sciences of the Czech Republic, Realistic application of formal methods in component systems

• 1ET408050503, research and development project: Name: Techniky automatické verifikace a validace softwarových a hardwarových systémů

Investor: Academy of Sciences of the Czech Republic, Techniques for automatic verification and validation of software nad hardware systems

• 1M0545, research and development project: Name: Institut Teoretické Informatiky

Investor: Ministry of Education, Youth and Sports of the CR, Institute for Theoretical Computer Science