Quo Vadis Explicit-State Model Checking

D 2015

Quo Vadis Explicit-State Model Checking

BARNAT, Jiří

Basic information

Original name

Quo Vadis Explicit-State Model Checking

Authors

BARNAT, Jiří (203 Czech Republic, guarantor, belonging to the institution)

Edition

Neuveden, SOFSEM 2015: Theory and Practice of Computer Science - 41st International Conference on Current Trends in Theory and Practice of Computer Science, p. 46-57, 12 pp. 2015

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

Czech Republic

Confidentiality degree

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

Publication form

printed version "print"

References:

http://dx.doi.org/10.1007/978-3-662-46078-8_5

Impact factor

Impact factor: 0.402 in 2005

RIV identification code

RIV/00216224:14330/15:00082654

Organization unit

Faculty of Informatics

ISBN

978-3-662-46077-1

ISSN

DOI

http://dx.doi.org/10.1007/978-3-662-46078-8_5

Keywords in English

explicit-state model checking

Změněno: 3/5/2016 11:10, RNDr. Pavel Šmerk, Ph.D.

Abstract

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.

Links

7H13001, research and development project

Name: Critical System Engineering Acceleration (Acronym: CRYSTAL (MSMT))

Investor: Ministry of Education, Youth and Sports of the CR

Citovat

BARNAT, Jiří. Quo Vadis Explicit-State Model Checking. In Giuseppe F. Italiano and Tiziana Margaria-Steffen and Jaroslav Pokorný and Jean-Jacques Quisquater and Roger Wattenhofer. SOFSEM 2015: Theory and Practice of Computer Science - 41st International Conference on Current Trends in Theory and Practice of Computer Science. Neuveden: Springer, 2015, p. 46-57. ISBN 978-3-662-46077-1. Available from: https://dx.doi.org/10.1007/978-3-662-46078-8_5.

@inproceedings{1297139,
   author = {Barnat, Jiří},
   address = {Neuveden},
   booktitle = {SOFSEM 2015: Theory and Practice of Computer Science - 41st International Conference on Current Trends in Theory and Practice of Computer Science},
   doi = {http://dx.doi.org/10.1007/978-3-662-46078-8_5},
   editor = {Giuseppe F. Italiano and Tiziana Margaria-Steffen and Jaroslav Pokorný and Jean-Jacques Quisquater and Roger Wattenhofer},
   keywords = {explicit-state model checking},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Neuveden},
   isbn = {978-3-662-46077-1},
   pages = {46-57},
   publisher = {Springer},
   title = {Quo Vadis Explicit-State Model Checking},
   url = {http://dx.doi.org/10.1007/978-3-662-46078-8_5},
   year = {2015}
}

TY  - JOUR
ID  - 1297139
AU  - Barnat, Jiří
PY  - 2015
TI  - Quo Vadis Explicit-State Model Checking
PB  - Springer
CY  - Neuveden
SN  - 9783662460771
KW  - explicit-state model checking
UR  - http://dx.doi.org/10.1007/978-3-662-46078-8_5
L2  - http://dx.doi.org/10.1007/978-3-662-46078-8_5
N2  - 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.
ER  -

BARNAT, Jiří. Quo Vadis Explicit-State Model Checking. In Giuseppe F. Italiano and Tiziana Margaria-Steffen and Jaroslav Pokorný and Jean-Jacques Quisquater and Roger Wattenhofer. \textit{SOFSEM 2015: Theory and Practice of Computer Science - 41st International Conference on Current Trends in Theory and Practice of Computer Science}. Neuveden: Springer, 2015, p.~46-57. ISBN~978-3-662-46077-1. Available from: https://dx.doi.org/10.1007/978-3-662-46078-8\_{}5.

Detailed Information on Publication Record