Pubblicazioni

Autori:

Germiniani, Samuele; Nicoletti, Daniele; Pravadelli, Graziano

Titolo:

A Baseline Framework for the Qualification of LTL Specification Miners

Anno:

2025

Tipologia prodotto:

Contributo in atti di convegno

Tipologia ANVUR:

Contributo in Atti di convegno

Lingua:

Inglese

Titolo del Convegno:

ACM/IEEE Design, Automation & Test in Europe Conference & Exhibition (DATE)

Luogo:

Lyon

Periodo:

March 31 - April 2

Intervallo pagine:

1-7

Parole chiave:

Linear Temporal Logic, Specification Mining, SVA Generation, Assertion Mining, Behavior Detection

Breve descrizione dei contenuti:

Over the past few decades, the verification community has developed several specification miners as an alternative to manual assertion definition. However, assessing their effectiveness remains a challenging task. Most studies evaluate these miners using predefined ranking metrics, which often fail to ensure the quality of the inferred specifications, especially when no fixed ground truth exists and the relevance of the specifications varies depending on the use case. This paper presents a comprehensive framework aimed at facilitating the evaluation and comparison of Linear Temporal Logic (LTL) specification miners. Unlike traditional approaches, which struggle with subjective analyses and complex tool configurations, our framework provides a structured method for assessing and comparing the quality of specifications generated by multiple sources, using both semantic and syntactic techniques. To achieve this, the framework offers users an easy-to-extend environment for installing, configuring, and running third-party miners via Docker containers. Additionally’ it supports the inclusion of new evaluation methods through a modular design. Miner comparison can be based either on user-defined designs or on synthetic benchmarks, which are automatically generated to serve as a non-subjective ground truth for the evaluation of the miners. We demonstrate the utility of our framework through comparative analyses with four well-known LTL miners, illustrating its ability to standardize and enhance the specification mining evaluation process.

Id prodotto:

146129

Handle IRIS:

11562/1163727

ultima modifica:

3 giugno 2025

Citazione bibliografica:

Germiniani, Samuele; Nicoletti, Daniele; Pravadelli, Graziano, A Baseline Framework for the Qualification of LTL Specification Miners  in Proc. of ACM/IEEE Design, Automation & Test in Europe Conference & Exhibition (DATE) , Atti di "ACM/IEEE Design, Automation & Test in Europe Conference & Exhibition (DATE)" , Lyon , March 31 - April 2 , 2025 , pp. 1-7

Consulta la scheda completa presente nel repository istituzionale della Ricerca di Ateneo