Model Classifications and Automated Verification

PELÁNEK, Radek. Model Classifications and Automated Verification. In Formal Methods for Industrial Critical Systems. Německo: Springer, 2008, s. 149-163. ISBN 978-3-540-79706-7.

Základní údaje

Originální název

Model Classifications and Automated Verification

Název česky

Klasifikace modelů a automatická verifikace

Autoři

PELÁNEK, Radek (203 Česká republika, garant)

Vydání

Německo, Formal Methods for Industrial Critical Systems, od s. 149-163, 15 s. 2008

Nakladatel

Springer

---

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í

Kód RIV

RIV/00216224:14330/08:00024587

Organizační jednotka

Fakulta informatiky

ISBN

978-3-540-79706-7

UT WoS

000256437300010

Klíčová slova anglicky

model checking; automated verification; state space

Štítky

automated verification, Model checking, state space

Příznaky

Mezinárodní význam, Recenzováno

---

Anotace

V originále

Due to the significant progress in automated verification, there are often several techniques for a particular verification problem. In many circumstances different techniques are complementary - each echnique works well for different type of input instances. Unfortunately, it is not clear how to choose an appropriate technique for a specific instance of a problem. In this work we argue that this problem, selection of a technique and tuning its parameter values, should be considered as a standalone problem (a verification meta-search). We propose several classifications of models of asynchronous system and discuss applications of these classifications in the context of explicit finite state model checking.

Česky

Díky rozvoji automatické verifikace, existuje dnes pro většinu verifikačních problémů několik technik. V mnoha případech se tyto techniky vzájemně doplňují - každá technika pracuje dobře pro jiné instance problému. Bohužel však není jasné, jak vybrat vhodnou techniku pro specifickou vstupní instanci. V této práci zdůvodňujeme, že problém výběru vhodné techniky a nastavení parametrů, by se měl uvažovat jako samostatný problém. Navrhujeme také několik klasifikací modelů a diskutujeme jejich aplikace v kontextu explicitního ověřování modelů.

---

Návaznosti

GP201/07/P035, projekt VaV	Název: Automatická analýza modelů pomocí procházení stavového prostoru Investor: Grantová agentura ČR, Automatická analýza modelů pomocí procházení stavového prostoru
1M0545, projekt VaV	Název: Institut Teoretické Informatiky Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky