My main area of research is software engineering, with emphasis on formal methods, verification and validation, and requirements engineering. Specifically, my research interested are focused on the following three main areas:

In the next three sections, I describe in detail my contributions in these three areas. I then provide a short description of other significant results I obtained in different areas. Finally, I outline my current research and my plans for future research.

Verification of logic- and automata-based specification and verification

Model checking, a fully automatic technique to verify a model of a system against a property, is one of my main research interests. Traditional model checking approaches describe a system using an operational model, such as an automaton. Unlike these traditional approaches, in my dissertation I have proposed a technique for (1) specifying systems using a purely descriptive specification, such as a more concise version of linear temporal logic (LTL) with metric (MTL), and (2) verifying such specification performing an automatic translation of the specification into an automaton. Although the translation of temporal logic into automata has been deeply studied, my approach was the first one to deal with very large formulae with metric, with both past and future modalities, and definable on both mono- or bi-infinite time domains. Furthermore, I have contributed to extending the approach to logic specifications enriched with a modular structure that describes the architecture of the system. I implemented most of my techniques in a tool, called MTL2Promela, which is built on top of the Spin model-checking engine. The study of MTL as a purely descriptive specification language, and the development of a model checking technique to verify MTL specifications, led to a challenging research problem: the possibility of transform MTL formulae, that rely on the next operator to encode time distances, in qualitative LTL formulae, that use only the until operator and are more efficiently verifiable. I have addressed and solved this issue by defining an approach for transforming any metric LTL formula into a qualitative one. Such LTL formula is equi-satisfiable over words with variability bounded with respect to the largest distances used in the original formula and with size independent of such distances. Besides the theoretical value of this contribution, may results may also help in practice to simplify the verification of systems with time-granularity heterogeneity, where large distances are required to express the coarse-grained dynamics in terms of fine-grained time units.

Moreover, I have faced some of the challenges arisen by the use of adaptive systems, which are systems able to respond to significant changes in their environment (e.g., a component failure) by modifying their behavior at run time. In particular, an adaptation can be defined as the replacement of a system component with a new version of the component at runtime, from a verification point of view, and this implies that a system needs to be verified every time a component is replaced. However, re-running the verification on the whole system can be extremely expensive and sometimes infeasible. To overcome this problem, I have worked on a methodology, called LOVER, that allows the designer to verify a system at design time, even if some components are unspecified. The LOVER algorithm verifies whether a set of requirements holds and, if needed, produces a set of constraints for the unspecified components. Hence, once the components are specified at run time, they can be verified in isolation against this new set of constraints, without checking again the entire system. Following this idea, I have collaborated in defining AGAVE, another step towards integrating formal verification into an incremental and iterative development style. More precisely, AGAVE considers models expressed in Statecharts, a notation that intrinsically supports iterative specification in the form of states that are refined as both simple sub-Statecharts or the parallel composition of them, and manages to verify such models deriving constraints that can be later proved on the refinement, even in the case it is a parallel composition of Statecharts.

Definition of temporal logic-based languages and verification techniques for these languages

General-purpose model checking techniques offer a general tool for verifying systems, but they do not exploit the peculiarity of a particular context, set of systems, or architectural paradigm. Besides the techniques presented in the previous section, my research concentrated on two particular kinds of systems: service-oriented architectures and self-adaptive systems.

Service-oriented computing is a paradigm that supports the development of distributed systems, which are realized by composing external services to create new functionalities. These systems are developed in an open world, where different services can appear and disappear, and the compositions change dynamically. In this scenario, traditional techniques for verifying systems need to be integrated with a mechanism for studying, at runtime, the dynamic changes of these systems. In this context, I have defined a new language, called ALBERT, that is able to describe functional and non- functional properties of service compositions. I have also proposed techniques to validate service compositions both online and offline. In the more specific context of web services and their composition, I have also collaborated to define a goal language and a technique for verification of such language.

In addition to service-oriented computing, I have also concentrated my attention on self-adaptation, a key characteristic of many modern software systems that is used to tackle their complexity and cope with the many environments in which they can operate. Besides being a requirement per se, self-adaptation impacts other (conventional) requirements of the system—all these new and old requirements must be elicited and represented in a coherent and homogenous way, which is challenging. To address this challenge, I contributed to the definition of FLAGS, a language that enriches some key elements inherited from the well-known goal model KAOS. Specifically, FLAGS extends KAOS with adaptive goals, which can express adaptation strategies in the goal model, and fosters self-adaptation by considering requirements as live, runtime entities. FLAGS is also able to distinguish between crisp and fuzzy goals. Adaptation strategies are triggered by violated goals, and the goal model is modified accordingly to keep a coherent view of the system and enforce adaptation directives on the running system. While defining FLAGS, I have introduced a new semantics for Fuzzy temporal logic. Moreover, and in a completely different setting, recently I have been exploiting the FLAGS features in a medical context. More precisely, I have worked in collaboration with the Spinal Unit at Niguarda Hospital and the Respiratory Medicine Section at Policlinico (both based in Milan, Italy) to define a methodology for eliciting and modeling medical requirements needed to develop videogames with physiotherapeutic purposes.

Practical application of verification techniques

I have applied my knowledge on verification techniques in different fields of computer science and engineering. In my experience, the main goal in doing this kind of research is to exploit the characteristics of the paradigms themselves in order to have a suitable verification approach and to avoid the traditional problems connected with verification (e.g. state explosion problem). Some of the contexts in which I have worked are model checking thecniques for publish/subscribe architectures, verification of graph transformation systems, and model checking of flexible manufacturing systems, and model checking and monitoring of multi-agent systems.