Abstract
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.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
de Alfaro, L.: Temporal Logics for the Specification of Performance and Reliability. In: Reischuk, R., Morvan, M. (eds.) STACS 1997. LNCS, vol. 1200, pp. 165–176. Springer, Heidelberg (1997)
Andrews, T., et al.: Business Process Execution Language for Web Services, Version 1.1 (2003)
Baresi, L., Bianculli, D., Ghezzi, C., Guinea, S., Spoletini, P.: Validation of web service compositions. IET Softw. 1(6), 219–232 (2007)
Baresi, L., Di Nitto, E. (eds.): Test and Analysis of Web Services. Springer (2007)
Baresi, L., Di Nitto, E., Ghezzi, C.: Toward open-world software: Issue and challenges. IEEE Computer 39(10), 36–43 (2006)
Basin, D., Klaedtke, F., Müller, S.: Policy Monitoring in First-Order Temporal Logic. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 1–18. Springer, Heidelberg (2010)
Bauer, A., Goré, R., Tiu, A.: A First-Order Policy Language for History-Based Transaction Monitoring. In: Leucker, M., Morgan, C. (eds.) ICTAC 2009. LNCS, vol. 5684, pp. 96–111. Springer, Heidelberg (2009)
Bianculli, D., Ghezzi, C., Pautasso, C., Senti, P.: Specification patterns from research to industry: a case study in service-based applications. In: Proc. of ICSE 2012, pp. 968–976. IEEE Computer Society (2012)
Boker, U., Chatterjee, K., Henzinger, T.A., Kupferman, O.: Temporal specifications with accumulative values. In: Proc. of LICS 2011, pp. 43–52. IEEE Computer Society (2011)
Canfora, G., Di Penta, M.: Service-Oriented Architectures Testing: A Survey. In: De Lucia, A., Ferrucci, F. (eds.) ISSSE 2006-2008. LNCS, vol. 5413, pp. 78–105. Springer, Heidelberg (2009)
Deutsch, A., Sui, L., Vianu, V.: Specification and verification of data-driven web applications. J. Comput. Syst. Sci. 73(3), 442–474 (2007)
Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Property specification patterns for finite-state verification. In: Proc. of FMSP 1998, pp. 7–15. ACM (1998)
Finkbeiner, B., Sankaranarayanan, S., Sipma, H.: Collecting statistics over runtime executions. Formal Methods in System Design 27, 253–274 (2005)
Gauci, A., Pace, G.J., Colombo, C.: Statistics and runtime verification. Tech. rep., University of Malta (2010)
Ghezzi, C., Guinea, S.: Run-time monitoring in service-oriented architectures. In: Baresi, Di Nitto [4] pp. 237–264
Gruhn, V., Laue, R.: Patterns for timed property specifications. Electron. Notes Theor. Comput. Sci. 153(2), 117–133 (2006)
Hallé, S., Villemaire, R.: Runtime monitoring of message-based workflows with data. In: Proc. of EDOC 2008, pp. 63–72. IEEE Computer Society (2008)
Hallé, S., Villemaire, R., Cherkaoui, O.: Specifying and validating data-aware temporal web service properties. IEEE Trans. Softw. Eng. 35(5), 669–683 (2009)
Hella, L., Libkin, L., Nurmonen, J., Wong, L.: Logics with aggregate operators. J. ACM 48, 880–907 (2001)
Josuttis, N.: SOA in Practice: The Art of Distributed System Design. O’Reilly Media, Inc. (2007)
Kamp, H.W.: Tense Logic and the Theory of Linear Order. PhD thesis, University of California at Los Angeles, USA (1968)
Keller, A., Ludwig, H.: The WSLA framework: specifying and monitoring service level agreement for web services. J. Netw. Syst. Manage. 11(1) (2003)
Konrad, S., Cheng, B.H.C.: Real-time specification patterns. In: Proc. of ICSE 2005, pp. 372–381. ACM (2005)
Kowalski, R., Sergot, M.: A logic-based calculus of events. New Gen. Comput. 4, 67–95 (1986)
Laroussinie, F., Meyer, A., Petonnet, E.: Counting LTL. In: Proc. of TIME 2010, pp. 51–58. IEEE (2010)
Laroussinie, F., Meyer, A., Petonnet, E.: Counting CTL. In: Ong, L. (ed.) FOSSACS 2010. LNCS, vol. 6014, pp. 206–220. Springer, Heidelberg (2010)
Mahbub, K., Spanoudakis, G.: Monitoring WS-Agreements: An event calculus-based approach. In: Baresi, Di Nitto [4], pp. 265–306
Müller, C., Martín-Díaz, O., Ruiz-Cortés, A., Resinas, M., Fernández, P.: Improving Temporal-Awareness of WS-Agreement. In: Krämer, B.J., Lin, K.-J., Narasimhan, P. (eds.) ICSOC 2007. LNCS, vol. 4749, pp. 193–206. Springer, Heidelberg (2007)
Papazoglou, M.P.: The Challenges of Service Evolution. In: Bellahsène, Z., Léonard, M. (eds.) CAiSE 2008. LNCS, vol. 5074, pp. 1–15. Springer, Heidelberg (2008)
Pelov, N., Denecker, M., Bruynooghe, M.: Well-founded and stable semantics of logic programs with aggregates. Theory and Practice of Logic Programming 7(3), 301–353 (2007)
Pradella, M., Morzenti, A., San Pietro, P.: The symmetry of the past and of the future: bi-infinite time in the verification of temporal properties. In: Proc. of ESEC-FSE 2007, pp. 312–320. ACM (2007)
Pradella, M., Morzenti, A., San Pietro, P.: A Metric Encoding for Bounded Model Checking. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 741–756. Springer, Heidelberg (2009)
Rabinovich, A.: Complexity of Metric Temporal Logics with Counting and the Pnueli Modalities. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol. 5215, pp. 93–108. Springer, Heidelberg (2008)
Raimondi, F., Skene, J., Emmerich, W.: Efficient online monitoring of web-service slas. In: Proc. of SIGSOFT 2008/FSE-16, pp. 170–180. ACM, New York (2008)
Salaün, G.: Analysis and verification of service interaction protocols - a brief survey. In: Proc. of TAV-WEB 2010. EPTCS, vol. 35, pp. 75–86 (2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bianculli, D., Ghezzi, C., San Pietro, P. (2013). The Tale of SOLOIST: A Specification Language for Service Compositions Interactions. In: Păsăreanu, C.S., Salaün, G. (eds) Formal Aspects of Component Software. FACS 2012. Lecture Notes in Computer Science, vol 7684. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-35861-6_4
Download citation
DOI: https://doi.org/10.1007/978-3-642-35861-6_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-35860-9
Online ISBN: 978-3-642-35861-6
eBook Packages: Computer ScienceComputer Science (R0)