Due to the increasing need of highly dependable services in Service-Oriented Architectures
(SOA), service-level agreements include more and more frequently such non-functional
aspects as security, safety, availability, reliability, etc. Whenever a service can
no longer be provided with the required QoS, the service requester needs to switch
dynamically to a new service having adequate service parameters after exchanging a
sequence of messages. In the current paper, we first extend the core SOA metamodel
with parameters required for reliable messaging in services. Then we model reconfigurations
for reliable message delivery by graph transformation rules. Finally, we carry out
a formal verification of the proposed rule set by combining analysis tools for graph
transformation and labeled transition systems.
