A verification environment for bigraphs
Research output: Contribution to journal › Journal article › Research › peer-review
Standard
A verification environment for bigraphs. / Perrone, Gian David; Debois, Søren; Hildebrandt, Thomas.
In: Innovations in Systems and Software Engineering, Vol. 9, No. 2, 2013, p. 95-104.Research output: Contribution to journal › Journal article › Research › peer-review
Harvard
APA
Vancouver
Author
Bibtex
}
RIS
TY - JOUR
T1 - A verification environment for bigraphs
AU - Perrone, Gian David
AU - Debois, Søren
AU - Hildebrandt, Thomas
PY - 2013
Y1 - 2013
N2 - 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.
AB - 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.
U2 - 10.1007/s11334-013-0210-2
DO - 10.1007/s11334-013-0210-2
M3 - Journal article
VL - 9
SP - 95
EP - 104
JO - Innovations in Systems and Software Engineering
JF - Innovations in Systems and Software Engineering
SN - 1614-5046
IS - 2
ER -
ID: 227990342