Projects per year
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 | |
Publication status | Published - 2013 |
Keywords
- Bigraphs
- Reactive systems
- Reachability analysis
- Domain-specific modelling languages
Fingerprint
Dive into the research topics of 'A verification environment for bigraphs'. Together they form a unique fingerprint.Projects
- 1 Finished
-
Jingling Genie: Context-Sensitive Services Developed in Global Collaboration
Staunstrup, J. (PI), Hildebrandt, T. (CoI), Stald, G. B. (CoI) & Hansen, J. P. (CoI)
Danish Council for Strategic Research
01/01/2009 → 31/12/2013
Project: Research