Ändra sökning
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Formal Approaches to Service-oriented Design: From Behavioral Modeling to Service Analysis
Mälardalens högskola, Akademin för innovation, design och teknik. (Formal Modelling and Analysis of Embedded Systems)ORCID-id: 0000-0001-5293-3804
2011 (Engelska)Licentiatavhandling, sammanläggning (Övrigt vetenskapligt)
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.

Ort, förlag, år, upplaga, sidor
Västerås: Mälardalen University , 2011.
Serie
Mälardalen University Press Licentiate Theses, ISSN 1651-9256 ; 134
Nyckelord [en]
service-oriented software engineering, formal modeling, service-oriented systems, resources, analysis, behavior, correctness check
Nationell ämneskategori
Datavetenskap (datalogi)
Forskningsämne
datavetenskap
Identifikatorer
URN: urn:nbn:se:mdh:diva-12166ISBN: 978-91-7485-012-3 (tryckt)OAI: oai:DiVA.org:mdh-12166DiVA: diva2:413030
Presentation
2011-06-10, Gamma, Högskoleplan 1, Västerås, 10:00 (Engelska)
Opponent
Handledare
Projekt
Q-ImPreSS
Forskningsfinansiär
EU, FP7, Sjunde ramprogrammet
Tillgänglig från: 2011-05-03 Skapad: 2011-04-27 Senast uppdaterad: 2014-01-09Bibliografiskt granskad
Delarbeten
1. Analyzing Resource-Usage Impact on Component-Based Systems Performance and Reliability
Öppna denna publikation i ny flik eller fönster >>Analyzing Resource-Usage Impact on Component-Based Systems Performance and Reliability
2008 (Engelska)Ingår i: 2008 International Conference on Computational Intelligence for Modelling Control & Automation, Los Alamitos, CA: IEEE Computer Society , 2008, 302-308 s.Konferensbidrag, Publicerat paper (Refereegranskat)
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.

Ort, förlag, år, upplaga, sidor
Los Alamitos, CA: IEEE Computer Society, 2008
Nyckelord
resource-usage, performance, reliability, prediction, comonent-based systems
Nationell ämneskategori
Datavetenskap (datalogi)
Forskningsämne
datavetenskap
Identifikatorer
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)
Konferens
International Conference on Computational Intelligence for Modelling, Control and Automation Vienna, AUSTRIA, DEC 10-12, 2008
Projekt
Q-ImPrEESPROGRESS
Tillgänglig från: 2009-05-13 Skapad: 2009-04-16 Senast uppdaterad: 2013-12-03Bibliografiskt granskad
2. Towards a Unified Behavioral Model for Component-Based and Service-Oriented Systems
Öppna denna publikation i ny flik eller fönster >>Towards a Unified Behavioral Model for Component-Based and Service-Oriented Systems
2009 (Engelska)Ingår i: Computer Software and Applications Conference, 2009. COMPSAC '09. 33rd Annual IEEE International, 2009, 497-503 s.Konferensbidrag, Publicerat paper (Refereegranskat)
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.

Nyckelord
service-oriented systems, component-based systems, behavioral modeling, analysis, timed automata
Nationell ämneskategori
Teknik och teknologier
Identifikatorer
urn:nbn:se:mdh:diva-6563 (URN)10.1109/COMPSAC.2009.182 (DOI)2-s2.0-70449658389 (Scopus ID)978-0-7695-3726-9 (ISBN)
Konferens
IEEE 33rd International Computer Software and Applications Conference, Seattle, WA, JUL 20-24, 2009
Projekt
PROGRESSQ-ImPrESS
Tillgänglig från: 2009-07-09 Skapad: 2009-07-09 Senast uppdaterad: 2014-05-16Bibliografiskt granskad
3. Modeling and Reasoning about Service Behaviors and their Compositions
Öppna denna publikation i ny flik eller fönster >>Modeling and Reasoning about Service Behaviors and their Compositions
2010 (Engelska)Ingår i: Lecture Notes in Computer Science, vol. 6416, Berlin: Springer , 2010, 82-96 s.Kapitel i bok, del av antologi (Refereegranskat)
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.

Ort, förlag, år, upplaga, sidor
Berlin: Springer, 2010
Serie
Lecture Notes in Computer Science, ISSN 0302-9743 ; 6416
Nationell ämneskategori
Teknik och teknologier
Identifikatorer
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)
Anmärkning

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

Tillgänglig från: 2010-11-10 Skapad: 2010-11-10 Senast uppdaterad: 2014-06-22Bibliografiskt granskad

Open Access i DiVA

fulltext(649 kB)1152 nedladdningar
Filinformation
Filnamn FULLTEXT02.pdfFilstorlek 649 kBChecksumma SHA-512
315b9c44be6c639b7f67d9a0bf86b127495e5f9c7dfbc412fbb82e732a9fba79ff36dec2ef2d7e46d490a181c48378f829485ce0a71301235ec0ec479922aaf6
Typ fulltextMimetyp application/pdf

Sök vidare i DiVA

Av författaren/redaktören
Čaušević, Aida
Av organisationen
Akademin för innovation, design och teknik
Datavetenskap (datalogi)

Sök vidare utanför DiVA

GoogleGoogle Scholar
Totalt: 1152 nedladdningar
Antalet nedladdningar är summan av nedladdningar för alla fulltexter. Det kan inkludera t.ex tidigare versioner som nu inte längre är tillgängliga.

Totalt: 302 träffar
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf