mdh.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
Algorithmic Computation of Strongest Postconditions of Services as Priced Timed Automata
Mälardalen University, School of Innovation, Design and Engineering. (IS)ORCID iD: 0000-0001-5293-3804
Mälardalen University, School of Innovation, Design and Engineering. (IS)ORCID iD: 0000-0003-2870-2680
Mälardalen University, School of Innovation, Design and Engineering. (IS)ORCID iD: 0000-0003-4040-3480
2012 (English)Report (Other academic)
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 provide a formal mechanism of computing service guarantees, automatically. We assume service models annotated with pre- and postconditions, 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).

Place, publisher, year, edition, pages
Västerås: Mälardalen Real-Time Research Centre, Mälardalen University , 2012.
Series
MRTC Report, ISSN 1404-3041
National Category
Engineering and Technology
Identifiers
URN: urn:nbn:se:mdh:diva-17259ISRN: MDH-MRTC-263/2012-1-SEOAI: oai:DiVA.org:mdh-17259DiVA, id: diva2:579590
Available from: 2012-12-20 Created: 2012-12-20 Last updated: 2013-12-03Bibliographically approved

Open Access in DiVA

No full text in DiVA

Authority records BETA

Causevic, AidaSeceleanu, CristinaPettersson, Paul

Search in DiVA

By author/editor
Causevic, AidaSeceleanu, CristinaPettersson, Paul
By organisation
School of Innovation, Design and Engineering
Engineering and Technology

Search outside of DiVA

GoogleGoogle Scholar

urn-nbn

Altmetric score

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