|Thesis abstract: |
In the recent years software engineering researchers and practitioners have focused on new classes of software, such as service-based applications  (SBAs). This kind of software has become very popular because of its flexibility, easy access and rapid development time. For example, it has been adopted as predominant technology in enterprises for building their information systems.
From a research standpoint, engineering SBAs still presents many open issues , because of the dynamic environment in which these applications operate.
In my doctoral dissertation I will tackle the issue of correctness and dependability of SBAs, by proposing innovative verification approaches, grounded in formal methods, for this class of software. Verification will focus on quantitative aspects of SBAs, since they are very relevant from an industrial perspective .
I will explore two main lines of research.
The first one will develop methods and techniques for deriving behavior interfaces of the individual service used in a composite SBA, by decomposing  the requirements specification of the composite service. The obtained behavioral interfaces guarantee that the composite application will fulfill its requirements specification, while it interacts with the partner services at run-time.
Additionally, this decomposition method can enable service selection by exploiting interface equivalence. Automatized service selection at design time can help engineers in the process of composing services, while at run time it can be used for system adaptation, failure recovery and/or avoidance.
The other research direction will focus on efficient techniques for run-time verification of SBAs, leveraging incremental verification approaches .
Runtime verification is important because it bridges the gap between the formal specification that is applied at design time and testing, which validates implementations at runtime, but lacks the formality. Runtime verification is applied when desiging dependable safety-critical systems.
 Luciano Baresi, Elisabetta Di Nitto, and Carlo Ghezzi. Toward open-world software: Issue and challenges. Computer, 39(10):36¿43, October 2006.
 Domenico Bianculli, Carlo Ghezzi, Cesare Pautasso, and Patrick Senti. Specification patterns from research to industry: a case study in service-based applications. In Proceedings of the 34th International Conference on Software Engineering (ICSE 2012), Zürich, Switzerland, pages 968¿976. IEEE Computer Society Press, June 2012.
 Domenico Bianculli, Dimitra Giannakopoulou, and Corina S. P?s?reanu. Interface decomposition for service compositions. In Proceedings of the 33rd International Conference on Software Engineering (ICSE 2011), Honolulu, Hawaii, USA, pages 501¿510. ACM, May 2011.
 Elisabetta Di Nitto, Carlo Ghezzi, Andreas Metzger, Mike Papazoglou, and Klaus Pohl. A journey to highly dynamic, self-adaptive service-based applications. Automated Software Engg., 15(3-4):313¿341, December 2008.
 Thomas Erl. Service-Oriented Architecture: Concepts, Technology, and Design. Prentice Hall PTR, Upper Saddle River, NJ, USA, 2005.
 Carlo Ghezzi. Evolution, adaptation, and the quest for incrementality. In Proceedings of the 17th Monterey conference on Large-Scale Complex IT Systems: development, operation and management, pages 369¿379, Berlin, Heidelberg, 2012. Springer-Verlag.