Objectives:
My research activity takes place in the field of formal methods in computer science and aims at the
development of methodologies for the design of computer, communication, and software systems on the basis of
the following principles:
- Formality – the utilization of rigorous mathematical foundations for defining modeling languages,
so as to avoid ambiguity and enable system description analysis and system property prediction.
- Expressiveness – the capability of easily representing computation and communication concepts as
well as functional and extra-functional aspects.
- Usability – the provision of abstractions related to paradigms, patterns, and styles frequently
occurring in the system development practice, while hiding technical details.
- Efficiency – the automation of the system development process for synthesizing systems from their
formal descriptions by preserving the properties verified on the latter.
- The ultimate goal of my research activity is to increase system quality in terms of dependability and
performance and, at the same time, reduce system development and maintenance costs deriving from the late
discovery of design errors.
- Semantics of concurrent programming languages.
- Process calculi, behavioral equivalences, modal logics.
- Labeled transition systems, Petri nets, event structures.
- Modeling and verification of concurrent and distributed systems.
- Performance evaluation of computer systems and networks.
- Foundations of software architecture and engineering.
- Automated support for model-based software development.
- The stochastic process algebra EMPAgr – Extended Markovian Process Algebra,
together with its interleaving semantics based on reward continuous-time Markov chains and its truly
concurrent semantics based on generalized stochastic Petri nets, and stochastic extensions of bisimulation
and testing equivalences, as illustrated in the Ph.D. thesis
"Theory and Application of Extended
Markovian Process Algebra" and in the publications
[TCS290,
PE50,
JLAP72,
ICTCS2007,
TCS563].
- The architectural description language Æmilia
based on EMPAgr, together with several component-oriented methodologies for detecting
architectural mismatches of functional and extra-functional nature based on behavioral equivalences and
queueing networks, as well as for generating correct-by-construction code, as illustrated in the book
"A Process Algebraic Approach to Software
Architecture Design" and in the publication
[JSS83].
- The modeling and verification software tool
TwoTowers, supporting system description in
Æmilia and system description assessment through model
checking, equivalence checking, information flow security analysis, and performance evaluation (reward
Markov chain solution and discrete event simulation), as illustrated in the Ph.D. thesis
"Theory and Application of Extended
Markovian Process Algebra" and in the publications
[MASCOTS2003,
QEST2004].
- The behavioral metamodel ULTraS – Uniform
Labeled Transition System, which offers a unifying view of numerous behavioral models and behavioral
equivalences appeared in the theoretical computer science literature and has originated new behavioral
equivalences with noteworthy properties in the presence of nondeterminism and quantitative aspects, as
illustrated in the publications
[IC225,
EPEW2013,
JLAMP94,
RDN65,
WADT2020,
LMCS10,
AI52,
TCS546].
- Publications and slides I have produced:
- Research projects in which I have been playing a leading role:
- NiRvAna – Noninterference and
Reversibility Analysis in Private Blockchains [2022-2025]
» funded by MUR – Ministry for University and Research under programme PRIN
» principal investigator.
- CINA – Compositionality,
Interaction, Negotiation and Autonomicity in the Future ICT Society [2013-2016]
» funded by MIUR – Ministry for Education, University, and Research under programme PRIN
» work package leader.
- PaCo – Performability-Aware Computing:
Logics, Models, and Languages [2008-2010]
» funded by MIUR – Ministry for Education, University, and Research under programme PRIN
» principal investigator.
- Scientific events I have organized or chaired:
- Scientific organizations of which I have been member:
- Awards and invitations I have received: