×

An accessible verification environment for UML models of services. (English) Zbl 1215.68065

Summary: Service-Oriented Architectures (SOAs) provide methods and technologies for modelling, programming and deploying software applications that can run over globally available network infrastructures. Current software engineering technologies for SOAs, however, remain at the descriptive level and lack rigorous foundations enabling formal analysis of service-oriented models and software. To support automated verification of service properties by relying on mathematically founded techniques, we have developed a software tool that we called Venus (Verification ENvironment for UML models of Services). Our tool takes as an input service models specified by UML 2.0 activity diagrams according to the UML4SOA profile, while its theoretical bases are the process calculus COWS and the temporal logic SocL. A key feature of Venus is that it provides access to verification functionalities also to those users not familiar with formal methods. Indeed, the tool works by first automatically translating UML4SOA models and natural language statements of service properties into, respectively, COWS terms and SocL formulae, and then by automatically model checking the formulae over the COWS terms. In this paper we present the tool, its architecture and its enabling technologies by also illustrating the verification of a classical ‘travel agency’ scenario.

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)

Software:

ACTLW; VIATRA2; COWS; SPIN
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Arons, T.; Hooman, J.; Kugler, H.; Pnueli, A.; van der Zwaag, M., Deductive verification of UML models in TLPVS, (UML. UML, LNCS (2004), Springer), 335-349
[2] Banti, F.; Lapadula, A.; Pugliese, R.; Tiezzi, F., Specification and analysis of SOC systems using COWS: a finance case study, (WWV. WWV, ENTCS (2009), Elsevier), 71-105
[3] Banti, F., Pugliese, R., Tiezzi, F., 2009b. Towards a Framework for the Verification of UML Models of Services. In: WWV.; Banti, F., Pugliese, R., Tiezzi, F., 2009b. Towards a Framework for the Verification of UML Models of Services. In: WWV. · Zbl 1215.68065
[4] Bartoletti, M.; Degano, P.; Ferrari, G. L.; Zunino, R., Semantics-Based Design for Secure Web Services, IEEE Trans. Softw. Eng., 34, 1, 33-49 (2008)
[5] Bauer, J.; Nielson, F.; Nielson, H.; Pilegaard, H., Relational analysis of correlation, (SAS. SAS, LNCS (2008), Springer), 32-46 · Zbl 1149.68308
[6] Beato, M. E.; Barrio-Solrzano, M.; Cuesta, C. E.; de la Fuente, P., UML automatic verification tool with formal methods, ENTCS, 127, 4, 3-16 (2005)
[7] Bocchi, L.; Laneve, C.; Zavattaro, G., A calculus for long-running transactions, (FMOODS. FMOODS, LNCS (2003), Springer), 124-138 · Zbl 1253.68056
[8] Boreale, M.; Bruni, R.; De Nicola, R.; Loreti, M., Sessions and pipelines for structured service programming, (FMOODS. FMOODS, LNCS, vol. 5051 (2008), Springer), 19-38
[9] Butler, M.; Hoare, C.; Ferreira, C., A trace semantics for long-running transactions, (25 Years Communicating Sequential Processes. 25 Years Communicating Sequential Processes, LNCS, vol. 3525 (2005), Springer), 133-150 · Zbl 1081.68644
[10] Carbone, M.; Honda, K.; Yoshida, N., Structured communication-centred programming for web services, (ESOP. ESOP, LNCS (2007), Springer), 2-17 · Zbl 1187.68064
[11] Clarke, E.; Emerson, E., Design and synthesis of synchronization skeletons using branching-time temporal logic, (Logic of Programs. Logic of Programs, LNCS, vol. 131 (1981), Springer), 52-71
[12] Clarke, E.; Grumberg, O.; Peled, D., Model Checking (1999), MIT Press
[13] Compton, K., Gurevich, Y., Huggins, J., Shen, W., 2000. An Automatic Verification Tool for UML. Tech. rep., Dept. of EECS, University of Michigan.; Compton, K., Gurevich, Y., Huggins, J., Shen, W., 2000. An Automatic Verification Tool for UML. Tech. rep., Dept. of EECS, University of Michigan.
[14] Crane, M.; Dingel, J., Towards a UML virtual machine: implementing an interpreter for UML 2 actions and activities, (CASCON (2008), ACM), 96-110
[15] Csertán, G., Huszerl, G., Majzik, I., Pap, Z., Pataricza, A., Varró, D., 2002. VIATRA — visual automated transformations for formal verification and validation of UML models. In: ASE. IEEE, pp. 267-270.; Csertán, G., Huszerl, G., Majzik, I., Pap, Z., Pataricza, A., Varró, D., 2002. VIATRA — visual automated transformations for formal verification and validation of UML models. In: ASE. IEEE, pp. 267-270.
[16] De Nicola, R., Latella, D., Loreti, M., Massink, M., 2010. SoSL: service oriented stochastic logic. In: M. Wirsing and M. Hölzl (eds.), Rigorous Software Engineering for Service-Oriented Systems — Results of the SENSORIA Project on Software Engineering for Service-Oriented Computing. Springer (in press).; De Nicola, R., Latella, D., Loreti, M., Massink, M., 2010. SoSL: service oriented stochastic logic. In: M. Wirsing and M. Hölzl (eds.), Rigorous Software Engineering for Service-Oriented Systems — Results of the SENSORIA Project on Software Engineering for Service-Oriented Computing. Springer (in press).
[17] De Nicola, R.; Vaandrager, F., Action versus state based logics for transition systems, (Proc. of the Ecole de Printemps on Semantics of Concurrency. Proc. of the Ecole de Printemps on Semantics of Concurrency, LNCS, vol. 469 (1990), Springer), 407-419
[18] De Nicola, R.; Vaandrager, F., Three logics for branching bisimulation, Journal of the ACM, 42, 2, 458-487 (1995) · Zbl 0886.68064
[19] Dong, W.; Wang, J.; Qi, X.; Qi, Z., Model checking UML statecharts, (APSEC (2001), IEEE), 363-370
[20] Eichner, C.; Fleischhack, H.; Meyer, R.; Schrimpf, U.; Stehno, C., Compositional semantics for UML 2.0 sequence diagrams using petri nets, (SDL. SDL, LNCS, vol. 3530 (2005), Springer), 133-148
[21] Fantechi, A.; Gnesi, S.; Lapadula, A.; Mazzanti, F.; Pugliese, R.; Tiezzi, F., A model checking approach for verifying COWSspecifications, (FASE. FASE, LNCS, vol. 4961 (2008), Springer), 230-245
[22] Fantechi, A., Gnesi, S., Lapadula, A., Mazzanti, F., Pugliese, R., Tiezzi, F., 2010. A logical verification methodology for service-oriented computing. Tech. Rep., DSI, Università di Firenze. Available at:http://rap.dsi.unifi.it/cows/papers/cows_logic_full.pdf; Fantechi, A., Gnesi, S., Lapadula, A., Mazzanti, F., Pugliese, R., Tiezzi, F., 2010. A logical verification methodology for service-oriented computing. Tech. Rep., DSI, Università di Firenze. Available at:http://rap.dsi.unifi.it/cows/papers/cows_logic_full.pdf
[23] Ferrari, G.; Guanciale, R.; Strollo, D., Event based service coordination over dynamic and heterogeneous networks, (ICSOC. ICSOC, LNCS, vol. 4294 (2006), Springer), 453-458
[24] Geguang, P.; Xiangpeng, Z.; Shuling, W.; Zongyan, Q., Towards the semantics and verification of BPEL4WS, (WLFM. WLFM, ENTCS, vol. 151/2 (2005), Elsevier), 33-52
[25] (Grumberg, O.; Veith, H., 25 years of model checking — history, achievements, perspectives. 25 years of model checking — history, achievements, perspectives, LNCS, vol. 5000 (2008), Springer) · Zbl 1139.68003
[26] Guidi, C.; Lucchi, R.; Gorrieri, R.; Busi, N.; Zavattaro, G., SOCK: a calculus for service oriented computing, (ICSOC. ICSOC, LNCS (2006), Springer), 327-338
[27] Holzmann, G., The Spin Model Checker — Primer and Reference Manual (2003), Addison-Wesley
[28] Huth, M.; Ryan, M., Logic in Computer Science: Modelling and Reasoning About Systems (2004), Cambridge University Press · Zbl 1073.68001
[29] Jürjens, J.; Shabalin, P., Automated verification of UMLsec models for security requirements, (UML. UML, LNCS, vol. 3273 (2004), Springer), 365-379
[30] Knapp, A.; Merz, S.; Rauh, C., Model checking — timed UML state machines and collaborations, (FTRTFT. FTRTFT, LNCS (2002), Springer), 395-416
[31] Lanese, I.; Martins, F.; Ravara, A.; Vasconcelos, V., Disciplining orchestration and conversation in service-oriented computing, (SEFM (2007), IEEE), 305-314
[32] Lapadula, A.; Pugliese, R.; Tiezzi, F., A calculus for orchestration of web services, (ESOP. ESOP, LNCS (2007), Springer), 33-47, full version available at: http://rap.dsi.unifi.it/cows/papers/cows-esop07-full.pdf · Zbl 1187.68070
[33] Lapadula, A.; Pugliese, R.; Tiezzi, F., Regulating data exchange in service oriented applications, (FSEN. FSEN, LNCS (2007), Springer), 223-239 · Zbl 1141.68509
[34] Lapadula, A.; Pugliese, R.; Tiezzi, F., A formal account of WS-BPEL, (COORDINATION. COORDINATION, LNCS (2008), Springer), 199-215
[35] Latella, D.; Majzik, I.; Massink, M., Automatic verification of a behavioural subset of UML statechart diagrams using the SPIN model-checker, Formal Asp. Comput., 11, 6, 637-664 (1999) · Zbl 0966.68124
[36] Latella, D.; Massink, M., A formal testing framework for UML statechart diagrams behaviours: from theory to automatic verification, (HASE (2001), IEEE), 11-22
[37] Mayer, P., Koch, N., Schroeder, A., 2008a. The UMLSOAhttp://www.uml4soa.eu/profile; Mayer, P., Koch, N., Schroeder, A., 2008a. The UMLSOAhttp://www.uml4soa.eu/profile
[38] Mayer, P.; Schroeder, A.; Koch, N., Mdd4soa: model-driven service orchestration, (EDOC (2008), IEEE), 203-212
[39] Meolic, R.; Kapus, T.; Brezocnik, Z., ACTLW — an action-based computation tree logic with unless operator, Elsevier Information Sciences, 178, 6, 1542-1557 (2008) · Zbl 1134.68033
[40] Milner, R.; Parrow, J.; Walker, D., A calculus of mobile processes, I and II, Information and Computation, 100, 1, 1-40 (1992), 41-77 · Zbl 0752.68036
[41] No Magic Inc., 2009. MagicDraw UML academic personal edition 16.5. Available at: http://www.magicdraw.com/; No Magic Inc., 2009. MagicDraw UML academic personal edition 16.5. Available at: http://www.magicdraw.com/
[42] OASIS WSBPEL TC, April 2007. Web Services Business Process Execution Language Version 2.0. Tech. rep., OASIS.; OASIS WSBPEL TC, April 2007. Web Services Business Process Execution Language Version 2.0. Tech. rep., OASIS.
[43] Object Management Group, 2007a. Unified Modeling Language (UML), version 2.1.2.; Object Management Group, 2007a. Unified Modeling Language (UML), version 2.1.2.
[44] Object Management Group, 2007b. XMI Mapping Specification, v2.1.1.; Object Management Group, 2007b. XMI Mapping Specification, v2.1.1.
[45] Object Management Group, 2008. Sevice oriented architecture Modeling Language (SoaML) — Specification for the UML Profile and Metamodel for Services (UPMS).; Object Management Group, 2008. Sevice oriented architecture Modeling Language (SoaML) — Specification for the UML Profile and Metamodel for Services (UPMS).
[46] Prandi, D.; Quaglia, P., Stochastic COWS, (ICSOC. ICSOC, LNCS, vol. 4749 (2007), Springer), 245-256
[47] Störrle, H.; Hausmann, J., Towards a Formal Semantics of UML 2.0 Activities, (Software Engineering. Software Engineering, LNI (2005), GI), 117-128
[48] Sun Microsystems, 2009. The Swing Tutorial. Available at: http://java.sun.com/docs/books/tutorial/uiswing; Sun Microsystems, 2009. The Swing Tutorial. Available at: http://java.sun.com/docs/books/tutorial/uiswing
[49] Tabuchi, N.; Sato, N.; Nakamura, H., Model-driven performance analysis of UML design models based on stochastic process algebra, (ECMDA-FA. ECMDA-FA, LNCS, vol. 3748 (2005), Springer), 41-58
[50] ter Beek, M.; Gnesi, S.; Mazzanti, F., Formal verification of an automotive scenario in service-oriented computing, (ICSE (2008), ACM), 613-622
[51] Varró, D., Transformation of UML models to CSP: a case study for graph transformation tools, (AGTIVE. AGTIVE, LNCS, vol. 5088 (2008), Springer), 540-565
[52] VIATRA2 Developer Team, 2009. VIATRA2 Project Overview. Available at: http://eclipse.org/gmt/VIATRA2/; VIATRA2 Developer Team, 2009. VIATRA2 Project Overview. Available at: http://eclipse.org/gmt/VIATRA2/
[53] Vieira, H.; Caires, L.; Seco, J. C., The conversation calculus: a model of service-oriented computation, (ESOP. ESOP, LNCS, vol. 4960 (2008), Springer), 269-283 · Zbl 1133.68388
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.