Tutorial: Parallel Model Checking

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F07%3A00020381" target="_blank" >RIV/00216224:14330/07:00020381 - isvavai.cz</a>

Result on the web

—

DOI - Digital Object Identifier

—

Result language

angličtina

Original language name

Tutorial: Parallel Model Checking

Original language description

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 relevan

Czech name

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

Czech description

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í modeluse 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.

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

2007

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

Model Checking Software

ISBN

978-3-540-73369-0

ISSN

0302-9743

e-ISSN

—

Number of pages

2

Pages from-to

—

Publisher name

Springer-Verlag

Place of publication

Berlin, Heidelberg

Event location

Berlin, Germany

Event date

Jan 1, 2007

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

000247906900002