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.
Other formats:   BibTeX LaTeX RIS
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
Original language English
Type of outcome Proceedings paper
Field of Study 10201 Computer sciences, information science, bioinformatics
Country of publisher Germany
Confidentiality degree is not subject to a state or trade secret
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
Changed by Changed by: doc. Mgr. Radek Pelánek, Ph.D., učo 4297. Changed: 23/6/2009 12:51.
Abstract
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.
Abstract (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 projectName: 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 projectName: Institut Teoretické Informatiky
Investor: Ministry of Education, Youth and Sports of the CR, Institute for Theoretical Computer Science
PrintDisplayed: 25/4/2024 11:18