Bonsai: cutting models down to size

S. Vijzelaar, K. Verstoep, W. Fokkink, H. Bal

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

2 Citations (Scopus)

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 languageEnglish
Title of host publicationPerspectives of System Informatics - 9th International Ershov Informatics Conference, PSI 2014, St. Petersburg, Russia, June 24-27, 2014. Revised Selected Papers
EditorsA Voronkov, I. Virbitskaite
Place of PublicationBerlin
PublisherSpringer
Pages361-375
Number of pages15
ISBN (Electronic)978-3-662-46823-4
ISBN (Print)978-3-662-46822-7
DOIs
Publication statusPublished - 2015
Externally publishedYes
Event9th International Ershov Informatics Conference on Perspectives of System Informatics, (PSI2014) - St. Petersburg, Russian Federation
Duration: 24 Jun 201427 Jun 2014
http://psi.iis.nsk.su/psi14/index

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume8974
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference9th International Ershov Informatics Conference on Perspectives of System Informatics, (PSI2014)
Abbreviated titlePSI2014
CountryRussian Federation
CitySt. Petersburg
Period24/06/1427/06/14
Internet address

Fingerprint Dive into the research topics of 'Bonsai: cutting models down to size'. Together they form a unique fingerprint.

Cite this