Defining and executing bigraphical model in Maude

Software architectures can help in 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. This approach offers 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.