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
Formal Approaches to Service-oriented Design: From Behavioral Modeling to Service Analysis
Mälardalen University, School of Innovation, Design and Engineering. (Formal Modelling and Analysis of Embedded Systems)ORCID iD: 0000-0001-5293-3804
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 [en]
service-oriented software engineering, formal modeling, service-oriented systems, resources, analysis, behavior, correctness check
National Category
Computer Sciences
Research subject
Computer Science
Identifiers
URN: urn:nbn:se:mdh:diva-12166ISBN: 978-91-7485-012-3 (print)OAI: oai:DiVA.org:mdh-12166DiVA, id: diva2:413030
Presentation
2011-06-10, Gamma, Högskoleplan 1, Västerås, 10:00 (English)
Opponent
Supervisors
Projects
Q-ImPreSS
Funder
EU, FP7, Seventh Framework ProgrammeAvailable from: 2011-05-03 Created: 2011-04-27 Last updated: 2018-01-12Bibliographically approved
List of papers
1. Analyzing Resource-Usage Impact on Component-Based Systems Performance and Reliability
Open this publication in new window or tab >>Analyzing Resource-Usage Impact on Component-Based Systems Performance and Reliability
2008 (English)In: 2008 International Conference on Computational Intelligence for Modelling Control & Automation, Los Alamitos, CA: IEEE Computer Society , 2008, p. 302-308Conference paper, Published paper (Refereed)
Abstract [en]

An early prediction of resource utilization and its impacton system performance and reliability can reduce theoverall system cost, by allowing early correction of detectedproblems, or changes in development plans with minimizedoverhead. Nowadays, researchers are using both academicand commercial models to predict such attributes, by measuringthem at earliest stages of system development. Inthis paper, we give a short overview of existing predictionmodels for performance and reliability, targeting popularcomponent-based frameworks. Next, we describe our ownapproach for tackling such predictions, through an illustrationon a small example that deals with estimations of energyconsumption.

Place, publisher, year, edition, pages
Los Alamitos, CA: IEEE Computer Society, 2008
Keywords
resource-usage, performance, reliability, prediction, comonent-based systems
National Category
Computer Sciences
Research subject
Computer Science
Identifiers
urn:nbn:se:mdh:diva-5722 (URN)10.1109/CIMCA.2008.190 (DOI)000277076500053 ()2-s2.0-70449570706 (Scopus ID)978-0-7695-3514-2 (ISBN)
Conference
International Conference on Computational Intelligence for Modelling, Control and Automation Vienna, AUSTRIA, DEC 10-12, 2008
Projects
Q-ImPrEESPROGRESS
Available from: 2009-05-13 Created: 2009-04-16 Last updated: 2018-01-13Bibliographically approved
2. Towards a Unified Behavioral Model for Component-Based and Service-Oriented Systems
Open this publication in new window or tab >>Towards a Unified Behavioral Model for Component-Based and Service-Oriented Systems
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.

Keywords
service-oriented systems, component-based systems, behavioral modeling, analysis, timed automata
National Category
Engineering and Technology
Identifiers
urn:nbn:se:mdh:diva-6563 (URN)10.1109/COMPSAC.2009.182 (DOI)000274261400187 ()2-s2.0-70449658389 (Scopus ID)978-0-7695-3726-9 (ISBN)
Conference
IEEE 33rd International Computer Software and Applications Conference, Seattle, WA, JUL 20-24, 2009
Projects
PROGRESSQ-ImPrESS
Available from: 2009-07-09 Created: 2009-07-09 Last updated: 2018-08-21Bibliographically approved
3. Modeling and Reasoning about Service Behaviors and their Compositions
Open this publication in new window or tab >>Modeling and Reasoning about Service Behaviors and their Compositions
2010 (English)In: Lecture Notes in Computer Science, vol. 6416, Berlin: Springer , 2010, p. 82-96Chapter in book (Refereed)
Abstract [en]

Service-oriented systems have recently emerged as context-independent component-based systems. Unlike components, services can be created, invoked, composed, and destroyed at run-time. Consequently, all services need a way of advertising their capabilities to the entities that will use them, and serviceoriented modeling should cater for various kinds of service composition. In this paper, we show how services can be formally described by the resource-aware timed behavioral language REMES, which we extend with service-specific information, such as type, capacity, time-to-serve, etc., as well as boolean constraints on inputs, and output guarantees. Assuming a Hoare-triple model of service correctness, we show how to check it by using the strongest postcondition semantics. To provide means for connecting REMES services, we propose a hierarchical language for service composition, which allows for verifying the latter's correctness. The approach is applied on an abstracted version of an intelligent shuttle system.

Place, publisher, year, edition, pages
Berlin: Springer, 2010
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 6416
National Category
Engineering and Technology
Identifiers
urn:nbn:se:mdh:diva-10859 (URN)10.1007/978-3-642-16561-0_14 (DOI)000289492800014 ()2-s2.0-78650272412 (Scopus ID)978-364216560-3 (ISBN)
Note

4th International Symposium on Leveraging Applications, ISoLA 2010; Heraklion, Crete; 18 October 2010 through 21 October 2010

Available from: 2010-11-10 Created: 2010-11-10 Last updated: 2014-06-22Bibliographically approved

Open Access in DiVA

fulltext(649 kB)1825 downloads
File information
File name FULLTEXT02.pdfFile size 649 kBChecksum SHA-512
315b9c44be6c639b7f67d9a0bf86b127495e5f9c7dfbc412fbb82e732a9fba79ff36dec2ef2d7e46d490a181c48378f829485ce0a71301235ec0ec479922aaf6
Type fulltextMimetype application/pdf

Authority records

Čaušević, Aida

Search in DiVA

By author/editor
Čaušević, Aida
By organisation
School of Innovation, Design and Engineering
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar
Total: 1826 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

isbn
urn-nbn

Altmetric score

isbn
urn-nbn
Total: 823 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