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.

An Accessible Verification Environment for UML Models of Services / F.Banti; R.Pugliese; F.Tiezzi. - In: JOURNAL OF SYMBOLIC COMPUTATION. - ISSN 0747-7171. - STAMPA. - 46(2):(2011), pp. 119-149. [10.1016/j.jsc.2010.08.005]

An Accessible Verification Environment for UML Models of Services

PUGLIESE, ROSARIO;F. Tiezzi
2011

Abstract

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.
2011
46(2)
119
149
F.Banti; R.Pugliese; F.Tiezzi
File in questo prodotto:
File Dimensione Formato  
11JSC-An accessible verification environment for UML models of services.pdf

Accesso chiuso

Tipologia: Versione finale referata (Postprint, Accepted manuscript)
Licenza: Tutti i diritti riservati
Dimensione 2.06 MB
Formato Adobe PDF
2.06 MB Adobe PDF   Richiedi una copia

I documenti in FLORE sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificatore per citare o creare un link a questa risorsa: https://hdl.handle.net/2158/558322
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 8
  • ???jsp.display-item.citation.isi??? 6
social impact