Detailed Information on Publication Record
2007
Tutorial: Parallel Model Checking
BRIM, Luboš and Jiří BARNATBasic information
Original name
Tutorial: Parallel Model Checking
Name in Czech
Úvod do paralelního ověřování modelu
Authors
BRIM, Luboš (203 Czech Republic, guarantor) and Jiří BARNAT (203 Czech Republic)
Edition
Berlin, Heidelberg, Model Checking Software, p. 2-3, 2 pp. 2007
Publisher
Springer-Verlag
Other information
Language
English
Type of outcome
Stať ve sborníku
Field of Study
10201 Computer sciences, information science, bioinformatics
Country of publisher
Germany
Confidentiality degree
není předmětem státního či obchodního tajemství
Impact factor
Impact factor: 0.402 in 2005
RIV identification code
RIV/00216224:14330/07:00020381
Organization unit
Faculty of Informatics
ISBN
978-3-540-73369-0
ISSN
UT WoS
000247906900002
Keywords in English
LTL Parallel Model Checking
Tags
International impact, Reviewed
Změněno: 2/6/2009 10:46, prof. RNDr. Jiří Barnat, Ph.D.
V originále
With the increase in the complexity of computer systems, it becomes even more important to develop formal methods for ensuring their quality. Various techniques for automated and semi-automated analysis and verification have been proposed. In particular, model-checking has become a very practical technique due to its push-button character. The basic principle behind model-checking is to build a model of the system under consideration together with a formal description of the verified property in a suitable temporal logic. The model-checking algorithm is a decision procedure which in addition to the yes/no answer returns a trace of a faulty behaviour in case the checked property is not satisfied by the model. One of the additional advantages of this approach is that verification can be performed against partial specifications, by considering only a subset of all specification requirements. This allows for increased efficiency by checking correctness with respect to only the most relevant requirements that should be fulfilled.
In Czech
S rostoucí složitostí komplexity počítačových systémů se stále důležitější vyvíjet metody pro ověřování jejich kvalit. Byly navženy různé techniky pro (polo-)automatizovanou analýzu a verifikaci těchto systémů, konkrétně například metoda ověřování modelu se jeví jako velmi použitelná v praxi. Hlavní myšlenkou metody je vytvořit model popisující daný systém a ověrit chování tohoto modelu. Ověřovací procedura je výpočetně náročná a tak jeden z možných přístupů k její realizaci je použití agregované síly paralelních systémů. Tento tutoriál dává přehlad základních technik použitých v paralelizaci ověřovací procedury.
Links
| GA201/06/1338, research and development project |
| ||
| MSM0021622419, plan (intention) |
| ||
| 1M0545, research and development project |
|