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

Kód výsledku v 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>

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

Tutorial: Parallel Model Checking

Popis výsledku v původním jazyce

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

Název v anglickém jazyce

Tutorial: Parallel Model Checking

Popis výsledku anglicky

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

Druh

D - Stať ve sborníku

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

Výsledek vznikl pri realizaci vícero projektů. Více informací v záložce Projekty.

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>Z - Vyzkumny zamer (s odkazem do CEZ)

Rok uplatnění

2007

Kód důvěrnosti údajů

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

Název statě ve sborníku

Model Checking Software

ISBN

978-3-540-73369-0

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

2

Strana od-do

—

Název nakladatele

Springer-Verlag

Místo vydání

Berlin, Heidelberg

Místo konání akce

Berlin, Germany

Datum konání akce

1. 1. 2007

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

000247906900002