Abstract
In model checking, abstractions can cause spurious results, which need to be verified in the concrete system to gain conclusive results. Verification based on multi-valued model checking can distinguish conclusive and inconclusive results, while increasing precision over traditional two-valued over- and under-abstractions. This paper describes the theory and implementation of multi-valued model checking for Promela specifications. We believe our tool Bonsai is the first four-valued model checker capable of multi-valued verification of parallel models, i.e. consisting of multiple concurrent processes. A novel aspect is the ability to only partially abstract a model, keeping parts of it concrete.
Original language | English |
---|---|
Title of host publication | Perspectives of System Informatics - 9th International Ershov Informatics Conference, PSI 2014, St. Petersburg, Russia, June 24-27, 2014. Revised Selected Papers |
Editors | A Voronkov, I. Virbitskaite |
Place of Publication | Berlin |
Publisher | Springer |
Pages | 361-375 |
Number of pages | 15 |
ISBN (Electronic) | 978-3-662-46823-4 |
ISBN (Print) | 978-3-662-46822-7 |
DOIs | |
Publication status | Published - 2015 |
Externally published | Yes |
Event | 9th International Ershov Informatics Conference on Perspectives of System Informatics, (PSI2014) - St. Petersburg, Russian Federation Duration: 24 Jun 2014 → 27 Jun 2014 http://psi.iis.nsk.su/psi14/index |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Publisher | Springer |
Volume | 8974 |
ISSN (Print) | 0302-9743 |
ISSN (Electronic) | 1611-3349 |
Conference
Conference | 9th International Ershov Informatics Conference on Perspectives of System Informatics, (PSI2014) |
---|---|
Abbreviated title | PSI2014 |
Country/Territory | Russian Federation |
City | St. Petersburg |
Period | 24/06/14 → 27/06/14 |
Internet address |