Reference : The tale of SOLOIST: a specification language for service compositions interactions
Scientific congresses, symposiums and conference proceedings : Paper published in a book
Engineering, computing & technology : Computer science
The tale of SOLOIST: a specification language for service compositions interactions
Bianculli, Domenico mailto [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > >]
Ghezzi, Carlo [Politecnico di Milano, Italy]
San Pietro, Pierluigi [Politecnico di Milano, Italy]
Formal Aspects of Component Software
[en] 9th International Symposium, FACS 2012, Mountain View, CA, USA, September 12-14, 2012. Revised Selected Papers
Păsăreanu, Corina
Salaün, Gwen
Lecture Notes in Computer Science; 7684
Formal Aspects of Component Software (FACS'12)
September 12-14, 2012
Mountain View, CA
[en] Service-based applications are a new class of software systems that provide the basis for enterprises to build their information systems by following the principles of service-oriented architectures. These software systems are often realized by orchestrating remote, third-party services, to provide added-values applications that are called service compositions. The distributed ownership and the evolving nature of the services involved in a service composition make verification activities crucial. On a par with verification is also the problem of formally specifying the interactions—with third-party services—of service compositions, with the related issue of balancing expressiveness and support for automated verification.
This paper showcases SOLOIST, a specification language for formalizing the interactions of service compositions. SOLOIST has been designed with the primary objective of expressing the most significant specification patterns found in the specifications of service-based applications. The language is based on a many-sorted first-order metric temporal logic, extended with new temporal modalities that support aggregate operators for events occurring in a certain time window. We also show how, under certain assumptions, the language can be reduced to linear temporal logic, paving the way for using SOLOIST with established verification techniques, both at design time and at run time.
The original publication is available at

File(s) associated to this reference

Fulltext file(s):

Limited access
facs2012.pdfAuthor postprint795.37 kBRequest a copy

Bookmark and Share SFX Query

All documents in ORBilu are protected by a user license.