Projekter pr. år
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.
Bidragets oversatte titel | Et verifikationsmiljø for bigrafer |
---|---|
Originalsprog | Engelsk |
Tidsskrift | Innovations in Systems and Software Engineering |
Vol/bind | 9 |
Udgave nummer | 2 |
Sider (fra-til) | 95-104 |
ISSN | 1614-5046 |
DOI | |
Status | Udgivet - 2013 |
Emneord
- Bigraphs
- Reactive Systems
- Reachability analysis
- Domain-specific modelling languages
Fingeraftryk
Dyk ned i forskningsemnerne om 'Et verifikationsmiljø for bigrafer'. Sammen danner de et unikt fingeraftryk.Projekter
- 1 Afsluttet
-
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
Projekter: Projekt › Forskning