Bachelor and Master Theses

Title: Connecting a Design Framework for Service-oriented Systems with UPPAAL model-checker
Subject: Computer Science
Level: Advanced
Description: Service-oriented systems (SOS) use services as their fundamental functional units, with capabilities of being published, invoked, composed and destroyed at run-time. Services are loosely coupled and have a greater level of independence from implementation attributes than components.

To address functional but also extra-functional behaviour such as timing and resource usage of services in SOS we use dense time hierarchical modelling language called REMES. The language has been initially intended to provide modelling and analysis of embedded systems in a component-based fashion [1]. We have extended REMES with constructs fit for SOS description [3]. For the analysis purposes REMES models can be semantically transformed to Timed Automata (TA) and Priced Timed Automata(PTA) formal framework and analysed in UPPAAL1 model checker [2].The service interface has been defined, such that a service could be published and visible to service users. Our service interface is modelled to include information about the service type, time-to-serve, service capacity, service status, service pre-, and postcondition. The latter specify the set of initial conditions to be fulfilled by the service in order to be executed, as the precondition, and the guaranteed result of operation, that includes information about extra-functional properties such as timing and resource-usage, as the service postcondition. REMES SOS provides support for modelling of atomic and composite services. Additionally, services can be employed in various types of service compositions achieved via serial, parallel, or parallel with synchronization type of binding. To provide service manipulation we have enriched REMES with interface operations such as: create service, delete service, replace service, etc. Alongside these operations, we have defined a hierarchical language that supports REMES service composition (HDCL) and facilitates modelling of nested sequential, parallel or synchronized services.
To enable the correctness check of REMES services we use forward analysis technique that assumes computation of the strongest postcondition of a REMES service with respect to a given precondition. To prove the correctness of a REMES service in isolation, we check the Boolean implication between the calculated strongest postcondition and the given requirement. We have proposed two techniques for strongest postcondition calculation for services: a deductive one, starting from the guarded command language description of REMES services [3], and algorithmic one starting from the PTA description of a service [4]. The latter includes also the minimum/maximum resource-usage trace computation, while performing stronges t postcondition analysis.
The language is accompanied with a design framework that provides a graphical user interface for behaviour modelling of services based on REMES language, called REMES Service IDE2 [5]. In the current version NetBeans Visual Library API is used to display editable service diagrams with support for graph-oriented models. A textual dynamic service composition language was implemented, together with means to automatically verify the service composition correctness. An automated traceability between the service specification interfaces is ensured.
The goal of this master thesis is to extend already existing service-oriented design framework by providing an automated way to transform REMES models into TA and PTA, suitable for analysis in UPPAAL model-checker.

Expected outcome:

a) The tool extension implemented in Java.
b) Integration of the GUI with a UPPAAL-based model checker.
c) The thesis report describing the work.


References:
[1] REMES: A Resource Model for Embedded Systems, Cristina Seceleanu, Aneta Vulgarakis, Paul Pettersson, In Proc. of the 14th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS 2009), IEEE Computer Society, June, 2009

[2] Formal Semantics of the ProCom Real-Time Component Model, Aneta Vulgarakis, Jagadish Suryadevara, Jan Carlson, Cristina Seceleanu, Paul Pettersson, 35th Euromicro Conference on Software Engineering and Advanced Applications (SEAA), Patras, Greece, August, 2009

[3] Modeling and Reasoning about Service Behaviors and their Compositions, Aida Causevic, Cristina Seceleanu, Paul Pettersson, Proceedings of 4th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISOLA 2010), Formal Methods in Model-Driven Development for Service-Oriented and Cloud Computing track, Springer LNCS, Amirandes, Heraclion, Crete, October, 2010

[4] Checking Correctness of Services Modeled as Priced Timed Automata, Aida Causevic, Cristina Seceleanu, Paul Pettersson, Proceedings of 5th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, LNCS Proceedings (Springer Verlag), Amirandes, Heraclion, Crete, October, 2012

[5] A Design Tool for Service-oriented Systems, Eduard Paul Enoiu, Raluca Marinescu, Aida Causevic, Cristina Seceleanu, 9th International Workshop on Formal Engineering approaches to Software Components and Architectures (FESCA 2012), ENTCS, Estonia, March, 2012

Company: Mälardalens Högskola, kontaktperson: Aida Causevic
Prel. end date: 2013-06-30
Presentation date: 2013-06-13
Student: Predrag Filipovikj pfj12001@student.mdh.se
IDT supervisor: Aida Causevic
aida.delic@mdh.se, +46-21-107011
Examinator: Cristina Seceleanu
Cristina Seceleanu
cristina.seceleanu@mdh.se, +46-21-151764

Rapport och bilagor

Size

Senaste uppdatering

TR1469.pdf

1545068

2013-12-03, 14:08


  • Mälardalen University |
  • Box 883 |
  • 721 23 Västerås/Eskilstuna |
  • 021-101300, 016-153600 |
  • webmaster |
  • Latest update: 2017.08.23