Perrone, Gian David1; Debois, Søren3; Hildebrandt, Thomas3
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 Department6 Computer Science, IT University of Copenhagen
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