<?xml version="1.0" encoding="UTF-8"?><xml><records><record><source-app name="Biblio" version="6.x">Drupal-Biblio</source-app><ref-type>47</ref-type><contributors><authors><author><style face="normal" font="default" size="100%">Alejandro Sanchez</style></author><author><style face="normal" font="default" size="100%">Luis Soares Barbosa</style></author><author><style face="normal" font="default" size="100%">Daniel Riesco</style></author></authors><secondary-authors><author><style face="normal" font="default" size="100%">Hei Wang</style></author><author><style face="normal" font="default" size="100%">Richard Banach</style></author></secondary-authors></contributors><titles><title><style face="normal" font="default" size="100%">Verifying bigraphical models of architectural reconfigurations</style></title><secondary-title><style face="normal" font="default" size="100%">7th IEEE Symposium on Theoretical Aspects of Software Engineering - TASE</style></secondary-title></titles><dates><year><style  face="normal" font="default" size="100%">2013</style></year><pub-dates><date><style  face="normal" font="default" size="100%">July</style></date></pub-dates></dates><urls><related-urls><url><style face="normal" font="default" size="100%">https://haslab.uminho.pt/sites/default/files/lsb/files/sbr13-tase.pdf</style></url></related-urls></urls><publisher><style face="normal" font="default" size="100%">IEEE Computer Society</style></publisher><pub-location><style face="normal" font="default" size="100%">Birmingham, UK</style></pub-location><pages><style face="normal" font="default" size="100%">135-138</style></pages><language><style face="normal" font="default" size="100%">eng</style></language><abstract><style face="normal" font="default" size="100%">&lt;p&gt;ARCHERY is an architectural description language for modelling and reasoning about distributed, heterogeneous and dynamically reconfigurable systems. This paper proposes a structural semantics for ARCHERY, and a method for deriving labelled transition systems (LTS) in which states and transitions represent configurations and reconfiguration operations, respectively. Architectures are modelled by bigraphs and their dynamics by parametric reaction rules. The resulting LTSs can be regarded as Kripke frames, appropriate for verifying reconfiguration constraints over architectural patterns expressed in a modal logic. The derivation method proposed here applies Leifer's approach twice, and combines the results of each application to obtain a label representing a reconfiguration operation and its actual parameters. Labels obtained in this way are minimal and yield LTSs in which bisimulation is a congruence.&lt;/p&gt;
</style></abstract></record></records></xml>