Publications

Authors:

Germiniani, Samuele; Nicoletti, Daniele; Pravadelli, Graziano

Title:

A Baseline Framework for the Qualification of LTL Specification Miners

Year:

2025

Type of item:

Contributo in atti di convegno

Tipologia ANVUR:

Contributo in Atti di convegno

Language:

Inglese

Congresso:

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

Place:

Lyon

Period:

March 31 - April 2

Page numbers:

1-7

Keyword:

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

Short description of contents:

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.

Product ID:

146129

Handle IRIS:

11562/1163727

Last Modified:

June 3, 2025

Bibliographic citation:

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) , Proceedings of "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