1,720,974 research outputs found
Exploiting clustering and decision-tree algorithms to mine LTL assertions containing non-boolean expressions
No full textState-of-the-art mining tools generate assertions that either describe the temporal relations between Boolean expressions, or extract non-temporal logic formulas between more complex propositions involving arithmetic and/or relational operators. This paper presents a method for generating Linear Temporal Logic (LTL) assertions containing both the temporal dimension and the complexity of non-Boolean expressions. Starting from a set of simulation traces of the design under verification (DUV), our approach generates LTL assertions where the Boolean layer contains expressions of the form c = ne, c ≤ ne, c ≥ ne, c l ≤ ne ≤ c r , where c, c l , c r are constants of numeric type, and ne is a numerical expression predicating over the variables of the DUV. The method exploits a clustering algorithm to mine a meaningful set of propositions following the aforementioned structure. After that, the propositions are used to generate temporal assertions through a decision tree algorithm. Experimental results show real improvements with respect to the state-of-the-art in terms of fault coverage and readability of the mined assertions
Mining signal temporal logic specifications for hybrid systems
No full textSeveral approaches have been proposed over the
years to automatically generate specifications of digital systems
by means of dynamic techniques, which are now ripe to be
applied in large-scale industrial scenarios. On the other hand,
the automatic extraction of specifications for the hybrid domain,
where systems express both discrete and continuous behaviours,
remains mainly unexplored. Therefore, in this paper, we propose
a tool for dynamically mining the specifications of hybrid systems
in the form of assertions compliant with the Signal Temporal
Logic (STL), which has been proven to be effective at capturing
the behaviours of such systems. Our approach takes as input a set
of execution traces of the target system and mixes clustering and
decision-tree algorithms to generate STL assertions that describe
what has been actually implemented
Invited Talk: Pros and Cons of Assertion Mining
No full textAssertion mining flips the way verification works by extracting formal properties from the actual implementation of the target design and searching for inconsistencies with respect to the initial specification. While this removes the burden of time-consuming and error-prone manual definition, are the mined properties actually useful? After reviewing the state of the art concerning existing approaches and tools, this talk questions the pros and cons of assertion mining and describes how mined assertions can be exploited as an effective coverage metrics for functional verification
A Baseline Framework for the Qualification of LTL Specification Miners
No full textOver 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
A Systematic Literature Review on Mining LTL Specifications
Full text linkLinear Temporal Logic (LTL) specifications play a crucial role in the verification process of cyber-physical systems, increasing the guarantees of their correctness. These specifications are vital for ensuring that both hardware and software components behave as expected, especially in complex real-world scenarios. In the last decades, researchers have developed several methodologies and tools to automatically generate LTL specifications, creating an urgent need to organize and synthesize existing literature to ease entry into this field and guide future research efforts. Therefore, starting from a pool of over 3000 papers extracted from the Scopus database in the temporal range 2000-2024, this paper employs the Preferred Reporting Items for Systematic Reviews and Meta-Analyses (PRISMA) methodology to produce a systematic review of mining LTL specifications of hardware and software systems. In particular, we provide a taxonomy of the methods and describe with significant detail all the relevant techniques present at the state of the art. Finally, we discuss the challenges of mining LTL specifications and explore potential directions and opportunities for future research
System-level bug explanation through program slicing and instruction clusterization
No full textMany verification strategies have been proposed to identify unexpected behaviours in system-level implementations. However, when one of such behaviours is found, the verification engineer still has to understand its cause to fix the originating error. This requires a tedious and long process, generally based on manual inspection of the execution traces of the design under verification. Nevertheless, usually only a few instructions in the execution traces are relevant to understand the cause of the unexpected behaviour. To help the verification engineers identifying and focusing on such instructions, we present a tool that automatically removes the irrelevant ones. It works by combining dynamic program slicing with a clustering procedure on the execution traces corresponding to unexpected behaviours. Firstly, program slicing is applied to remove instructions not belonging to the cone of influence of the unexpected behaviour. Then, clusters of instructions based on store operations at the LLVM intermediate representation are created to guide the heuristic in removing further irrelevant instructions
Special Session: A Model-Driven Design Tool for Modelling, Simulation and Assertion-Based Verification of Hybrid Automata
No full textIn a cyber-physical system (CPS), physical and digital components are deeply intertwined, making its design and verification a challenging process. To manage this complexity, hybrid automata are generally adopted to model CPS, allowing the representation of both its discrete and continuous behaviours, which are implemented in the digital and the physical parts. While some tools exist at the state of the art for either modelling or verifying hybrid automata, they present some drawbacks, specifically in terms of ease of use and lack of a unified tool that makes seamless the integration of design, simulation and verification steps. To fill in the gap, we present a new EDA tool for model-driven design and verification of hybrid automata. It does not require designers to learn domain-specific languages, as automatons are graphically modeled; furthermore, the tool integrates a simulation engine for analyzing the evolution of the automata and detecting design errors through the execution of checkers synthesized from Signal Temporal Logic (STL) assertions. The effectiveness of the proposed tool is demonstrated with a case study
A complete assertion-based verification framework from the edge to the cloud
Full text linkAssertion-based verification (ABV) is a well-known approach for checking the functional correctness of a system. Since modern cyber-physical systems are increasingly complex and distributed, it is no longer appropriate applying ABV only to the single components; instead, it is necessary to embrace holistic approaches that look at the entire system. Furthermore, due to the dynamic nature of the system under verification (SUV), ABV cannot be applied only in an offline fashion. Alternatively, it is necessary to extend the verification process to the post-deployment phase; however, this collides with the issues of dealing with a distributed system affected by unpredictable latency and providing limited computational resources. Therefore, it becomes essential to develop a dynamic orchestration approach where checkers perform runtime verification without negatively influencing the computation of the functional parts of the SUV. To fill in the gap, I propose a complete framework to verify complex distributed systems, from the formalisation of specifications to runtime execution. The proposed framework aims at covering several holes in the verification process of systems executing in an edge-to-cloud computing environment
From Informal Specifications to an ABV Framework for Industrial Firmware Verification
No full textFirmware verification for small and medium industries is a challenging task; as a matter of fact, they generally do not have personnel dedicated to such activity. In this context, verification is executed very late in the design flow, and it is usually carried on by the same engineers involved in coding and testing. The specifications initially discussed with the customers are generally not formalised, leading to ambiguity in the expected functionalities. The adoption of a more formal design flow would require the recruitment of people with expertise in formal and semi-formal verification, which is not often compatible with the budget resources of small and medium industries. The alternative is helping the existing engineers with tools and methodologies they can easily adopt without being experts in formal methods. The paper follows this direction by presenting MIST, a framework for the automatic generation of an assertion-based verification environment and its integrated execution inside an off-the-shelf industrial design tool. In particular, MIST allows generating a complete environment to verify C/C++ firmware starting from informal specifications. Given a set of specifications written in natural language, the tool guides the user in translating each specification into an XML formal description, capturing a temporal behaviour that must hold in the design. Our XML format guarantees the same expressiveness of linear temporal logic, but it is designed to be used by designers that are not familiar with formal methods. Once each behaviour is formalised, MIST automatically generates the corresponding testbench and checker to stimulate and verify the design. To guide the verification process, MIST employs a clustering procedure that classifies the internal states of the firmware. Such classification aims at finding an effective ordering to check the expected behaviours and to advise for possible specification holes. MIST has been fully integrated into the IAR System EmbeddedWorkbench. Its effectiveness and efficiency have been evaluated to formalise and check a complex test plan for industrial firmware. © 2021, IFIP International Federation for Information Processing
HARM: A Hint-Based Assertion Miner
Full text linkThis article presents HARM, a tool to generate linear temporal logic (LTL) assertions starting from a set of user-defined hints and the simulation traces of the design under verification (DUV). The tool is agnostic with respect to the design from which the trace was generated, thus the DUV source code is not necessary. The user-defined hints involve LTL templates, propositions, and ranking metrics that are exploited by the assertion miner to reduce the search space and improve the quality of the generated assertions. This way, the tool supports the work of the verification engineer by including his/her insights in the process of automatically generating assertions. The experimental results show real improvements with respect to the state-of-the-art in terms of assertion coverage and scalability
- …
