Model Classifications and Automated Verification

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

Basic information

Original name

Model Classifications and Automated Verification

Name in Czech

Klasifikace modelů a automatická verifikace

Authors

PELÁNEK, Radek (203 Czech Republic, guarantor)

Edition

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

Publisher

Springer

---

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í

RIV identification code

RIV/00216224:14330/08:00024587

Organization unit

Faculty of Informatics

ISBN

978-3-540-79706-7

UT WoS

000256437300010

Keywords in English

model checking; automated verification; state space

Tags

automated verification, Model checking, state space

Tags

International impact, Reviewed

---

Abstract

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.

In Czech

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ů.

---

Links

GP201/07/P035, research and development project	Name: Automatická analýza modelů pomocí procházení stavového prostoru Investor: Czech Science Foundation, Automatic model analysis by state space exploration
1M0545, research and development project	Name: Institut Teoretické Informatiky Investor: Ministry of Education, Youth and Sports of the CR, Institute for Theoretical Computer Science