Logotype Mälardalenn University

MRTC publications



Algorithmic Computation of Strongest Postconditions of Services as Priced Timed Automata

Full text:  
Authors: Aida Causevic, Cristina Seceleanu, Paul Pettersson
Source: MRTC report ISSN 1404-3041 ISRN MDH-MRTC-263/2012-1-SE, Mälardalen Real-Time Research Centre, Mälardalen University
 

Abstract

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).
 

BibTeX entry

@techreport{Causevic_2786:2012,
   author = {Aida Causevic and Cristina Seceleanu and Paul Pettersson},
   title = {Algorithmic Computation of Strongest Postconditions of Services as Priced Timed Automata},
   month = {April},
   year = {2012},
   institution = {M{\aa}lardalen University},
   number = {ISSN 1404-3041 ISRN MDH-MRTC-263/2012-1-SE},
   type = {{T}echnical {R}eport},
   url = {http://www.mrtc.mdh.se/index.php?choice=publications&id=2786},
}

  • Mälardalen University |
  • Box 883 |
  • 721 23 Västerås/Eskilstuna |
  • 021-101300, 016-153600 |
  • webmaster |
  • Latest update: 2012.08.24