Author name cluster

Davide Basile 0001

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

3 papers

1 author row

FM Conference 2026 Conference Paper

Asynchronous Team Automata

Davide Basile 0001
Maurice H. ter Beek
José Proença

Abstract Team automata were introduced as a flexible extension of I/O automata to model collaborative behaviour in component-based and distributed systems. Their distinctive features include multi-party communication and a liberal synchronisation mechanism: components may jointly execute shared actions according to synchronisation policies that specify which subsets of components participate as senders or receivers. While this makes team automata well suited for modelling coordination, existing communication is synchronous and therefore insufficient for capturing certain behavioural aspects (e. g. , due to message reordering) of modern networks and distributed systems, in which communication is typically asynchronous and message delays are unpredictable. In this paper, we introduce asynchronous team automata (ATeams), which extend team automata with buffers to model asynchronous communication, in addition to conventional synchronous interaction. ATeams support individual interactions involving multiple senders and receivers, unlike well-known asynchronous models such as communicating finite-state machines and multi-party session types. We formalise the syntax and operational semantics of ATeams, study well-formedness and well-behavedness conditions, and present the prototypical tool that supports specification, animation and automated checks. This proposes ATeams as a unifying semantic foundation for modelling and analysis of heterogeneous synchronous–asynchronous multi-party interactions.

DOI

FormaliSE Conference 2024 Conference Paper

Time for Networks: Mutation Testing for Timed Automata Networks

David Cortés
James Ortiz 0001
Davide Basile 0001
Jesús Aranda
Gilles Perrouin
Pierre-Yves Schobbens

Mutation Testing (MT) is a technique employed to assess the efficacy of tests by introducing artificial faults, known as mutations, into the system. The goal is to evaluate how well the tests can detect these mutations. These artificial faults are generated using mutation operators, which produce a set of mutations derived from the original system. Mutation operators and frameworks exist for a variety of programming languages, and model-based mutation testing is gaining traction, particularly for timed safety-critical systems. This paper focuses on extending MT to Networks of Timed Automata (NTAs), an area that has not been extensively explored. We introduce mutation operators designed for NTAs specified in UPPAAL, aiming to create temporal interaction faults. We assess the effectiveness of these operators on five UPPAAL NTAs sourced from the literature, specifically examining the generation of equivalent and duplicate mutants. Our results demonstrate a varied prevalence of equivalent mutants (from 12% to 71%) while the number of duplicates is less. In all cases, timed bisimulation was able to process each mutant pair in less than one second. CCS CONCEPTS• Software and its engineering → Software testing and debugging; • Theory of computation → Timed and hybrid models.

Details

FormaliSE Conference 2023 Conference Paper

Mutant Equivalence as Monotonicity in Parametric Timed Games

Davide Basile 0001
Maurice H. ter Beek
Hendrik Göttmann
Malte Lochau

The detection of faults in software systems can be enhanced effectively by model-based mutation testing. The efficiency of this technique is hindered when mutants are equivalent to the original system model, since this makes them useless. Recently, the application of model-based mutation testing to real-time systems modelled as timed games has been investigated, which has resulted in guidelines for statically avoiding equivalent mutants. In this paper, we recast this problem into the framework of parametric timed games. We then prove a correspondence between theoretical results for the detection of equivalent mutants in timed games and the property of monotonicity that is known to hold for a sub-class of parametric timed games called L/U parametric timed games. The presented results not only simplify the theory underlying the detection of equivalent mutants in timed games, but at the same time they improve the expressiveness of a known decidable fragment of parametric timed games for which monotonicity holds.

Details