Return to search

Connecting a Design Framework for Service-oriented Systems with UPPAAL model-checker

In the context of Service-Oriented Systems (SOS), services represent loosely coupled discrete units that can be created, invoked, composed and decomposed upon a client request. In such a setting, where complex systems are composed out of services based on the client request, ensuring the expected level of Quality-of-Service (QoS) becomes a difficult task. In systems built on service-oriented principles, the formal specification of both functional and extra-functional system behavior, service availability, compatibility and interoperability between different services and systems have become important issues. To be compliant with the new features, the REMES language has been extended towards SOS with new constructs that have been given formal semantics. In this thesis, we propose transformation rules, definitions and techniques for transforming these new constructs into Timed Automata (TA) counterparts to facilitate the formal analysis. Also, we present an extension to an existing REMES SOS IDE toolset for performing an automated transformation of the REMES SOS models into the TA framework suitable for the formal analysis with the UPPAAL model-checker. The contribution from our work is on two fronts: a) define transformation rules for all of the constructs specific for the REMES SOS modeling and b) prototype implementation of the transformation rules as an extension add-on to the already existing IDE for modeling SOS to perform the automated transformation. The benefit of performing an automated transformation of the REMES SOS models in TA is twofold. First, by automating the transformation process, the process of validation of the models becomes faster. Second, we considerably reduce the influence from the human factor in the entire process, and at the same time lower the risks of introducing errors into the systems in the phase of creating the formal model. Additional benefit from the automated process is that the SOS designer does not have to be a verification expert in order to be able to verify the modeled system.

Identiferoai:union.ndltd.org:UPSALLA1/oai:DiVA.org:mdh-23137
Date January 2013
CreatorsFilipovikj, Predrag
PublisherMälardalens högskola, Akademin för innovation, design och teknik
Source SetsDiVA Archive at Upsalla University
LanguageEnglish
Detected LanguageEnglish
TypeStudent thesis, info:eu-repo/semantics/bachelorThesis, text
Formatapplication/pdf
Rightsinfo:eu-repo/semantics/openAccess

Page generated in 0.0025 seconds