ITU

A Model Checker for Bigraphs

Research output: Conference Article in Proceeding or Book/Report chapterArticle in proceedingsResearchpeer-review

View graph of relations

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 languageEnglish
Title of host publicationSAC '12. Proceedings of the 27th Annual ACM Symposium on Applied Computing
Place of PublicationNew York, NY, USA
PublisherAssociation for Computing Machinery
Publication dateMar 2012
Pages1320-1325
ISBN (Print)978-1-4503-0857-1
DOIs
Publication statusPublished - Mar 2012
EventACM Symposium on Applied Computing 2012 - Riva del Garda, Italy
Duration: 26 Mar 201230 Mar 2012
Conference number: 27th
http://www.acm.org/conferences/sac/sac2012/

Conference

ConferenceACM Symposium on Applied Computing 2012
Nummer27th
LandItaly
ByRiva del Garda
Periode26/03/201230/03/2012
Internetadresse

ID: 32340421