Change search
ReferencesLink to record
Permanent link

Direct link
Connecting a Design Framework for Service-oriented Systems with UPPAAL model-checker
Mälardalen University, School of Innovation, Design and Engineering. (Formal Modeling and Analysis Group)
2013 (English)Independent thesis Advanced level (degree of Master (Two Years)), 20 credits / 30 HE creditsStudent thesis
Abstract [en]

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. 

Place, publisher, year, edition, pages
2013. , 77 p.
Keyword [en]
SOS, UPPAAL, REMES, design framework, formal modeling
National Category
Computer Science
URN: urn:nbn:se:mdh:diva-23137OAI: diva2:673451
Subject / course
Computer Science
2013-06-14, Kappa, Högskoleplan 1, Västerås, 16:15 (English)
Available from: 2013-12-04 Created: 2013-12-03 Last updated: 2013-12-04Bibliographically approved

Open Access in DiVA

pfj12001(1509 kB)74 downloads
File information
File name FULLTEXT01.pdfFile size 1509 kBChecksum SHA-512
Type fulltextMimetype application/pdf

Search in DiVA

By author/editor
Filipovikj, Predrag
By organisation
School of Innovation, Design and Engineering
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 74 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Total: 111 hits
ReferencesLink to record
Permanent link

Direct link