ITU

A verification environment for bigraphs

Research output: Journal Article or Conference Article in JournalJournal articleResearchpeer-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: Journal Article or Conference Article in JournalJournal articleResearchpeer-review

Harvard

APA

Vancouver

Author

Bibtex

@article{583fca1afd8647fb9e53decd4c1bc0bc,
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.",
keywords = "Bigraphs, Reactive Systems, Reachability analysis, Domain-specific modelling languages",
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 U K",
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.

KW - Bigraphs

KW - Reactive Systems

KW - Reachability analysis

KW - Domain-specific modelling languages

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: 38554540