PELÁNEK, Radek a Václav ROSECKÝ. EMMA: Explicit Model Checking Manager (Tool Presentation). Online. In Model Checking Software. Německo: Springer, 2009. s. 169-173. ISBN 978-3-642-02651-5. Dostupné z: https://dx.doi.org/10.1007/978-3-642-02652-2_15. [citováno 2024-04-23]
Další formáty:   BibTeX LaTeX RIS
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 (203 Česká republika, garant, domácí) a Václav ROSECKÝ (203 Česká republika)
Vydání Německo, Model Checking Software, od s. 169-173, 5 s. 2009.
Nakladatel Springer
Další údaje
Originální 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
Kód RIV RIV/00216224:14330/09:00065860
Organizační jednotka Fakulta informatiky
ISBN 978-3-642-02651-5
ISSN 0302-9743
Doi http://dx.doi.org/10.1007/978-3-642-02652-2_15
UT WoS 000268327800011
Klíčová slova anglicky model checking; evaluation; tool
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 30. 4. 2014 05:53.
Anotace
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.
Anotace č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 VaVNá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 VaVNázev: Institut Teoretické Informatiky
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky
VytisknoutZobrazeno: 23. 4. 2024 18:29