Perrone, Gian David1; Debois, Søren2; Hildebrandt, Thomas2
1 Programming, Logic and Semantics, Software & Systems, The Department2 Theoretical Computer Science, The Department3 Process and System Models, Software & Systems, The Department4 Pervasive Interaction Technology, Software & Systems, The Department5 Programming Logic and Semantics, Theoretical Computer Science, The Department
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.
Innovations in Systems and Software Engineering, 2013, Vol 9, Issue 2, p. 95-104
Bigraphs; Reactive Systems; Reachability analysis; Domain-specific modelling languages