Abstract
This chapter presents different tools that have been developed inside the Sensoria project. Sensoria studied qualitative analysis techniques for verifying properties of service implementations with respect to their formal specifications. The tools presented in this chapter have been developed to carry out the analysis in an automated, or semi-automated, way.
We present four different tools, all developed during the Sensoria project, exploiting new techniques and calculi from the Sensoria project itself.
This work has been partially sponsored by the project Sensoria, IST-2005-016004.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Alves, A., et al.: Web Services Business Process Execution Language Version 2.0. Technical report, OASIS (2006)
Bartoletti, M., Degano, P., Ferrari, G.L.: Enforcing secure service composition. In: Proc. of CSFW-18 2005, pp. 211–223. IEEE Computer Society, Los Alamitos (2005)
Bartoletti, M., Degano, P., Ferrari, G.L.: History-based access control with local policies. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol. 3441, pp. 316–332. Springer, Heidelberg (2005)
Bartoletti, M., Degano, P., Ferrari, G.L., Zunino, R.: Types and effects for resource usage analysis. In: Seidl, H. (ed.) FOSSACS 2007. LNCS, vol. 4423, pp. 32–47. Springer, Heidelberg (2007)
Bartoletti, M., Degano, P., Ferrari, G.L., Zunino, R.: Model checking usage policies. In: Kaklamanis, C., Nielson, F. (eds.) TGC 2008. LNCS, vol. 5474, pp. 19–35. Springer, Heidelberg (2009)
Bartoletti, M., Degano, P., Ferrari, G.L., Zunino, R.: Local policies for resource usage analysis. ACM Trans. Program. Lang. Syst. 31(6) (2009)
Bhat, G., Cleaveland, R., Grumberg, O.: Efficient on-the-fly model checking for CTL*. In: Proc. of LICS 1995, pp. 388–397. IEEE Computer Society, Los Alamitos (1995)
Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without bdds. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)
Bravetti, M., Zavattaro, G.: Towards a unifying theory for choreography conformance and contract compliance. In: Lumpe, M., Vanderperren, W. (eds.) SC 2007. LNCS, vol. 4829, pp. 34–50. Springer, Heidelberg (2007)
Caires, L.: Behavioral and spatial observations in a logic for the pi-calculus. In: Walukiewicz, I. (ed.) FOSSACS 2004. LNCS, vol. 2987, pp. 72–89. Springer, Heidelberg (2004)
Caires, L., Cardelli, L.: A Spatial Logic for Concurrency (Part I). Information and Computation 186(2), 194–235 (2003)
Caires, L., Vieira, H.T.: Conversation types. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 285–300. Springer, Heidelberg (2009)
Carbone, M., Honda, K., Yoshida, N.: Structured communication-centred programming for web services. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 2–17. Springer, Heidelberg (2007)
Carbone, M., Honda, K., Yoshida, N., Milner, R., Brown, G., Ross-Talbot, S.: A theoretical basis of communication–centred concurrent programming. Technical report, W3C (2006)
Fantechi, A., Gnesi, S., Lapadula, A., Mazzanti, F., Pugliese, R., Tiezzi, F.: A model checking approach for verifying COWS specifications. In: Fiadeiro, J.L., Inverardi, P. (eds.) FASE 2008. LNCS, vol. 4961, pp. 230–245. Springer, Heidelberg (2008)
Gnesi, S., Mazzanti, F.: On the fly model checking of communicating UML state machines. In: Proc. of SERA 2004, pp. 331–338. ACIS (2004)
Gnesi, S., Mazzanti, F.: A model checking verification environment for UML statecharts. In: Proc. of XLIII Annual Italian Conference AICA. AICA (2005)
Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In: Proc. of POPL 2008, pp. 273–284. ACM, New York (2008)
Koch, N., Mayer, P., Heckel, R., Gönczy, L., Montangero, C.: UML for Service-Oriented Systems. SensoriaDeliverable 1.4a (September 2007)
Lapadula, A., Pugliese, R., Tiezzi, F.: A calculus for orchestration of web services. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 33–47. Springer, Heidelberg (2007)
Lapadula, A., Pugliese, R., Tiezzi, F.: A Calculus for Orchestration of Web Services (full version). Technical report, Dipartimento di Sistemi e Informatica, Univ. Firenze (2007), http://rap.dsi.unifi.it/cows
Mayer, P., Schroeder, A., Koch, N.: Mdd4soa: Model-driven service orchestration. In: Proc. of EDOC 2008, pp. 203–212. IEEE Computer Society, Los Alamitos (2008)
Mazzanti, F.: UMC User Guide v3.3. Technical Report 2006-TR-33, Istituto di Scienza e Tecnologie dell’Informazione “A. Faedo”. CNR (2006), http://fmt.isti.cnr.it/WEBPAPER/UMC-UG33.pdf
ter Beek, M.H., Fantechi, A., Gnesi, S., Mazzanti, F.: An action/state-based model-checking approach for the analysis of communication protocols for service-oriented applications. In: Leue, S., Merino, P. (eds.) FMICS 2007. LNCS, vol. 4916, pp. 133–148. Springer, Heidelberg (2008)
ter Beek, M.H., Gnesi, S., Koch, N., Mazzanti, F.: Formal verification of an automotive scenario in service-oriented computing. In: Proc. of ICSE 2008, pp. 613–622. ACM Press, New York (2008)
ter Beek, M.H., Gnesi, S., Mazzanti, F., Moiso, C.: Formal modelling and verification of an asynchronous extension of soap. In: Proc. of ECOWS 2006, pp. 287–296. IEEE Computer Society, Los Alamitos (2006)
ter Beek, M.H., Mazzanti, F., Gnesi, S.: CMC-UMC: A framework for the verification of abstract service-oriented properties. In: Proc. of SAC 2009, pp. 2111–2117. ACM Press, New York (2009)
Unified Modeling Language, http://www.uml.org/
Vieira, H.T., Caires, L., Seco, J.C.: The conversation calculus: A model of service oriented computation. In: Gairing, M. (ed.) ESOP 2008. LNCS, vol. 4960, pp. 269–283. Springer, Heidelberg (2008)
Vieira, H.T., Caires, L., Sousa, D.: Checking Services Conformance Based on Spatial Logic Model-Checking (revised). Technical Report TR-DI/FCT/UNL-04/2009, Departamento de Informática, Universidade Nova de Lisboa (2009)
Vieira, H.T., Caires, L., Viegas, R.: The Spatial Logic Model Checker, http://ctp.di.fct.unl.pt/SLMC/
Vieira, H.T., Caires, L., Viegas, R.: The Spatial Logic Model Checker User’s Manual v1.0. Technical Report TR-DI/FCT/UNL-05/2005, Departamento de Informática, Universidade Nova de Lisboa (2005)
Web Services Choreography Working Group WCDL. Web Services Choreography Description Language: Primer (2006), http://www.w3.org/TR/2006/WD-ws-cdl-10-primer-20060619/
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Bartoletti, M. et al. (2011). Tools and Verification. In: Wirsing, M., Hölzl, M. (eds) Rigorous Software Engineering for Service-Oriented Systems. Lecture Notes in Computer Science, vol 6582. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-20401-2_19
Download citation
DOI: https://doi.org/10.1007/978-3-642-20401-2_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-20400-5
Online ISBN: 978-3-642-20401-2
eBook Packages: Computer ScienceComputer Science (R0)