A verification environment for bigraphs

Bidragets oversatte titel: Et verifikationsmiljø for bigrafer

Gian David Perrone, Søren Debois, Thomas Hildebrandt

Publikation: Artikel i tidsskrift og konference artikel i tidsskriftTidsskriftartikelForskningpeer review


We present the BigMC tool for bigraphical reactive systems that may be instantiated as a verification tool for any formalism or domain-specific modelling language encoded as a bigraphical reactive system. We introduce the syntax and use of BigMC, and exemplify its use with two small examples: a textbook “philosophers” example, and an example motivated by a ubiquitous computing application. We give a tractable heuristic with which to approximate interference between reaction rules, and prove this analysis to be safe. We provide a mechanism for state reachability checking of bigraphical reactive systems, based upon properties expressed in terms of matching, and describe a checking algorithm that makes use of the causation heuristic.
Bidragets oversatte titelEt verifikationsmiljø for bigrafer
TidsskriftInnovations in Systems and Software Engineering
Udgave nummer2
Sider (fra-til)95-104
StatusUdgivet - 2013


  • Bigraphs
  • Reactive Systems
  • Reachability analysis
  • Domain-specific modelling languages