Domenico Bianculli
ABSTRACT
Service-based applications can be realized by composing existing services into new, added-value composite services. The external services with which a service composition interacts are usually known by means of their syntactical interface. However, an interface providing more information, such as a behavioral specification, could be more useful to a service integrator for assessing that a certain external service can contribute to fulfill the functional requirements of the composite application.
Given the requirements specification of a composite service, we present a technique for obtaining the behavioral interfaces - in the form of labeled transition systems - of the external services, by decomposing the global interface specification that characterizes the environment of the service composition. The generated interfaces guarantee that the service composition fulfills its requirements during the execution. Our approach has been implemented in the LTSA tool and has been applied to two case studies.
- D. Alrajeh, J. Kramer, A. Russo, and S. Uchitel. Learning operational requirements from goal models. In Proc. of ICSE'09, pages 265--275. IEEE, 2009. Google Scholar
Digital Library
- L. Baresi, E. Di Nitto, and C. Ghezzi. Towards Open-World Software: Issues and Challenges. IEEE Computer, 39:36--43, 2006. Google ScholarDigital Library
- A. Bertolino, P. Inverardi, P. Pelliccione, and M. Tivoli. Automatic synthesis of behavior protocols for composable Web-services. In Proc. of ESEC/FSE '09, pages 141--150. ACM, 2009. Google ScholarDigital Library
- D. Bianculli, C. Ghezzi, and C. Pautasso. Embedding continuous lifelong verification in service life cycles. In Proc. of PESOS 2009, pages 99--102. IEEE, 2009. Google ScholarDigital Library
- D. Bianculli, C. Ghezzi, P. Spoletini, L. Baresi, and S. Guinea. A guided tour through SAVVY-WS: a methodology for specifying and validating Web service compositions. In Advances in Software Engineering, volume 5316 of LNCS, pages 131--160. Springer, 2008. Google ScholarDigital Library
- I. Brückner. Slicing concurrent real-time system specifications for verification. In Proc. of IFM 2007, volume 4591 of LNCS, pages 54--74. Springer, 2007. Google ScholarDigital Library
- M. Caporuscio, P. Inverardi, and P. Pelliccione. Compositional verification of middleware-based software architecture descriptions. In Proc. of ICSE'04, pages 221--230. IEEE, 2004. Google ScholarDigital Library
- S. C. Cheung and J. Kramer. Checking safety properties using compositional reachability analysis. ACM Trans. Softw. Eng. Methodol., 8(1):49--78, 1999. Google ScholarDigital Library
- C. Damas, B. Lambeau, P. Dupont, and A. van Lamsweerde. Generating annotated behavior models from end-user scenarios. IEEE Trans. Softw. Eng., 31(12):1056--1073, 2005. Google ScholarDigital Library
- H. Foster. WS-Engineer 2008: A service architecture, behaviour and deployment verification platform. In Proc. of ICSOC 2008, volume 5364 of LNCS, pages 728--729. Springer, 2008. Google ScholarDigital Library
- H. Foster, S. Uchitel, J. Magee, and J. Kramer. Model-based verification of Web service compositions. In Proc. of ASE 2003, pages 152--163. IEEE, 2003.Google ScholarDigital Library
- X. Fu, T. Bultan, and J. Su. Conversation protocols: a formalism for specification and verification of reactive electronic services. Theor. Comput. Sci., 328(1--2):19--37, 2004. Google ScholarDigital Library
- D. Giannakopoulou and J. Magee. Fluent model checking for event-based systems. In Proc. of ESEC/FSE-11, pages 257--266. ACM, 2003. Google ScholarDigital Library
- D. Giannakopoulou, C. Păsăreanu, and H. Barringer. Assumption generation for software component verification. In Proc. of ASE 2002, pages 3--12, 2002. Google ScholarDigital Library
- P. Inverardi, P. Pelliccione, and M. Tivoli. Towards an assume-guarantee theory for adaptable systems. In Proc. of SEAMS 2009, pages 106--115. IEEE, 2009. Google ScholarDigital Library
- JavaPathFinder. http://babelfish.arc.nasa.gov/trac/jpf.Google Scholar
- I. Krka, Y. Brun, G. Edwards, and N. Medvidović. Synthesizing partial component-level behavior models from system specifications. In Proc. of ESEC/FSE'09, pages 305--314. ACM, 2009. Google ScholarDigital Library
- S. Labbe, J.-P. Gallois, and M. Pouzet. Slicing communicating automata specifications for efficient model reduction. In Proc. of ASWEC'07, pages 191--200. IEEE, 2007. Google ScholarDigital Library
- N. Lohmann, O. Kopp, F. Leymann, and W. Reisig. Analyzing BPEL4Chor: Verification and participant synthesis. In Proc. of WS-FM 2007, volume 4937 of LNCS, pages 46--60. Springer, 2008. Google ScholarDigital Library
- D. Lorenzoli, L. Mariani, and M. Pezzé. Automatic generation of software behavioral models. In Proc. of ICSE'08, pages 501--510. ACM, 2008. Google ScholarDigital Library
- J. Magee and J. Kramer. Concurrency: State Models And Java Programs. John Wiley & Sons, 2006. Google ScholarDigital Library
- B. Metzler, H. Wehrheim, and D. Wonisch. Decomposition for compositional verification. In Proc. of ICFEM'08, volume 5256 of LNCS, pages 105--125. Springer, 2008. Google ScholarDigital Library
- OASIS. Web Service Business Process Execution Language Version 2.0 Specification, 2007.Google Scholar
- Z. Qiu, X. Zhao, C. Cai, and H. Yang. Towards the theoretical foundation of choreography. In Proc. of WWW 2007, pages 973--982. ACM, 2007. Google ScholarDigital Library
- G. Salaün and T. Bultan. Realizability of choreographies using process algebra encodings. In Proc. of IFM 2009, volume 5423 of LNCS, pages 167--182. Springer, 2009. Google ScholarDigital Library
- S. Uchitel, G. Brunet, and M. Chechik. Synthesis of partial behavior models from properties and scenarios. IEEE Trans. Softw. Eng., 35(3):384--406, 2009. Google ScholarDigital Library
- A. W. Valentin Dallmeier, Christian Lindig and A. Zeller. Mining object behavior with ADABU. In Proc. of WODA 2006, pages 17--24. ACM, 2006. Google ScholarDigital Library
Index Terms
- Interface decomposition for service compositions
Recommendations
Designing level 3 behavioral RESTful web service interfaces
A web service interface contains information about the names of the operations that can be invoked on the service and the input and output parameters of these operations. This information is not enough to facilitate service developer and consumer in ...
Leveraging Integrated Tools for Model-Based Analysis of Service Compositions
ICIW '08: Proceedings of the 2008 Third International Conference on Internet and Web Applications and ServicesDeveloping service compositions, using multiple standards and implementation techniques, typically involves specifying service characteristics in different languages and tools. Examples are defining service composition behaviour, in the form of the ...
Market-Specific Service Compositions: Specification and Matching
SERVICES '15: Proceedings of the 2015 IEEE World Congress on ServicesThe Collaborative Research Centre "On-The-Fly Computing" works on foundations and principles for the vision of the Future Internet. It proposes the paradigm of On-The-Fly Computing, which tackles emerging worldwide service markets. In these markets, ...
Comments