D 2009

EMMA: Explicit Model Checking Manager (Tool Presentation)

PELÁNEK, Radek and Václav ROSECKÝ

Basic information

Original name

EMMA: Explicit Model Checking Manager (Tool Presentation)

Name in Czech

EMMA: Manažer explicitního ověřování modelů (prezentace nástroje)

Authors

PELÁNEK, Radek (203 Czech Republic, guarantor, belonging to the institution) and Václav ROSECKÝ (203 Czech Republic)

Edition

Německo, Model Checking Software, p. 169-173, 5 pp. 2009

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

France

Confidentiality degree

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

Publication form

printed version "print"

Impact factor

Impact factor: 0.402 in 2005

RIV identification code

RIV/00216224:14330/09:00065860

Organization unit

Faculty of Informatics

ISBN

978-3-642-02651-5

ISSN

DOI

UT WoS

000268327800011

Keywords in English

model checking; evaluation; tool

Tags

International impact, Reviewed
Změněno: 30/4/2014 05:53, RNDr. Pavel Šmerk, Ph.D.

Abstract

ORIG CZ

V originále

Although model checking is usually described as an automatic technique, the verification process with the use of model checker is far from being fully automatic. In this paper we elaborate on concept of a verification manager, which contributes to automation of the verification process by enabling efficient parallel combination of different verification techniques. We introduce a tool EMMA (Explicit Model checking MAnager), which is a practical realization of the concept, and discuss practical experience with the tool.

In Czech

Metoda ověřování modelu je většinou popisována jako automatická metoda; v praxi však použití této metody není zdaleka plně automatické. V tomto příspěvku rozebíráme koncept verifikačního manažera, který přispívá k automatizaci verifikace prostřednictvím automatického paralelního spouštění velkého množství verifikačních technik. Popisujeme praktickou realizaci tohoto konceptu (nástroj EMMA) a diskutujeme praktické zkušenosti s použitím nástroje.

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