Leveraging Applications of Formal Methods, Verification and Validation. REoCAS Colloquium in Honor of Rocco De Nicola

This volume contains the proceedings of the Colloquium in honor of Rocco De Nicola’s 70^th birthday, held jointly with the ISOLA 2024’s track on REoCAS (Rigorous Engineering of Collective Adaptive Systems). Rocco De Nicola has significantly contributed to collective adaptive systems through novel approaches for their formal specification, analysis, and verification. The Colloquium features one homage paper and 23 contributions from invited authors who reflected upon these developments within the context of Rocco’s much broader legacy in concurrency theory, distributed systems, domain-specific languages, service-oriented computing, and formal methods, exploring his recent contributions to cybersecurity.

The aim of the REoCAS Colloquium in honor of the 70th birthday of Rocco De Nicola was to acknowledge his scientific impact on the field of collective adaptive systems and, more in general, his much broader legacy in concurrency theory, distributed systems, and formal methods, exploring Rocco’s more recent contributions to cybersecurity. Numerous colleagues have contributed to this task. With this paper, we wish to provide an overview of Rocco’s efforts in shaping computer science research within IMT School for Advanced Studies Lucca, which Rocco has fundamentally shaped since his appointment until his serving as Rector for 2021–2024.

On many occasions, Rocco De Nicola has shown an amazing ability to combine different research topics to offer original results to seemingly different research problems.

We review the origins of Klaim, one of the outstanding ideas of Rocco that, around the mid-nineties, emerged as a solution for problems at the confluence of research in process calculi, models of distributed coordination, and languages for network-aware programming. Besides the opportunity to reconstruct Klaim ’s genesis and reflect on its impact, which continues over time, this paper is a sign of our gratitude to Rocco for sharing his ideas, views, and friendship with us.

The paper introduces a general framework for handling BPMN graphical (semi-formal) models used for describing business process collaborations. It offers a systematic and architecturally comprehensive synthesis of the authors’ prior work on the direct formalization of business process collaborations, the specification of their properties, and their verification and animation. The results exposed in this paper (and many others, indeed) have a direct “causal link” with what the authors learned collaborating with Rocco De Nicola; methodologies and techniques to the specification and design of complex systems and one of Rocco’s scientific career “constants”: formality!

‘Up-to techniques’ represent enhancements of the coinduction proof method and are widely used on coinductive behavioural relations such as bisimilarity. Abstract formulations of these coinductive techniques exist, using fixed-points or category theory.

A proposal has been recently put forward [27] for transporting the enhancements onto the concrete realms of inductive behavioural relations, i.e., relations defined from inductive observables, such as traces or enriched forms of traces. The abstract meaning of such ‘inductive enhancements’, however,  has not been explored. In this paper, we review the theory, and then propose an abstract account of it, using fixed-point theory in complete lattices.

Language equivalence is closely related to Rocco De Nicola’s contributions to concurrency theory. Here we study language equivalence and state reduction for Nondeterministic Finite Automata (NFAs). We work in a linear algebraic setting based on Weighted Automata (WAs) and with a focus on algorithmic aspects. We start from the classic projection-based minimization algorithm for WAs with weights in a field. We analyse the reasons for the failure of this algorithm, in both a theoretical and a practical perspective, when transferred to the poorer algebraic setting of Boolean WAs, that is NFAs. This analysis suggests a different construction based on quotients and an ensuing algorithm applicable to NFAs. Although this algorithm does  not achieve NFAs minimization in general, it is quite effective at state reduction in a practical perspective. Additionally, we show that its linear algebraic formulation is amenable to an efficient vectorized implementation, and discuss the resulting empirical complexity. Experiments conducted with a proof-of-concept implementation of this algorithm across a variety of benchmarks show promising results in comparison to a state-of-the-art tool for NFAs state reduction.

This contribution reflects on a shared teaching experience with Rocco De Nicola that unfolded from 2006 to 2009 at the IMT School for Advanced Studies in Lucca, Italy. During this period, we co-taught a course on formal methods based on process algebras, including Milner’s Calculus of Communicating Systems (CCS). While the course underwent yearly changes in nomenclature and content, it was there that we started using a logical puzzle known as the “50 prisoners puzzle” as a pedagogical tool for CCS modelling and analysis. By bridging theoretical abstractions with concrete problem solving scenarios, we empowered students to grasp the intricacies of process algebras while fostering critical thinking and problem-solving skills. Subsequently I revisited this very same example in subsequent MSc level courses, which I teach at the University of Pisa.

Hennessy and De Nicola established the foundations of formal testing for (discrete) processes. In this paper, we review the challenges before establishing a formal testing theory for quantum processes. We survey the recent approaches that provide credible attacks to these challenges and propose some directions towards a testing theory for quantum processes.

The recent development of quantum communication protocols calls for adequate modelling and verification techniques, which requires abstracting and focusing on the basic features of quantum concurrent systems. Several quantum process calculi and behavioural equivalences have been proposed to address this problem, but they are often incompatible with the prescriptions of quantum theory, as they implicitly define omniscient observers that are capable of exactly discriminating the state of a physical system, therefore contradicting the uncertainty principle. In this paper, we directly model these observational limitations by resorting to testing equivalence for a quantum capable version of CCS, building on the concrete actions and experiments that a real tester can perform. Thus, we obtain an equivalence notion pairing processes that cannot be distinguished by any physically implementable observer.

Probabilistic programming is an emerging paradigm enabling software developers to model uncertainty of real data and to support suitable inference operations directly into computer programs. Probabilistic programs find applications in security/privacy, randomized algorithms, data prediction, generative and probabilistic machine learning and in modeling stochastic dynamical systems. A very challenging task is a how to automatically analyze statically the behavior of probabilistic programs with loops that can generate a continuous and infinite-state space.

The probabilistic programming paradigm is gaining popularity due to the possibility of easily representing probabilistic systems and running a number of off-the-shelf inference algorithms on them. This paper explores how this paradigm can be used to analyse collective systems, in the form of Markov Population Processes (MPPs). MPPs have been extensively used to represent systems of interacting agents, but their analysis is challenging due to the high computational cost required to perform exact simulations of the systems. We represent MPPs as runs of the approximate variant of the Stochastic Simulation Algorithm (SSA), known as \(\tau \)-leaping, which can be seen as a probabilistic program. We apply Gaussian Semantics, a recently proposed inference method for probabilistic programs, to analyse it. We show that \(\tau \)-leaping runs can be effectively analysed using a tailored version of Second Order Gaussian Approximation in which we use a Gaussian Mixture encoding of Poisson distributions. In the resulting analysis, the state of the system is approximated by a multivariate Gaussian Mixture generalizing other common Gaussian approximations such as the Linear Noise Approximation and the Langevin Method. Preliminary numerical experiments show that this approach is able to analyse MPPs with reasonable accuracy on the significant statistics while avoiding expensive numerical simulations.

Driven by and dependent on ICT, like almost everything today, railway transportation has become a critical infrastructure and, as such, is exposed to threats against communication of on-board and wayside components. The shift to cybersecurity brings up the need to comply with new security requirements, and once more security software engineers are confronted with a well-known problem: how to express informal requirements into unambiguous formal expressions that can be translated into enforceable policies or be used to verify the security of a system design. We have experience in translating natural language requirements from standards, regulations, and guidelines into Controlled Natural Language for Data Sharing Agreements (CNL4DSA), a formalism that serves the purpose of bridging natural and formal expressions. The translation of requirements is challenging, calling for a rigorous process of coding agreement between researchers. Following the trend of the time, in this paper, we question whether AI and, in particular, the novel Generative Language Models, can help us with this translation exercise. Previous work shows that AI can help in writing security code, although not always producing secure code; less studied is the quality of generative AI’s working with controlled natural languages in writing requirements for security compliance. Can AI be a valuable tool or companion in this endeavour too? To answer this question, we engage ChatGPT and Microsoft 365 Copilot with the same challenges that we faced when translating cybersecurity requirements for railway systems into CNL4DSA. Comparing our results from some time ago with those of the machine, we found surprising insights, showing the high potentiality of using AI in requirements engineering.

Modeling and analyzing collective adaptive systems with heterogeneous components poses challenges to language designers, software engineers, and computer scientists interested in the formal verification of the modeled systems. This requires the integration of computational, reasoning, and analysis tools, but also of techniques to validate and shed light on the actual behavior described by a model. We build on a methodology built in collaboration with Rocco De Nicola, based on his influential contributions in the modeling and programming of distributed and adaptive systems. Such methodology allows to model and analyze collective adaptive systems equipped with reasoning capabilities. It combines SCEL, a language for programming collective adaptive systems, with Pirlo, a reasoner that can enrich agents with reasoning capabilities, and MultiVeStA, a statistical model checker that can analyze the obtained models by simulating them. Here, we further enrich this methodology with techniques from process-oriented data science, and in particular process mining, to ease the validation and debugging of such models. This follows recent proposals from the literature that validate models by explaining graphically the behaviors observed by a statistical model checker. We demonstrate our approach by considering a simple collision-avoidance robotic scenario where a group of robots moves in an arena while aiming at minimizing the number of collisions.

Inspired by Rocco De Nicola and colleagues’ novel approach to the compositional analysis of complex adaptive systems, we foresee an integrated methodology combining those methods with the logical verification techniques offered by modern proof assistants. We explain our long-term perspective on rigorous analysis of ensembles based on these tools for computerised mathematics and propose some preliminary results to make our methodological viewpoint more concrete.

Modern digital systems are increasingly pervasive and autonomous, also due to the widespread use of AI technologies. They concur to create socio-technical systems, composed of distributed entities interacting with and within the environment, under constant perturbations. This resembles of Collective Adaptive Systems. However, from the human-perspective, AI-enabled autonomous and adaptive systems raise more than just privacy concerns; they also affect other ethical values and human dignity. In this paper, we introduce the concept of ethical-aware Collective Adaptive Systems and we outline challenges to design Collective Adaptive Systems respectful of human ethical values.

Applause is an ancient, widespread collective behaviour by which an audience expresses appreciation at the conclusion of a collective event such as an artistic performance or a public ceremony. In some cultures, it is possible to observe a spontaneous transition from an initially incoherent to a surprisingly synchronised form of applause. Such kind of emergent behaviour has long since fascinated researchers from different disciplines. This paper shows a possible application of formal methods to study similar phenomena. The key idea is to model the audience as a concurrent system, where each person is a separate process that follows the same, simple behaviour. The model can then be automatically analysed to study the possible evolutions of the system as a whole, and in particular to assess the likelihood of emerging synchronisation.

This paper elaborates on the concept that utilizing compositional specifications grounded in formal languages enables the modeling and analysis of intricate collective behaviors within natural systems, such as flocks of birds. Current state-of-the-art approaches primarily focus on formalisms that model system behavior for verification purposes, with less emphasis on quantitative aspects. The objective of this paper is to complement formal specifications with a quantitative abstraction, specifically Markov Population Processes (MPP), thus enabling the measurements of key properties, such as the probability of cohesion among birds, for scenarios under evaluation. Starting with a formal specification inherited from the literature, we develop an MPP model that enhances the types of analysis applicable to collective adaptive systems. Our results confirm that MPP models are suitable for replicating the behavior of flocks and pave the way for quantitative assessments, such as the timeliness of interactions between a prey and flocks.

In distributed agent systems, agents with different abilities work autonomously to reach a common task, in the face of challenges posed by their environment. Two types of structures shape the collective behaviour of the system: a temporal one, defined by the progression of states the system goes through, and a spatial one, defined by the various constraints imposed by the environment on agents’ moves. We argue that both structures can be modelled in terms of suitable topologies, giving rise to a common categorical structure, namely that of trees labelled over a well-founded meet-semilattice, which in turn originates specific kinds of propositional and modal logics. As a result, it is immediate to model some sort of temporal and spatial logic on the properties of state sequences. The resulting logics are extended to integrate the constraints induced by the strategies determining the actual behavior of the agents. The modularity of the approach implies a theoretical simplification and suggests the possibility of a variety of applications.

Function-as-a-Service (FaaS) is a Serverless Cloud paradigm where a platform manages the execution scheduling (e.g., resource allocation, runtime environments) of stateless functions. Recent developments demonstrate the benefits of using domain-specific languages to express per-function scheduling policies, e.g., enforcing the allocation of functions on nodes that enjoy low data-access latencies thanks to proximity and connection pooling. In this paper, we consider APP, one of the languages proposed to specify Allocation Priority Policies in FaaS implemented on top of the popular OpenWhisk serverless platform. The aim of our operational semantics is twofold: on the one hand, it represents the underlying substrate necessary for the application of formal analysis techniques, on the other hand, it can drive consistent implementations of APP on top of the numerous serverless platforms recently proposed.

A multiparty session formalises a set of concurrent interacting participants. By considering that (a) asynchronous communication models are widely adopted in real-life applications and (b) the possibility for a participant to delegate some interactions to another participant is crucial for the expressivity of concurrent interaction protocols, we propose the first type system for asynchronous multiparty sessions with internal delegation. Our type system enjoys relevant properties: Subject Reduction, Session Fidelity, Lock-freedom and Orphan-message-freedom.

We present Code-centric Code Generation (CCG), an approach designed to ease the development and evolution of template-based code generators. The key idea is to generate the required templates from appropriately annotated runnable prototypes written in the target language. In essence, this turns template definition into a two-step process: 1. writing a prototype (base configuration) in the target language, and 2. annotating the prototype’s AST with parameterized operations that, given the required parameters, allow one to transform this base configuration into the intended target code. The advantage of this approach is that prototypes, in contrast to templates, can be conveniently developed and evolved with the full tool support of common software development. We illustrate the ease of CCG-based code generator development by first specifying and then evolving the required templates in order to overcome a detected security vulnerability. A proof-of-concept implementation is publicly available for reproducibility.

Attack Trees are a graphical model of security used to study threat scenarios. While visually appealing and supported by solid theories and effective tools, one of their main drawbacks remains the amount of effort required by security experts to design them from scratch. This work aims at remedying this by providing a method for the automatic generation of Attack Trees from attack logs. The main original feature of our approach w.r.t. existing ones is the use of Process Mining algorithms to synthesize Attack Trees, which allow users to customize the way a set of logs are summarized as an Attack Tree, for example by discarding statistically irrelevant events. Our approach is supported by a prototype that, apart from the derivation and translation of the model, provides the user with an Attack Tree in the RisQFLan format, a tool used for quantitative risk modeling and analysis with Attack Trees. We use literature case studies to illustrate and explore the capabilities of our approach.

Concurrent Constraint Programming (CCP) originated in the late ’80s with Vijay A. Saraswat’s work. In the first ’00s, a “soft” perspective of the constraint store based on a parametric algebraic structure (a c-semiring) was proposed, namely soft CCP (SCCP). This paper enhances this SCCP language with local constraint spaces, where agents can see and interact with only a portion of the information stored. Thus, it is possible to represent areas where an agent can perform operations without affecting other local spaces. The resulting language is security-oriented as actions are checked against (e.g., read/write) rights, and it is quite rich because of nonmonotonic operations in the store (e.g., the removal of constraints is allowed), thus making the coordination of several agents more flexible and adaptive to personal and global goals.

The Internet of Things (IoT) is a rapidly evolving domain that connects various devices and sensors to the internet, facilitating data exchange and automation. However, ensuring the trustworthiness of sensor data utilized by actuators for decision-making is a crucial concern, especially in safety-critical systems that leverage IoT. Untrustworthy data could result in data breaches, system failures, or even loss of life. Therefore, it is essential to specify and analyze the security prerequisites of IoT systems. In this paper, we present SURFING, a requirement language for IoT based on the IoT-LySa process calculus. SURFING allows IoT systems to be specified in terms of their components, communication channels, data flows, and security properties. We also describe the SURFING toolkit, which supports the simulation, and verification of IoT specifications. Furthermore, we have developed a symbolic execution engine for the SURFING toolkit, which enables tracking, navigating, and analyzing data pathways within an IoT specification. This capability helps identify and prevent potential data leaks, tampering, or spoofing. We show the utility of SURFING and its toolkit through a case study involving a street lighting control system.

We continue the development of TinySol, a minimal object-oriented language based on Solidity, the standard smart-contract language used for the Ethereum platform. We first extend TinySol with exceptions and a gas mechanism, and equip it with a small-step operational semantics. Introducing the gas mechanism is fundamental for modelling real-life smart contracts in TinySol, since this is the way in which termination of Ethereum smart contracts is usually ensured. We then devise a type system for smart contracts guaranteeing that such programs never run out of gas at runtime. This is a desirable property for smart contracts, since a transaction that runs out of gas is aborted, but the price paid to run the code is not returned to the invoker.