Abstract
Service-oriented Computing is rapidly gaining importance across several application domains due to its capability of composing autonomous and loosely-coupled services. In order to support the engineering of service-oriented software applications, foundational theories, service modeling notations, evaluation techniques fully integrated in a pragmatic software engineering approach are required. This article introduces a framework for modeling and prototyping service-oriented applications. The framework consists of a precise and executable language, SCA-ASM, for model-based design, and of a tool for early and quick design evaluation of service assemblies. The language combines the OASIS/OSOA standard Service Component Architecture (SCA) capability of modeling and assembling heterogeneous service-oriented components in a technology agnostic way, with the rigor of the Abstract State Machine (ASM) formal method able to model notions of service behavior, interactions, orchestration, compensation and context-awareness in an abstract but executable way. The tool is based on existing execution environments for ASM models and SCA applications. An SCA-ASM model of a service-oriented component, possibly not yet implemented in code or available as off-the-shelf, can be (i) simulated and evaluated offline, i.e. in isolation from the other components; or (ii) executed as abstract implementation (or prototype) together with the other components implementations according to the chosen SCA assembly. As proof of concept, a case study taken from EU research projects has been considered to show the functionalities and potentialities of the proposed framework.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
Attiogbé C, André P, Ardourel G (2006) Checking component composability. In: Löwe W, Südholt M (eds) Software composition. Lecture notes in computer science, vol 4089. Springer, Berlin, pp 18–33
André P, Ardourel G, Attiogbé C (2008) Composing components with shared services in the Kmelia model. In: Pautasso C, Tanter É (eds) Software composition. LNCS, vol 4954. Springer, Berlin, pp 125–140
Ameur YA, Aït-Sadoune I (2012) Stepwise development of formal models for web services compositions: modelling and property verification. In: Liddle SW, Schewe K-D, Tjoa AM, Zhou X (eds) DEXA (1). Lecture notes in computer science, vol 7446. Springer, Berlin, p 9
Alonso G, Casati F, Kuno HA, Machiraju V (2004) Web Services—concepts, architectures and applications. Data-centric systems and applications. Springer, Berlin
Altenhofen M, Friesen A, Lemcke J (2008) ASMs in service oriented architectures. J Univers Comput Sci 14(12):2034–2058 http://www.jucs.org/jucs_14_12/asms_in_service_oriented
Arcaini P, Gargantini A, Riccobene E (2010) Asmetasmv: A way to link high-level ASM models to low-level NuSMV specifications. In: Frappier M, Glässer U, Khurshid S, Laleau R, Reeves S (eds), ASM. Lecture notes in computer science, vol 5977. Springer, Berlin, pp 61–74
Arcaini P, Gargantini A, Riccobene E (2010) Automatic review of Abstract State Machines by meta property verification. In: Muñoz C (ed) NASA formal methods. NASA conference proceedings, vol NASA/CP-2010-216215, pp 4–13
Arcaini P, Gargantini A, Riccobene E (2011) Coma: conformance monitoring of java programs by Abstract State Machines. In: Khurshid S, Sen K (eds) RV. Lecture notes in computer science, vol 7186. Springer, Berlin, pp 223–238
Arcaini P, Gargantini A, Riccobene E (2013) Combining model-based testing and runtime monitoring for program testing in the presence of nondeterminism. In: Proceedings of the 9th workshop on advances in model based testing (A-MOST 2013)
Arcaini P, Gargantini A, Riccobene E, Scandurra P (2011) A model-driven process for engineering a toolset for a formal method. Softw Pract Exp 41(2): 155–166
Abreu J, Mazzanti F, Fiadeiro JL, Gnesi S (2009) A model-checking approach for service component architectures. In: Lee D, Lopes A, Poetzsch-Heffter A (eds) FMOODS/FORTE. LNCS, vol 5522. Springer, Berlin, pp 219–224
The ASMETA toolset website (2011) http://asmeta.sf.net/
Barros AP, Börger E (2005) A compositional framework for service interaction patterns and interaction flows. In: Lau K-K, Banach R (eds) ICFEM. LNCS, vol 3785. Springer, Berlin, pp 5–35
Börger E, Butler MJ, Bowen JP, Boca P (eds) (2008) In: Proceedings of the Abstract State Machines, B and Z, first international conference, ABZ 2008, London, UK, September 16–18, 2008. Lecture notes in computer science, vol 5238. Springer, Berlin
Ter Beek MH, Bucchiarone A, Gnesi S (2007) Formal methods for service composition. Ann Math Comput Teleinform 1(5): 1–10
Boreale M, Bruni R, De Nicola R, Loreti M (2008) Sessions and pipelines for structured service programming. In: Barthe G, de Boer FS (eds) FMOODS. LNCS, vol 5051. Springer, Berlin, pp 19–38
Brugali D, Gherardi L, Riccobene E, Scandurra P (2011) Coordinated execution of heterogeneous service-oriented components by Abstract State Machines. In: Arbab F, PeterCsaba n++lveczky (eds) FACS. Lecture notes in computer science, vol 7253. Springer, Berlin, pp 331–349
Brugali D, Gherardi L, Scandurra P (2011) A robotics task coordination case study. In: Workshop on software development and integration in robotics (SDIR), 9 May 2011
Bussler C, Haller A (eds) (2006) Business process management workshops, BPM 2005 international workshops, BPI, BPD, ENEI, BPRM, WSCOBPM, BPS, Nancy, France, September 5, 2005, vol 3812. Revised Selected Papers
Bieberstein N, Laird R, Jones K, Mitra T (2008) Executing SOA: a practical guide for the service-oriented architect. Addison-Wesley, Reading
Banti F, Lapadula A, Pugliese R, Tiezzi F (2009) Specification and analysis of SOC systems using COWS: a finance case study. Electr Notes Theor Comput Sci 235: 71–105
Börger E (2007) Modeling workflow patterns from first principles. In: Parent C, Schewe K-D, Storey VC, Thalheim B (eds) ER. Lecture notes in computer science, vol 4801. Springer, Berlin, pp 1–20
OMG Business Process Model and Notation (BPMN) 2.0. (2010). http://www.omg.org/spec/BPMN/2.0
Bernardo M, Padovani L, Zavattaro G (eds) (2009) Formal methods for web services. In: 9th International school on formal methods for the design of computer, communication, and software systems, SFM 2009, Bertinoro, Italy, June 1–6, 2009, Advanced lectures. LNCS, vol 5569. Springer, Berlin
EU project BRICS (Best Practice in Robotics). www.best-of-robotics.org/
Bruni R (2009) Calculi for Service-Oriented Computing. In: Bernardo et al. [BPZ09], pp 1–41
Börger E, Stärk R (2003) Abstract State Machines: a method for high-level system design and analysis. Springer, Berlin
Brugali D, Shakhimardanov A (2010) Component-based robotic engineering (part II): systems and models. Robotics XX(1):1–12
Börger E, Sörensen O, Thalheim B (2009) On defining the behavior of or-joins in business process models. J Univ Comput Sci 15(1): 3–32
Börger E, Thalheim B (2008) Modeling workflows, interaction patterns, web services and business processes: the ASM-based approach. In: Börger et al. [BBBB08], pp 24–38
Cheng BHC, de Lemos R, Giese H, Inverardi P, Magee J (eds) (2009) Software engineering for self-adaptive systems [outcome of a Dagstuhl Seminar]. Lecture notes in computer science, vol 5525. Springer, Berlin
Carioni A, Gargantini A, Riccobene E, Scandurra P (2008) A scenario-based validation language for ASMs. In: Börger et al. [BBBB08], pp 71–84
Chandy M, Schulte R (2010) McGraw-Hill
Ding Z, Chen Z, Liu J (2008) A rigorous model of service component architecture. Electr Notes Theor Comput Sci 207: 33–48
Du D, Liu J, Cao H (2008) A rigorous model of contract-based service component architecture. In: CSSE (2). IEEE Computer Society, pp 409–412
Eclipse Modeling Framework (2008). http://www.eclipse.org/emf/
Filieri A, Ghezzi C, Tamburrelli G (2012) A formal approach to adaptive software: continuous assurance of non-functional requirements. Form Asp Comput 24(2): 163–186
Fiadeiro JL, Lopes A, Bocchi L (2011) An abstract model of service discovery and binding. Form Asp Comput 23(4): 433–463
Fiadeiro JL, Lopes A, Bocchi L, Abreu J (2011) The sensoria reference modelling language. In: Wirsing M, Hölzl MM (eds) Results of the SENSORIA project. Lecture notes in computer science, vol 6582. Springer, Berlin, pp 61–114
Fahland D, Reisig W (2005) ASM-based semantics for BPEL: the negative control flow. In: Proceedings of the 12th international workshop on Abstract State Machines, pp 131–151
Glässer U, Gurevich Y, Veanes M (2004) Abstract communication model for distributed systems. IEEE Trans Softw Eng 30(7): 458–472
Guidi C, Lucchi R, Gorrieri R, Busi N, Zavattaro G (2006) : A calculus for service oriented computing. In: Dan A, Lamersdorf W (eds) ICSOC. LNCS, vol 4294. Springer, Berlin, pp 327–338
Gargantini A, Riccobene E (2001) ASM-based testing: coverage criteria and automatic test sequence. J UCS 7(11): 1050–1067
Gargantini A, Riccobene E, Rinzivillo S (2003) Using spin to generate tests from ASM specifications. In: Börger E, Gargantini A, Riccobene E (eds) Abstract State Machines. Lecture notes in computer science, vol 2589. Springer, Berlin, pp 263–277
Gargantini A, Riccobene E, Scandurra P (2008) A metamodel-based language and a simulation engine for Abstract State Machines. J UCS 14(12): 1949–1983
Gurevich Y, Tillmann N (2005) Partial updates. Theor Comput Sci 336(2–3): 311–342
Hinz S, Schmidt K, Stahl C (2005) Transforming BPEL to Petri nets. In: Proceedings of the international conference on business process management (BPM2005). Lecture notes in computer science, vol 3649. Springer, Berlin, pp 220–235
Louhichi S, Graiet M, Kmimech M, Bhiri MT, Gaaloul W, Cariou E (2011) MDE approach for the generation and verification of sca model. In: Proceedings of the 13th international conference on information integration and web-based applications and services, iiWAS ’11, New York, NY, USA. ACM, pp 317–320
Lanese I, Martins F, Vasconcelos VT, Ravara A (2007) Disciplining orchestration and conversation in service-oriented computing. In: SEFM’07. IEEE, pp 305–314
Lapadula A, Pugliese R, Tiezzi F (2007) A calculus for orchestration of web services. LNCS. Springer, Berlin, pp 33–47
EU project BRICS (2011) Technical Report. A coordination use case. www.best-of-robotics.org/wiki/images/e/e0/coordinationusecaseubergamo.pdf
OMG. Service oriented architecture Modeling Language (SoaML) (2009) ptc/2009-04-01. http://www.omg.org/spec/soaml/1.0/beta1/
Martens A, Moser S (2006) Diagnosing SCA components using wombat. In: Dustdar S, Fiadeiro JL, Sheth AP (eds) Business process management. Lecture notes in computer science, vol 4102. Springer, Berlin, pp 378–388
Mayer P, Schroeder A, Koch N (2008) A model-driven approach to service orchestration. In: IEEE SCC (2), pp 533–536
Mayer P, Schroeder A, Koch N, Knapp A (2009) The UML4SOA profile. Technical Report, LMU Muenchen
Laws S, Combellack M, Feng R, Mahbod H, Nash S (2011) Tuscany SCA in action. Manning Publications
NuSMV: a new symbolic model checker. http://nusmv.fbk.eu/
The PEPA stochastic analyzer. http://www.dcs.ed.ac.uk/pepa/
Riccobene E, Potena P, Scandurra P (2012) Reliability prediction for Service Component Architectures with the sca-asm component model. In: Cortellessa V, Muccini H, Demirörs O (eds) EUROMICRO-SEAA. IEEE Computer Society, pp 125–132
Riccobene E, Scandurra P (2010) An ASM-based executable formal model of service-oriented component interactions and orchestration. In: BM-MDA’10: workshop on behavior modeling in model-driven architecture. ACM
Riccobene E, Scandurra P (2010) Specifying formal executable behavioral models for structural models of service-oriented components. In: van Sinderen M, Sapkota B (eds) ACT4SOC. SciTePress, pp 29–41
Riccobene E, Scandurra P, Albani F (2011) An Eclipse-based SCA design framework to support coordinated execution of services. In: Online proceedings of the 6th workshop of the Italian eclipse community (Eclipse-IT’2011)
Riccobene E, Scandurra P, Albani F (2011) A modeling and executable language for designing and prototyping service-oriented applications. In: EUROMICRO-SEAA. IEEE, pp 4–11
EU project S-Cube. http://www.s-cube-network.eu/
Salaün G, Bordeaux L, Schaerf M (2004) Describing and reasoning on web services using process algebra. In: Proceedings of the IEEE international conference on web services, ICWS ’04, Washington, DC, USA. IEEE Computer Society, p 43
OASIS/OSOA. Service Component Architecture (SCA). http://www.oasis-opencsa.org/sca
The SCA-ASM design framework. https://asmeta.svn.sf.net/svnroot/asmeta/code/experimental/SCAASM
SCA Service Component Architecture Assembly Model Specification—Extensions for Event Processing and Pub/Sub (2009). http://www.oasis-opencsa.org/sca
SCA Tools. http://eclipse.org/stp/sca/
EU project SENSORIA. www.sensoria-ist.eu/
The SENSORIA Approach: White Paper October 17th, 2007. http://www.sensoria-ist.eu/images/stories/frontpage/whitepaper_sensoria.pdf/
The Service-Oriented Modeling Framework in Enterprise Architect. http://www.sparxsystems.com/somf
ter Beek MH, Bucchiarone A, Gnesi S (2007) Web service composition approaches: From industrial standards to formal methods. In: ICIW. IEEE Computer Society, p 15
Apache Tuscany. http://tuscany.apache.org/
van der Aalst WMP, Beisiegel M, van Hee KM, König D, Stahl C (2006) A SOA-based architecture framework. In: Leymann F, Reisig W, Thatte SR, van der Aalst WMP (eds) The role of business processes in service oriented architectures. Dagstuhl seminar proceedings, vol 06291. Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany
van der Aalst WMP, Mooij AJ, Stahl C, Wolf K Service interaction: patterns, formalization, and analysis. In: Bernardo et al. [BPZ09], pp 42–88
Verbeek HMW, van der Aalst WMP (2005) Analyzing BPEL processes using Petri nets. In: Proceedings of the Second International Workshop on Applications of Petri Nets to Coordination, Workflow and Business Process Management. Florida International University, Miami, Florida, USA, pp 59–78
Vaquero LM, Rodero-Merino L, Caceres J, Lindner M (2008) A break in the clouds: towards a cloud definition. SIGCOMM Comput Commun Rev 39(1): 50–55
OASIS Standard WS-BPEL 2.0 (2007). http://docs.oasis-open.org/wsbpel/2.0/wsbpel-v2.0.pdf
Author information
Authors and Affiliations
Corresponding author
Additional information
M.J. Butler
Rights and permissions
About this article
Cite this article
Riccobene, E., Scandurra, P. A formal framework for service modeling and prototyping. Form Asp Comp 26, 1077–1113 (2014). https://doi.org/10.1007/s00165-013-0289-0
Received:
Revised:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00165-013-0289-0