Lifelong Verification of Dynamic Service Compositions

Service-oriented computing is an emerging paradigm that supports the development of distributed applications, which are realized by composing third-party services to provide new added-value services. These applications live in an open world, where new services can appear and disappear, and compositions may change dynamically. In this scenario, the traditional boundary between design time and run time is blurring. Verification, which traditionally pertains to design time, must now extend to run time. During my PhD studies, I defined a holistic approach for lifelong verification of dynamic service compositions.

Relevant projects

Automated performance assessment of service-oriented middleware

Middleware for Web service compositions, such as BPEL engines, provides the execution environment for services as well as additional functionalities, such as monitoring and self-tuning. Given its role in service provisioning, it is very important to assess the performance of middleware in the context of a SOA. SOABench is a framework for the automatic generation and execution of testbeds for benchmarking middleware for composite Web services and for assessing the performance of existing SOA infrastructures. SOABench defines a testbed model characterized by the composite services to execute, the workload to generate, the deployment configuration to use, the performance metrics to gather, the data analyses to perform on them, and the reports to produce.

Transparent Reputation Management for Composite Web Services

The dependability of composite services is largely affected by their constituent Web services. Composite services have to operate in an open and dynamically changing environment in order to leverage the best performing services available at the moment. Hence, there is the need for an efficient mechanism to provide reliable service rankings. We designed a novel, generic, and customizable reputation infrastructure to automatically and transparently monitor the execution of composite services, taking both functional and non-functional properties into account. The experienced Web service Quality-of-Service is communicated to a configurable reputation mechanism that publishes service rankings. Our reputation infrastructure supports notifications upon changes in service reputation, enabling self-tuning and self-healing properties in the execution of composite services.

See also the ReMan project

Model Checking Web Service Compositions

As part of my master thesis at Politecnico di Milano, I developed the Bpel2Bir framework, based on the model checker Bogor, for the formal verification of web service orchestrations described in BPEL4WS.

Model Checking Temporal Metric Specifications

As a graduate student at Politecnico di Milano, I started a collaboration with the Formal Methods Group, working on TRIO, a linear-time temporal logic with a quantitative metric on time.
Under the guidance of Paola Spoletini, I implemented Trio2Promela, a tool for model checking TRIO specifications by means of Spin.