A verification environment for bigraphs

Gian David Perrone; Søren Debois; Thomas Hildebrandt

doi:10.1007/s11334-013-0210-2

A verification environment for bigraphs

Gian David Perrone, Søren Debois, Thomas Hildebrandt

16 Citations (Scopus)

Abstract

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.

Translated title of the contribution	Et verifikationsmiljø for bigrafer
Original language	English
Journal	Innovations in Systems and Software Engineering
Volume	9
Issue number	2
Pages (from-to)	95-104
ISSN	1614-5046
DOIs	https://doi.org/10.1007/s11334-013-0210-2
Publication status	Published - Jun 2013
Externally published	Yes

Access to Document

10.1007/s11334-013-0210-2

Cite this

@article{6a51dc4f902b4ffa8a9ba49a1b86c3d7,

title = "A verification environment for bigraphs",

abstract = "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.",

author = "Perrone, {Gian David} and S{\o}ren Debois and Thomas Hildebrandt",

year = "2013",

month = jun,

doi = "10.1007/s11334-013-0210-2",

language = "English",

volume = "9",

pages = "95--104",

journal = "Innovations in Systems and Software Engineering",

issn = "1614-5046",

publisher = "Springer",

number = "2",

}

TY - JOUR

T1 - A verification environment for bigraphs

AU - Perrone, Gian David

AU - Debois, Søren

AU - Hildebrandt, Thomas

PY - 2013/6

Y1 - 2013/6

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

SN - 1614-5046

VL - 9

SP - 95

EP - 104

JO - Innovations in Systems and Software Engineering

JF - Innovations in Systems and Software Engineering

IS - 2

ER -