Istituto di Scienza e Tecnologie
dell’Informazione “A. Faedo”

This concerns the development of theoretical models of systems that are often distributed and feature complex collaboration, synchronization, cooperation, or communication protocols among sets of components (e.g. grammar systems, team automata, process algebras) and the development of formal techniques to subsequently analyze and verify such models and systems (e.g. model checking). The formal methods are applied in fields like security, service-oriented computing, and software engineering.

Contact: Maurice ter Beek

This topic is at the intersection of the research areas of complex networks, emergence in simple models of computation, and discrete, stochastic or deterministic models of physical space-time (quantum gravity, causal sets). The challenge is to exploit concepts and analytical techniques from the first two fields for developing increasingly realistic discrete models of space-time, with possible induced benefits for the involved technologies.

Contact: Tommaso Bolognesi

Software Product Line Engineering (SPLE) is a paradigm for developing a diversity ofsoftware products and software-intensive systems based on the underlying architectureof an organisation's product platform. Modelling variability in product families has been studied extensively in the literatureon SPLs and in this context we are working to define logics and associated verification tools for the qualitative analysis ofvariability aspects and their application to deal with adaptability and evolvability of systems.

Contact: Stefania Gnesi

In software engineering, requirements define the behaviour and the constraints of a software intensive system before its actual development. Considering that requirements have to be interpreted by different stakeholders of the software process, these are normally provided in informal natural language, which is inherently ambiguous. Ambiguities might lead to the realisation of a software that does not meet the customer's expectation, and could cause costly software failures. The research challenge is to define formal techniques to reduce the ambiguities in requirements, and hence improve the overall quality of the software product.

Contact: Alessio Ferrari

Collective Adaptive Systems (CAS) consist of a large number of spatially distributed heterogeneous entities with decentralised control and varying degrees of complex, autonomous behaviour. These entities or agents may be competing for shared resources even when collaborating to reach common goals, possible leading to non-linear phenomena of the behaviour at the global system level. The pervasive but transparent nature of CAS, together with the importance of the goals that they address, mean that it is imperative that thorough a priori analysis of their design is carried out to investigate all aspects of their behaviour, including quantitative and emergent aspects, before they are put into operation. Formal, scalable, quantitative analysis, which provides multiple perspectives on system behaviour while being based on well-established reasoning techniques, is the approach pursued by the formal modelling community to master such complex systems. In particular, the discovery of precise scaling conditions under which the global behaviour of collective systems can be well approximated by the solution of a set of differential equations obtained from the individual behaviour of system components and their interaction and the insight that such equations can be directly generated from a compositional stochastic process algebraic specification of the individual behaviour of the single entities of the system and their interaction is one of the starting points for the development of scalable formal verification tools, such as model-checking techniques, for CAS.

Contact: Mieke Massink

Service-oriented computing has emerged as a new paradigm based on autonomous, platform-independent computational entities (called  services)  that can be described, published and categorised, and  dynamically discovered and assembled for developing massively  distributed, interoperable, evolvable systems and applications. Service-oriented Systems have then evolved - and are still evolving - towards systems were service components dynamically join into "ensembles" where services are provided through cooperation within the ensemble as well as between them. Fundamental characteristic of such systems are: high dynamicity, open-endedness, high parallelism and massive distribution. Consequently, typical features of such components are self-awareness, self-adaptation, self-expressiveness, and autonomicity. The very nature of these systems requires a priori assurance of correct or at least aceptable behaviour, and modelling and analysis techniques based on a formal, language-first, mathematical foundations are essential for their design and engineering. The topic of  Formal Modelling and Verification of Service Oriented Systems addresses exactly these issues and provides software support tools based on sound mathematical theories, which include qualitative and quantitative (e.g. stochastically timed/probabilistic) modelling languages like process algebras, qualitative and quantitative  temporal logics and related model-checking algorithms and software tools.

Contact: Diego Latella

This topic is related to the application of formal methods to model and analyze complex systems in in the field of railway control systems in order to improve transport outcomes such as transport safety, transport productivity, travel reliability. In fact, modelling and analysis activities are very important to optimize system life-cycle in the design, development, verification and operational stages, and they are essential whenever assessment and certification is required by international standards as the case of railway control systems.

Contact: Stefania Gnesi

Before the beginning of the implementation phase of a project it is extremely beneficial the possibility of building a formal model ofthe system design, and the possibility of verifying the correspondence of it with the intended requirements. To achieve that it is necessary to be able to rely on flexible but powerful model specification languages, on flexible but powerful property description methods, and appropriate tools that allow to check the satisfaction of the properties by the models.

Contact: Franco Mazzanti