Ä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 for Behavioral Modeling and Analysis of Design-time Services and Service Negotiations
Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system. (IS (Formal Modelling and Analysis of Embedded Systems))ORCID-id: 0000-0001-5293-3804
2014 (Engelska)Doktorsavhandling, sammanläggning (Övrigt vetenskapligt)
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.

Ort, förlag, år, upplaga, sidor
Västerås: Mälardalen University , 2014. , 236 s.
Serie
Mälardalen University Press Dissertations, ISSN 1651-4238 ; 147
Nyckelord [en]
Service-Oriented Systems, Formal modeling and Analysis, Service, Service Composition, Service Negotiation
Nationell ämneskategori
Datavetenskap (datalogi)
Forskningsämne
datavetenskap
Identifikatorer
URN: urn:nbn:se:mdh:diva-23271ISBN: 978-91-7485-128-1 (tryckt)OAI: oai:DiVA.org:mdh-23271DiVA: diva2:677410
Disputation
2014-01-15, Pi, Högskoleplan 1, Västerås, 09:00 (Engelska)
Opponent
Handledare
Projekt
Contesse
Forskningsfinansiär
Vetenskapsrådet
Tillgänglig från: 2013-12-10 Skapad: 2013-12-09 Senast uppdaterad: 2015-02-05Bibliografiskt granskad
Delarbeten
1. 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
2. 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
3. Checking Correctness of Services Modeled as Priced Timed Automata
Öppna denna publikation i ny flik eller fönster >>Checking Correctness of Services Modeled as Priced Timed Automata
2012 (Engelska)Ingår i: Lecture Notes in Computer Science, vol. 7610, issue part 2, Springer, 2012, 308-322 s.Kapitel i bok, del av antologi (Refereegranskat)
Abstract [en]

Service-Oriented Systems (SOS) have gained importance in different application domains thanks to their ability to enable reusable functionality provided via well-defined interfaces, and the increased opportunities to compose existing units, called services, into various configurations. Developing applications in such a setup, by reusing existing services, brings some concerns regarding the assurance of the expected Quality-of-Service (QoS), and correctness of the employed services. In this paper, we describe a formal mechanism of computing service guarantees, automatically. We assume service models annotated with pre- and postconditions, with their semantics given as Priced Timed Automata (PTA), and the forward analysis method for checking the service correctness w.r.t. given requirements. Under these assumptions, we show how to compute the strongest postcondition of the corresponding automata algorithmically, with respect to the specified precondition. The approach is illustrated on a small example of a service modeled as Priced Timed Automaton (PTAn).

Ort, förlag, år, upplaga, sidor
Springer, 2012
Serie
Lecture Notes in Computer Science, ISSN 0302-9743 ; 7610
Nationell ämneskategori
Teknik och teknologier
Identifikatorer
urn:nbn:se:mdh:diva-17344 (URN)10.1007/978-3-642-34032-1_29 (DOI)2-s2.0-84868288030 (Scopus ID)978-364234031-4 (ISBN)
Anmärkning

5th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation: Technologies for Mastering Change, ISoLA 2012; Heraklion, Crete; 15 October 2012 through 18

Tillgänglig från: 2012-12-20 Skapad: 2012-12-20 Senast uppdaterad: 2016-05-17Bibliografiskt granskad
4. An Analyzable Model of Automated Service Negotiation
Öppna denna publikation i ny flik eller fönster >>An Analyzable Model of Automated Service Negotiation
2013 (Engelska)Ingår i: Proceedings - 2013 IEEE 7th International Symposium on Service-Oriented System Engineering, SOSE 2013, 2013, 125-136 s.Konferensbidrag, Publicerat paper (Refereegranskat)
Abstract [en]

Negotiation is a key aspect of Service-Oriented Systems, which is rarely supported by formal models and tools for analysis. Often, service negotiation proceeds with timing, cost and resource constraints, under which the users and providers exchange information on their respective goals, until reaching a consensus. Consequently, a mathematically driven technique to analyze various ways to achieve such goals is beneficial. In this paper, we propose an analyzable negotiation model between service clients and providers, in our recently introduced language REMES and its corresponding textual service composition language HDCL. The model can be viewed as a negotiation interface for different negotiation strategies and protocols, which iterates until an agreement is reached. We show how to analyze the negotiation model against timing, cost and utility constraints, by transforming it into the Timed Automata formal framework. We illustrate our approach through an insurance scenario assuming a form of the Contract Net Protocol for web services.

Nationell ämneskategori
Teknik och teknologier
Identifikatorer
urn:nbn:se:mdh:diva-21323 (URN)10.1109/SOSE.2013.51 (DOI)000325717400012 ()2-s2.0-84880890696 (Scopus ID)9780769549446 (ISBN)
Konferens
2013 IEEE 7th International Symposium on Service-Oriented System Engineering, SOSE 2013; Redwood City, San Francisco Bay, CA; United States; 25 March 2013 through 28 March 2013
Projekt
CONTESSE - Contract-Based Components for Embedded Software
Tillgänglig från: 2013-09-20 Skapad: 2013-09-11 Senast uppdaterad: 2015-11-04Bibliografiskt granskad
5. Distributed Energy Management Case Study: A Formal Approach to Analyzing Utility Functions
Öppna denna publikation i ny flik eller fönster >>Distributed Energy Management Case Study: A Formal Approach to Analyzing Utility Functions
2013 (Engelska)Rapport (Övrigt vetenskapligt)
Abstract [en]

The service-oriented paradigm has been established to enable quicker development of new applications from already existing services. Service negotiation is a key technique to provide a way of deciding and choosing the most suitable service, out of possibly many services delivering similar functionality but having different response times, resource usages, prices, etc. In this paper, we present a formal approach to the clients-providers negotiation of distributed energy management. The models are described in our recently introduced REMES HDCL language, with timed automata semantics that allows us to apply UPPAAL-based tools for model-checking various scenarios of service negotiation. Our target is to compute ways of reaching the price- and reliability-optimal values of the utility function, at the end of the service negotiation.

Ort, förlag, år, upplaga, sidor
Sweden: , 2013
Serie
MRTC Reports
Nationell ämneskategori
Teknik och teknologier
Identifikatorer
urn:nbn:se:mdh:diva-22304 (URN)
Projekt
CONTESSE - Contract-Based Components for Embedded Software
Tillgänglig från: 2013-10-31 Skapad: 2013-10-31 Senast uppdaterad: 2015-02-05Bibliografiskt granskad
6. A Design Tool for Service-oriented Systems
Öppna denna publikation i ny flik eller fönster >>A Design Tool for Service-oriented Systems
2013 (Engelska)Ingår i: Electronical Notes in Theoretical Computer Science, ISSN 1571-0661, E-ISSN 1571-0661, Vol. 295, 95-100 s.Artikel i tidskrift (Övrigt vetenskapligt) Published
Abstract [en]

In this paper we present a modeling and analysis tool for service-oriented systems. The tool enables graphical modeling of service-based systems, within the resource-aware timed behavioral language Remes, as well as a textual system description. We have developed a graphical environment where services can be composed as desired by the user, together with a textual service composition interface in which compositions can also be checked for correctness. We also provide automated traceability between the two design interfaces, which results in a tool that enhances the potential of system design by intuitive service manipulation. The paper presents the design principles, infrastructure, and the user interface of our tool.

Nationell ämneskategori
Datavetenskap (datalogi)
Forskningsämne
datavetenskap
Identifikatorer
urn:nbn:se:mdh:diva-14128 (URN)10.1016/j.entcs.2013.04.008 (DOI)2-s2.0-84877250201 (Scopus ID)
Konferens
Proceedings the 9th International Workshop on Formal Engineering approaches to Software Components and Architectures (FESCA)
Projekt
ContesseMBATATAC
Tillgänglig från: 2012-02-01 Skapad: 2012-02-01 Senast uppdaterad: 2015-11-04Bibliografiskt granskad

Open Access i DiVA

fulltext(1801 kB)477 nedladdningar
Filinformation
Filnamn FULLTEXT03.pdfFilstorlek 1801 kBChecksumma SHA-512
bf7df8bcea4aa7ef728306a15f1249fc3aa4cd69ac4339d7a283b7218dbc63870eb809e43292fa29481cb3b58c3e56b2f21134b1b6351b176ff21607b8c24f6f
Typ fulltextMimetyp application/pdf

Sök vidare i DiVA

Av författaren/redaktören
Čaušević, Aida
Av organisationen
Inbyggda system
Datavetenskap (datalogi)

Sök vidare utanför DiVA

GoogleGoogle Scholar
Totalt: 477 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: 786 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