Verification of quantitative properties of service based applications

Service-based applications (SBAs) are a new category of software, built according to the principle of service-orientation. SBAs may compose third-parties, independent services to build new, added-value service compositions. The distributed ownership and the evolving nature of SBAs make the quality assurance process very important. This is especially true for non-functional requirements, because the quality of service (QoS) provided by a composite service depends on the QoS of the external services in the composition. In terms of quality assurance for SBAs, it is crucial to study both how to formally specify the interactions of SBAs and also how to perform their automatic verification. In this thesis we focus on the verification of the quantitative properties of SBAs captured by some specification patterns specific to the provisioning of SBAs. Specifications are written using the SOLOIST specification language and the verification is performed using the Zot model checker. The thesis describes two ways of translating SOLOIST specifications into a form that can be processed by Zot. As part of this thesis we built a tool that is able to perform bounded history checking on execution traces of SBAs interactions, against properties specified in SOLOIST. We also include results of the experimental evaluation conducted to assess the efficiency of the proposed translations.

Le applicazioni basate sui servizi rappresentano un nuovo tipo di software, che si basa sui principi delle architetture orientate ai servizi. Questo tipo di applicazioni può realizzare composizioni di servizi più complessi, componendo servizi indipendenti e di terze parti. Il fatto che queste applicazioni dipendano da terze parti e possano evolvere continuamente rende il processo di garanzia della qualità del software molto importante. Questo è particolarmente vero per i requisiti non-funzionali, perché la qualità di servizio fornita da un servizio composito dipende dalla qualità dei servizi esterni coinvolti nella composizione. In termini di garanzia della qualità delle applicazioni basate su servizi, è molto importante sia specificare in modo formale le interazioni tra applicazioni e anche eseguire la loro verifica in modo automatico. Questa tesi tratta della verifica di proprietà quantitative di applicazioni basate su servizi; le proprietà corrispondono a quelle esprimibili da una schema di specifiche sviluppato espressamente per il contesto delle applicazioni basate su servizi. Le specifiche sono scritte nel linguaggio di specifica SOLOIST e la verifica è eseguita con il model checker Zot. La tesi descrive due modi di tradurre delle specifiche scritte in SOLOIST in una forma che può essere analizzata da Zot. Parte integrante della tesi è stato anche lo sviluppo di uno strumento che effettua la verifica di proprietà scritte in SOLOIST rispetto a delle storie su tracce di esecuzione che corrispondono a interazioni di applicazioni basate su servizi. Nella tesi sono inclusi i valori della valutazione sperimentale che è stata condotta per valutare l'efficienza delle due traduzioni proposte.