Tutorial: Parallel Model Checking

BRIM, Luboš a Jiří BARNAT. Tutorial: Parallel Model Checking. In Model Checking Software. Berlin, Heidelberg: Springer-Verlag, 2007, s. 2-3. ISBN 978-3-540-73369-0.

Základní údaje

Originální název

Tutorial: Parallel Model Checking

Název česky

Úvod do paralelního ověřování modelu

Autoři

BRIM, Luboš (203 Česká republika, garant) a Jiří BARNAT (203 Česká republika)

Vydání

Berlin, Heidelberg, Model Checking Software, od s. 2-3, 2 s. 2007

Nakladatel

Springer-Verlag

---

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Německo

Utajení

není předmětem státního či obchodního tajemství

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/07:00020381

Organizační jednotka

Fakulta informatiky

ISBN

978-3-540-73369-0

ISSN

UT WoS

000247906900002

Klíčová slova anglicky

LTL Parallel Model Checking

Štítky

LTL Parallel Model Checking

Příznaky

Mezinárodní význam, Recenzováno

---

Anotace

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.

Česky

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.

---

Návaznosti

GA201/06/1338, projekt VaV	Název: Automatizovaná verifikace softwaru Investor: Grantová agentura ČR, Automatizovaná verifikace softwaru
MSM0021622419, záměr	Název: Vysoce paralelní a distribuované výpočetní systémy Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Vysoce paralelní a distribuované výpočetní systémy
1M0545, projekt VaV	Název: Institut Teoretické Informatiky Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky