Software architectures can help in the specification, formal analysis and manipulation of complex and adaptive systems. Many languages and formalisms have been proposed for these tasks, especially those based on graph model. Bigraphical Reactive Systems (BRS) are an emerging graphical framework for specifying ubiquitous dynamic architectural systems.
In this work, we propose using the K semantic framework, a provably sound and complete modeling methodology, to integrate BRS into rewriting logic. Thanks to this approach, we obtain a high level specification of bigraphical systems without any encoding or translation process. Moreover, we are also able to formally reason on it.
Finally, we illustrate the use of the K-Maude tool through a simple example of a packet transport.
5th Mosharaka International Conference on Communications, Computers and Applications (MIC-CCA 2012)
Congress
2012 Global Congress on Communications, Computers and Applications (GC-CCA 2012), 12-14 October 2012, Istanbul, Turkey
Pages
--1
Topics
Behavioral Modeling Software Development
ISSN
2227-331X
DOI
BibTeX
@inproceedings{460CCA2012,
title={Defining and executing bigraphical model in Maude},
author={Manel Djenouhat, and Taha Abdelmoutaleb Cherfia, and Faiza Belala},
booktitle={2012 Global Congress on Communications, Computers and Applications (GC-CCA 2012)},
year={2012},
pages={--1},
doi={}},
organization={Mosharaka for Research and Studies}
}
