D 2009

EMMA: Explicit Model Checking Manager (Tool Presentation)

PELÁNEK, Radek a Václav ROSECKÝ

Základní údaje

Originální název

EMMA: Explicit Model Checking Manager (Tool Presentation)

Název česky

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

Autoři

PELÁNEK, Radek a Václav ROSECKÝ

Vydání

Německo, Model Checking Software, od s. 169-173, 5 s. 2009

Nakladatel

Springer

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Francie

Utajení

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

Forma vydání

tištěná verze "print"

Impakt faktor

Impact factor: 0.402 v roce 2005

Označené pro přenos do RIV

Ano

Kód RIV

RIV/00216224:14330/09:00065860

Organizační jednotka

Fakulta informatiky

ISBN

978-3-642-02651-5

ISSN

Klíčová slova anglicky

model checking; evaluation; tool

Příznaky

Mezinárodní význam, Recenzováno
Změněno: 30. 4. 2014 05:53, RNDr. Pavel Šmerk, Ph.D.

Anotace

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.

Česky

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.

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