FormaliSE 2024
Fri 12 - Sun 21 April 2024 Lisbon, Portugal
co-located with ICSE 2024

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.

Sun 14 Apr

Displayed time zone: Lisbon change

14:00 - 15:30
Timed behavior specification and verificationFormaliSE 2024 at Eugénio de Andrade
Chair(s): João F. Ferreira INESC-ID and IST, University of Lisbon
14:00
30m
Talk
Diagnosing Violations of Time-based Properties Captured in iCFTL
FormaliSE 2024
Cristina Stratan University of Luxembourg, Joshua Heneage Dawes University of Luxembourg, Domenico Bianculli University of Luxembourg
14:30
30m
Talk
Time for Networks: Mutation Testing for Timed Automata Networks
FormaliSE 2024
David Cortés Universidad del Valle, James Ortiz Université de Namur, Davide Basile Formal Methods and Tools lab, ISTI-CNR, Pisa, Italy, Jesus Aranda Universidad del Valle, Gilles Perrouin Fonds de la Recherche Scientifique - FNRS & University of Namur, Pierre Yves Schobbens Université de Namur
15:00
30m
Talk
Verifying Opacity of Discrete-Timed Automata
FormaliSE 2024
Julian Klein Technische Universität Berlin, Paul Kogel Technische Universität Berlin, Sabine Glesner Technische Universität Berlin