AIDA
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
FIRST PROJECT STEP
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
Usability
Which collects a set of considerations relating to the user interface, information feedback, flexibility, error management and user guide.
Effectiveness
Effectiveness, or degree of ability to carry out the task assigned.
Efficiency
Especially in terms of time spent solving certain tasks.
Robustness
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.
SECOND PROJECT STEP
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.
THIRD PROJECT STEP
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!