A verification environment for bigraphs

Publikation: Bidrag til tidsskrift › Tidsskriftartikel › Forskning › fagfællebedømt

Standard

A verification environment for bigraphs. / Perrone, Gian David; Debois, Søren; Hildebrandt, Thomas.

I: Innovations in Systems and Software Engineering, Bind 9, Nr. 2, 2013, s. 95-104.

Publikation: Bidrag til tidsskrift › Tidsskriftartikel › Forskning › fagfællebedømt

Harvard

Perrone, GD, Debois, S & Hildebrandt, T 2013, 'A verification environment for bigraphs', Innovations in Systems and Software Engineering, bind 9, nr. 2, s. 95-104. https://doi.org/10.1007/s11334-013-0210-2

APA

Perrone, G. D., Debois, S., & Hildebrandt, T. (2013). A verification environment for bigraphs. Innovations in Systems and Software Engineering, 9(2), 95-104. https://doi.org/10.1007/s11334-013-0210-2

Vancouver

Perrone GD, Debois S, Hildebrandt T. A verification environment for bigraphs. Innovations in Systems and Software Engineering. 2013;9(2):95-104. https://doi.org/10.1007/s11334-013-0210-2

Author

Perrone, Gian David ; Debois, Søren ; Hildebrandt, Thomas. / A verification environment for bigraphs. I: Innovations in Systems and Software Engineering. 2013 ; Bind 9, Nr. 2. s. 95-104.

Bibtex

@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",
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",

}

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