An Advanced Interface for Analysis of Distributed Automation

The AIDA project aims to design a tool that allows you to automate the process of verifying the requirements of a product.

In particular, in AIDA we want to experiment and integrate natural language management techniques and formal verification tools.

The goal is to obtain a tool that allows you to automatically check whether a specific product, whose characteristics are described in natural language, corresponds to certain requirements, also expressed in natural language.

Learn More


Analysis and selection of the tools to be used

The first part of the work concerned the analysis and selection of the tools to be used.
The following tools were evaluated, resulting from a pre-selection carried out during the proposal submission:

The Goal

To evaluate different tools and select the most relevant and valid ones for use in subsequent phases

In addition, the following tools were also evaluated, which did not emerge during the pre-selection:

Selection Criteria


Which collects a set of considerations relating to the user interface, information feedback, flexibility, error management and user guide.


Effectiveness, or degree of ability to carry out the task assigned.


Especially in terms of time spent solving certain tasks.


Which implies both the fact that the tool does not go into error, and the ability of the tool to guide the user in correcting incorrect ways of using it.

Documentation and Support

Availability of on-line documentation and/or technical support.

The Results

The results of the evaluation showed that no tool, among those analyzed, allows to manage both the conversion of natural language sentences into logical expressions, and the evaluation of the expressions themselves to prove whether the property to prove (the "theorem") is valid or not. However, some tools have shown that they can be used to perform one of the two tasks correctly. In particular:

SigmaNLP proved to be able to translate the benchmark test sentences into a set of logical formulas.
NuXMV has proved capable of verifying the correctness of the property to be proved.


Development of two use cases

To test the system that will be designed and built.

The first use case should have involved the production of electronic chip components, involving the Nexperia company. Unfortunately, after some talks, Nexperia had to give up due to difficulties in allocating people to the project Partner Noldus is considering some alternative options.

The second use case concerns a control system for an artisanal ice cream production and sale activity. The use case concerns the management of the life cycle of the product, from its preparation to its marketing.


Development of a new tool

The third work package concerns the development of a tool resulting from the integration of the selected tools, i.e. SigmaNLP and NuXMV.
This work package is currently in progress.

    Contact us

    We'd like to hear from you

    For more information please do not hesitate to contact us!

    • Via Quarantadue Martiri n. 165
      28924 Verbania Fondotoce (VB) - Italy

    • +39 0323 586730


    Thank you!

    Your message has been send, we will contact you as soon as possible.