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

Publikation: Konference artikel i Proceeding eller bog/rapport kapitel › Konferencebidrag i proceedings › Forskning › 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.

Originalsprog	Engelsk
Titel	SAC '12. Proceedings of the 27th Annual ACM Symposium on Applied Computing
Udgivelsessted	New York, NY, USA
Forlag	Association for Computing Machinery
Publikationsdato	mar. 2012
Sider	1320-1325
ISBN (Trykt)	978-1-4503-0857-1
DOI	https://doi.org/10.1145/2245276.2231985
Status	Udgivet - mar. 2012
Begivenhed	ACM Symposium on Applied Computing 2012 - Riva del Garda, Italien Varighed: 26 mar. 2012 → 30 mar. 2012 Konferencens nummer: 27th http://www.acm.org/conferences/sac/sac2012/

Konference

Konference	ACM Symposium on Applied Computing 2012
Nummer	27th
Land/Område	Italien
By	Riva del Garda
Periode	26/03/2012 → 30/03/2012
Internetadresse	http://www.acm.org/conferences/sac/sac2012/

Adgang til dokumentet

10.1145/2245276.2231985

Citationsformater

@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",

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/",

}

A Model Checker for Bigraphs. / Perrone, Gian David; Debois, Søren; Hildebrandt, Thomas.
SAC '12. Proceedings of the 27th Annual ACM Symposium on Applied Computing. New York, NY, USA: Association for Computing Machinery, 2012. s. 1320-1325.

Publikation: Konference artikel i Proceeding eller bog/rapport kapitel › Konferencebidrag i proceedings › Forskning › peer review

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

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

Konference

Adgang til dokumentet

Fingeraftryk

Citationsformater