Bonsai: Cutting models down to size

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

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.

LanguageEnglish
Title of host publicationPerspectives of System Informatics
Subtitle of host publication9th International Ershov Informatics Conference, PSI 2014, Revised Selected Papers
EditorsIrina Virbitskaite, Andrei Voronkov, Irina Virbitskaite
PublisherSpringer - Verlag
Pages361-375
Number of pages15
ISBN (Electronic)9783662468234
ISBN (Print)9783662468227
DOIs
Publication statusPublished - 2015
Event9th International Ershov Informatics Conference on Perspectives of System Informatics, PSI 2014 - St. Petersburg, Russian Federation
Duration: 24 Jun 201427 Jun 2014

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8974
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference9th International Ershov Informatics Conference on Perspectives of System Informatics, PSI 2014
CountryRussian Federation
CitySt. Petersburg
Period24/06/1427/06/14

Fingerprint

Model checking
Model Checking
Concurrent
Model
Concretes
Specification
Specifications
Abstraction

Cite this

Vijzelaar, S. J. J., Verstoep, K., Bal, H. E., & Fokkink, W. J. (2015). Bonsai: Cutting models down to size. In I. Virbitskaite, A. Voronkov, & I. Virbitskaite (Eds.), Perspectives of System Informatics: 9th International Ershov Informatics Conference, PSI 2014, Revised Selected Papers (pp. 361-375). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8974). Springer - Verlag. https://doi.org/10.1007/978-3-662-46823-4_29
Vijzelaar, S.J.J. ; Verstoep, K. ; Bal, H.E. ; Fokkink, W.J. / Bonsai: Cutting models down to size. Perspectives of System Informatics: 9th International Ershov Informatics Conference, PSI 2014, Revised Selected Papers. editor / Irina Virbitskaite ; Andrei Voronkov ; Irina Virbitskaite. Springer - Verlag, 2015. pp. 361-375 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{aca82e0edd724c189fea33108abba7d6,
title = "Bonsai: Cutting models down to size",
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.",
author = "S.J.J. Vijzelaar and K. Verstoep and H.E. Bal and W.J. Fokkink",
year = "2015",
doi = "10.1007/978-3-662-46823-4_29",
language = "English",
isbn = "9783662468227",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer - Verlag",
pages = "361--375",
editor = "Irina Virbitskaite and Andrei Voronkov and Irina Virbitskaite",
booktitle = "Perspectives of System Informatics",

}

Vijzelaar, SJJ, Verstoep, K, Bal, HE & Fokkink, WJ 2015, Bonsai: Cutting models down to size. in I Virbitskaite, A Voronkov & I Virbitskaite (eds), Perspectives of System Informatics: 9th International Ershov Informatics Conference, PSI 2014, Revised Selected Papers. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 8974, Springer - Verlag, pp. 361-375, 9th International Ershov Informatics Conference on Perspectives of System Informatics, PSI 2014, St. Petersburg, Russian Federation, 24/06/14. https://doi.org/10.1007/978-3-662-46823-4_29

Bonsai: Cutting models down to size. / Vijzelaar, S.J.J.; Verstoep, K.; Bal, H.E.; Fokkink, W.J.

Perspectives of System Informatics: 9th International Ershov Informatics Conference, PSI 2014, Revised Selected Papers. ed. / Irina Virbitskaite; Andrei Voronkov; Irina Virbitskaite. Springer - Verlag, 2015. p. 361-375 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8974).

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

TY - GEN

T1 - Bonsai: Cutting models down to size

AU - Vijzelaar, S.J.J.

AU - Verstoep, K.

AU - Bal, H.E.

AU - Fokkink, W.J.

PY - 2015

Y1 - 2015

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84942540670&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84942540670&partnerID=8YFLogxK

U2 - 10.1007/978-3-662-46823-4_29

DO - 10.1007/978-3-662-46823-4_29

M3 - Conference contribution

SN - 9783662468227

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 361

EP - 375

BT - Perspectives of System Informatics

A2 - Virbitskaite, Irina

A2 - Voronkov, Andrei

A2 - Virbitskaite, Irina

PB - Springer - Verlag

ER -

Vijzelaar SJJ, Verstoep K, Bal HE, Fokkink WJ. Bonsai: Cutting models down to size. In Virbitskaite I, Voronkov A, Virbitskaite I, editors, Perspectives of System Informatics: 9th International Ershov Informatics Conference, PSI 2014, Revised Selected Papers. Springer - Verlag. 2015. p. 361-375. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-662-46823-4_29