2015
Quo Vadis Explicit-State Model Checking
BARNAT, JiříZákladní údaje
Originální název
Quo Vadis Explicit-State Model Checking
Autoři
BARNAT, Jiří (203 Česká republika, garant, domácí)
Vydání
Neuveden, SOFSEM 2015: Theory and Practice of Computer Science - 41st International Conference on Current Trends in Theory and Practice of Computer Science, od s. 46-57, 12 s. 2015
Nakladatel
Springer
Další údaje
Jazyk
angličtina
Typ výsledku
Stať ve sborníku
Obor
10201 Computer sciences, information science, bioinformatics
Stát vydavatele
Česká republika
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/15:00082654
Organizační jednotka
Fakulta informatiky
ISBN
978-3-662-46077-1
ISSN
Klíčová slova anglicky
explicit-state model checking
Změněno: 3. 5. 2016 11:10, RNDr. Pavel Šmerk, Ph.D.
Anotace
V originále
Model checking has always been the flag ship in the fleet of automated formal verification techniques. It has been in the center of interest of formal verification research community for more than 25 years. Focusing primarily on the well-known state space explosion problem, a decent amount of techniques and methods have been discovered and applied to push further the frontier of systems verifiable with a model checker. Still, the technique as such has not yet been matured enough to become a common part of a software development process, and its penetration into the software industry is actually much slower than it was expected. In this paper we take a closer look at the so called explicit-state model checking, we briefly recapitulate recent research achievements in the field, and report on practical experience obtained from using our explicit state model checker DIVINE. Our goal is to help the reader understand what is the current position of explicit-state model checking in general practice and what are the strengths and weaknesses of the explicit-state approach after almost three decades of research. Finally, we suggest some research directions to pursue that could shed some light on the future of this formal verification technique.
Návaznosti
7H13001, projekt VaV |
|