https://www.mdu.se/

mdu.sePublications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Towards a Unified Behavioral Model for Component-Based and Service-Oriented Systems
Mälardalen University, School of Innovation, Design and Engineering. (Real-Time Systems Modelling and Analysis)ORCID iD: 0000-0001-5293-3804
Mälardalen University, School of Innovation, Design and Engineering. (Industrial Software Engineering)ORCID iD: 0000-0003-2383-7981
2009 (English)In: Computer Software and Applications Conference, 2009. COMPSAC '09. 33rd Annual IEEE International, 2009, p. 497-503Conference paper, Published paper (Refereed)
Abstract [en]

There is no clear distinction between service-orientedsystems (SOS) and component-based systems (CBS). However,there are several characteristics that could let one considerSOS as a step further from CBS. In this paper, we discussthe general features of CBS and SOS, while accountingfor behavioral modeling in the language called REMES.First, we present REMES in the context of CBS modeling,and then we show how it can become suitable for SOS. Wealso discuss the relation between our model and the currentstate of the art.

Place, publisher, year, edition, pages
2009. p. 497-503
Keywords [en]
service-oriented systems, component-based systems, behavioral modeling, analysis, timed automata
National Category
Engineering and Technology
Identifiers
URN: urn:nbn:se:mdh:diva-6563DOI: 10.1109/COMPSAC.2009.182ISI: 000274261400187Scopus ID: 2-s2.0-70449658389ISBN: 978-0-7695-3726-9 (print)OAI: oai:DiVA.org:mdh-6563DiVA, id: diva2:227057
Conference
IEEE 33rd International Computer Software and Applications Conference, Seattle, WA, JUL 20-24, 2009
Projects
PROGRESSQ-ImPrESSAvailable from: 2009-07-09 Created: 2009-07-09 Last updated: 2018-08-21Bibliographically approved
In thesis
1. Formal Approaches to Service-oriented Design: From Behavioral Modeling to Service Analysis
Open this publication in new window or tab >>Formal Approaches to Service-oriented Design: From Behavioral Modeling to Service Analysis
2011 (English)Licentiate thesis, comprehensive summary (Other academic)
Abstract [en]

Service-oriented systems (SOS) have recently emerged as context-independent component-based systems. In contrast to components, services can be created, invoked, composed and destroyed at run-time. Services are assumed to be platform independent and available for use within heterogeneous applications. One of the main assets in SOS is service composability. It allows the development of composite services with the main goal of reusable functionality provided by existing services in a low cost and rapid development process at run-time. However, in such distributed systems it becomes difficult to guarantee the quality of services (QoS), both in isolation, as well as of the newly created service compositions. Means of checking correctness of service composition can enable optimization w.r.t. the function and resource-usage of composed services, as well as provide a higher degree of QoS assurance of a service composition. To accomplish such goals, we employ model-checking technique for both single and composed services. The verification eventually provides necessaryinformation about QoS, already at early development stage.This thesis presents the research that we have been carrying out, on developing of methods and tools for specification, modeling, and formal analysis of services and service compositions in SOS. In this work, we first show how to formally check QoS in terms of performance and reliability for formallyspecified component-based systems (CBS). Next, we outline the commonalities and differences between SOS and CBS. Third, we develop constructs for the formal description of services using the resource-aware timed behavioral language called REMES, including development of language to support service compositions. At last, we show how to check service and service composition(functional, timing and resource-wise) correctness by employing the strongest post condition semantics. For less complex services and service compositions we choose to prove correctness using Hoare triples and the guarded command language. In case of complex services described as priced timed automata(PTA), we prove correctness via algorithmic computation of strongest post-condition of PTA.

Place, publisher, year, edition, pages
Västerås: Mälardalen University, 2011
Series
Mälardalen University Press Licentiate Theses, ISSN 1651-9256 ; 134
Keywords
service-oriented software engineering, formal modeling, service-oriented systems, resources, analysis, behavior, correctness check
National Category
Computer Sciences
Research subject
Computer Science
Identifiers
urn:nbn:se:mdh:diva-12166 (URN)978-91-7485-012-3 (ISBN)
Presentation
2011-06-10, Gamma, Högskoleplan 1, Västerås, 10:00 (English)
Opponent
Supervisors
Projects
Q-ImPreSS
Funder
EU, FP7, Seventh Framework Programme
Available from: 2011-05-03 Created: 2011-04-27 Last updated: 2018-01-12Bibliographically approved
2. Formal Approaches for Behavioral Modeling and Analysis of Design-time Services and Service Negotiations
Open this publication in new window or tab >>Formal Approaches for Behavioral Modeling and Analysis of Design-time Services and Service Negotiations
2014 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

During the past decade service-orientation has become a popular design paradigm, offering an approach in which services are the functional building blocks. Services are self-contained units of composition, built to be invoked, composed, and destroyed on (user) demand. Service-oriented systems (SOS) are a collection of services that are developed based on several design principles such as: (i) loose coupling between services (e.g., inter-service communication can involve either simple data passing or two or more connected services coordinating some activity) that allows services to be independent, yet highly interoperable when required; (ii) service abstraction, which emphasizes the need to hide as many implementation details as possible, yet still exposing functional and extra-functional capabilities that can be offered to service users; (iii) service reusability provided by the existing services in a rapid and flexible development process; (iv) service composability as one of the main assets of SOS that provide a design platform for services to be composed and decomposed, etc. One of the main concerns in such systems is ensuring service quality per se, but also guaranteeing the quality of newly composed services. To accomplish the above, we consider two system perspectives: the developer's and the user's view, respectively. In the former, one can be assumed to have access to the internal service representation: functionality, enabled actions, resource usage, and interactions with other services. In the second, one has information primarily on the service interface and exposed capabilities (attributes/features). Means of checking that services and service compositions meet the expected requirements, the so-called correctness issue, can enable optimization and possibility to guarantee a satisfactory level of a service composition quality. In order to accomplish exhaustive correctness checks of design-time SOS, we employ model-checking as the main formal verification technique, which eventually provides necessary information about quality-of-service (QoS), already at early stages of system development. ~As opposed to the traditional approach of software system construction, in SOS the same service may be offered at various prices, QoS, and other conditions, depending on the user needs. In such a setting, the interaction between involved parties requires the negotiation of what is possible at request time, aiming at meeting needs on demand. The service negotiation process often proceeds with timing, price, and resource constraints, under which users and providers exchange information on their respective goals, until reaching a consensus. Hence, a mathematically driven technique to analyze a priori various ways to achieve such goals is beneficial for understanding what and how can particular goals be achieved.

This thesis presents the research that we have been carrying out over the past few years, which resulted in developing methods and tools for the specification, modeling, and formal analysis of services and service compositions in SOS. The contributions of the thesis consist of: (i)constructs for the formal description of services and service compositions using the resource-aware timed behavioral language called REMES; (ii) deductive and algorithmic approaches for checking correctness of services and service compositions;(iii) a model of service negotiation that includes different negotiation strategies, formally analyzed against timing and resource constraints; (iv) a tool-chain (REMES SOS IDE) that provides an editor and verification support (by integration with the UPPAAL model-checker) to REMES-based service-oriented designs;(v) a relevant case-study by which we exercise the applicability of our framework.The presented work has also been applied on other smaller examples presented in the published papers.

Abstract [sv]

Under det senaste årtiondet har ett tjänstorienterat paradigm blivit allt-mer populärt i utvecklingen av datorsystem. I detta paradigm utgör så kallade tjänster den minsta funktionella systemenheten. Dessa tjänster är konstruerade så att de kan skapas, användas, sammansättas och avslutas separat. De ska vara oberoende av varandra samtidigt som de ska kunna fungera effektivt tillsammans och i samarbete med andra system när så behövs. Vidare ska tjänsterna dölja sina interna implementa-tionsdetaljer i så stor grad som möjligt, samtidigt som deras fulla funktionalitet ska exponeras för systemdesignern. Tjänsterna ska också på ett enkelt sätt kunna återanvändas och sammansättas i en snabb och flexibel utvecklingsprocess.En av de viktigaste aspekterna i tjänsteorienterade datorsystem är att kunna säkerställa systemens kvalitet. För att åstadkomma detta ärdet viktigt att få en djupare insikt om tjänstens interna funktionalitet, i termer av möjliga operationer, resursinformation, samt tänkbar inter-aktion med andra tjänster. Detta är speciellt viktigt när utvecklaren har möjlighet att välja mellan två funktionellt likvärda tjänster somär olika med avseende på andra egenskaper, såsom responstid eller andra resurskrav. I detta sammanhang kan en matematisk beskrivning av en tjänsts beteende ge ökad förståelse av tjänstemodellen, samt hjälpa användaren att koppla ihop tjänster på ett korrekt sätt. En matematisk beskrivning öppnar också upp för ett sätt att matematiskt resonera kring tjänster. Metoder för att kontrollera att komponerade tjänstermöter ställda resurskrav möjliggör också resursoptimering av tjänster samt verifiering av ställda kvalitetskrav.I denna avhandling presenteras forskning som har bedrivits under de senaste åren. Forskningen har resulterat i metoder och verktyg föratt specificera, modellera och formellt analysera tjänster och sammansättning av tjänster. Arbetet i avhandlingen består av (i) en formell definition av tjänster och sammansättning av tjänster med hjälp avett resursmedvetet formellt specifikationsspråk kallat Remes; (ii) två metoder för att analysera tjänster och kontrollera korrektheten i sammansättning av tjänster, både deduktivt och algoritmiskt; (iii) en modell av förhandlingsprocessen vid sammansättning av tjänster som inkluderar olika förhandlingsstrategier; (iv) ett antal verktyg som stödjer dessa metoder. Metoderna har använts i ett antal fallstudier som är presenterade i de publicerade artiklarna.

Place, publisher, year, edition, pages
Västerås: Mälardalen University, 2014. p. 236
Series
Mälardalen University Press Dissertations, ISSN 1651-4238 ; 147
Keywords
Service-Oriented Systems, Formal modeling and Analysis, Service, Service Composition, Service Negotiation
National Category
Computer Sciences
Research subject
Computer Science
Identifiers
urn:nbn:se:mdh:diva-23271 (URN)978-91-7485-128-1 (ISBN)
Public defence
2014-01-15, Pi, Högskoleplan 1, Västerås, 09:00 (English)
Opponent
Supervisors
Projects
Contesse
Funder
Swedish Research Council
Available from: 2013-12-10 Created: 2013-12-09 Last updated: 2018-01-11Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Authority records

Causevic, AidaVulgarakis, Aneta

Search in DiVA

By author/editor
Causevic, AidaVulgarakis, Aneta
By organisation
School of Innovation, Design and Engineering
Engineering and Technology

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 110 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf