A Model Checker for Bigraphs

Gian David Perrone; Søren Debois; Thomas Hildebrandt

doi:10.1145/2245276.2231985

A Model Checker for Bigraphs

Gian David Perrone
, Søren Debois
, Thomas Hildebrandt

Programming Logic and Semantics

Research output: Conference Article in Proceeding or Book/Report chapter › Article in proceedings › Research › peer-review

Abstract

We present a model checking tool for Bigraphical Reactive Systems that may be instantiated as a model checker for any formalism or domain-specific modelling language encoded as a Bigraphical Reactive System. We describe the implementation of the tool, and how it can be used to verify correctness properties of some infinite-state models by applying a static analysis to reaction rules that permits the exclusion of some infinite branches of execution shown to always be free of violations. We give a proof of correctness for this method, and illustrate the usage of the tool with two examples — a textbook implementation of the Dining Philosophers prob- lem, and an example motivated by a ubiquitous computing application.

Original language	English
Title of host publication	SAC '12. Proceedings of the 27th Annual ACM Symposium on Applied Computing
Place of Publication	New York, NY, USA
Publisher	Association for Computing Machinery
Publication date	Mar 2012
Pages	1320-1325
ISBN (Print)	978-1-4503-0857-1
DOIs	https://doi.org/10.1145/2245276.2231985
Publication status	Published - Mar 2012
Event	ACM Symposium on Applied Computing 2012 - Riva del Garda, Italy Duration: 26 Mar 2012 → 30 Mar 2012 Conference number: 27th http://www.acm.org/conferences/sac/sac2012/

Conference

Conference	ACM Symposium on Applied Computing 2012
Number	27th
Country/Territory	Italy
City	Riva del Garda
Period	26/03/2012 → 30/03/2012
Internet address	http://www.acm.org/conferences/sac/sac2012/

Keywords

Model Checking
Bigraphical Reactive Systems
Formal Verification
Infinite-State Models
Static Analysis

Access to Document

10.1145/2245276.2231985

Cite this

@inproceedings{fc0d85e2570a4bf4b7ce6f002e5c397f,

title = "A Model Checker for Bigraphs",

abstract = "We present a model checking tool for Bigraphical Reactive Systems that may be instantiated as a model checker for any formalism or domain-specific modelling language encoded as a Bigraphical Reactive System. We describe the implementation of the tool, and how it can be used to verify correctness properties of some infinite-state models by applying a static analysis to reaction rules that permits the exclusion of some infinite branches of execution shown to always be free of violations. We give a proof of correctness for this method, and illustrate the usage of the tool with two examples — a textbook implementation of the Dining Philosophers prob- lem, and an example motivated by a ubiquitous computing application.",

keywords = "Model Checking, Bigraphical Reactive Systems, Formal Verification, Infinite-State Models, Static Analysis, Model Checking, Bigraphical Reactive Systems, Formal Verification, Infinite-State Models, Static Analysis",

author = "Perrone, \{Gian David\} and S{\o}ren Debois and Thomas Hildebrandt",

year = "2012",

month = mar,

doi = "10.1145/2245276.2231985",

language = "English",

isbn = "978-1-4503-0857-1",

pages = "1320--1325",

booktitle = "SAC '12. Proceedings of the 27th Annual ACM Symposium on Applied Computing",

publisher = "Association for Computing Machinery",

address = "United States",

note = "ACM Symposium on Applied Computing 2012, SAC 2012 ; Conference date: 26-03-2012 Through 30-03-2012",

url = "http://www.acm.org/conferences/sac/sac2012/",

}

TY - GEN

T1 - A Model Checker for Bigraphs

AU - Perrone, Gian David

AU - Debois, Søren

AU - Hildebrandt, Thomas

N1 - Conference code: 27th

PY - 2012/3

Y1 - 2012/3

N2 - We present a model checking tool for Bigraphical Reactive Systems that may be instantiated as a model checker for any formalism or domain-specific modelling language encoded as a Bigraphical Reactive System. We describe the implementation of the tool, and how it can be used to verify correctness properties of some infinite-state models by applying a static analysis to reaction rules that permits the exclusion of some infinite branches of execution shown to always be free of violations. We give a proof of correctness for this method, and illustrate the usage of the tool with two examples — a textbook implementation of the Dining Philosophers prob- lem, and an example motivated by a ubiquitous computing application.

AB - We present a model checking tool for Bigraphical Reactive Systems that may be instantiated as a model checker for any formalism or domain-specific modelling language encoded as a Bigraphical Reactive System. We describe the implementation of the tool, and how it can be used to verify correctness properties of some infinite-state models by applying a static analysis to reaction rules that permits the exclusion of some infinite branches of execution shown to always be free of violations. We give a proof of correctness for this method, and illustrate the usage of the tool with two examples — a textbook implementation of the Dining Philosophers prob- lem, and an example motivated by a ubiquitous computing application.

KW - Model Checking

KW - Bigraphical Reactive Systems

KW - Formal Verification

KW - Infinite-State Models

KW - Static Analysis

KW - Model Checking

KW - Bigraphical Reactive Systems

KW - Formal Verification

KW - Infinite-State Models

KW - Static Analysis

U2 - 10.1145/2245276.2231985

DO - 10.1145/2245276.2231985

M3 - Article in proceedings

SN - 978-1-4503-0857-1

SP - 1320

EP - 1325

BT - SAC '12. Proceedings of the 27th Annual ACM Symposium on Applied Computing

PB - Association for Computing Machinery

CY - New York, NY, USA

T2 - ACM Symposium on Applied Computing 2012

Y2 - 26 March 2012 through 30 March 2012

ER -

A Model Checker for Bigraphs

Abstract

Conference

Keywords

Access to Document

Fingerprint

Cite this