WP6-16

SAGE

ID	WP6-SAGE
Contributor	UNISS
Levels	Tool
TRL	3

Detailed Description

The tools in the SAGE Verification Suite (SAGE-VS) proposed by UNISS to address UC5 targets targets requirement consistency checking (ReqV), automatic test pattern generation (ReqT) and Neural Network verification (NeVer).

Contribution and Improvements

• ReqV:
  • Formulate the technical requirements/specification using Property Specification Patterns (PSP), manually or using the wizard offered by the tool.
  • Verify the consistency.
  • Examine the feedback returned by the tool in the case of inconsistencies.
• ReqT:
  • Load the technical requirements/specification (in PSP) and the code related to the System Under Test.
  • Generate the test suite.
• Never:
  • Design and train a DNN in pyTorch or load a DNN in ONNX format
  • Encode the property to verify
  • Launch the verification process

Current Status

MDC has been tested in the context of UC5-D1 to model the application that needs to be accelerated on an FPGA so as to meet real-time responses: an AES encryption/decryption block provided by RO Technologies. It has successfully achieved a performance improvement of 2x.

Example of use

In the following we present an example related to NeVer. From Scenario 5.1.3 described in D1.1, Uncle John, as a wise farmer, knows that it would be good to save also a bit of his own effort without losing money in hiring someone to do the treatments. Therefore, he buys a rover that under the lead of its master (the image acquisition drone) actuates the treatment as determined in the acquisition campaign. This improvement results into: a. The possibility of saving Uncle John precious time and effort. b. The possibility of promptly intervening on nutritional deficiencies, other disease or insect infestations to avoid their worsening/spreading. In this context, the acquisition/monitoring system should be able to recognize nutritional deficiencies or other diseases by processing input images and the correctness of the classification is of paramount importance. Considering a Deep Neural Network (DNN) trained to deal with the classification task, it is well-established the sensitivity to adversarial perturbations -- i.e., minimal changes to correctly classified input data that cause a network to respond in unexpected and incorrect ways – of this kind of technology, so the need for tools to analyse (and possibly repair) DNNs is strong.

Evaluation

The ReqV and ReqT tools have been evaluated in collaboration with Abinsula, that provided their internal templates for the Requirements Traceability Matrix and Validation Test, continuously providing support in identifying the requirements classifications and in the application of their internal procedures. The tools have been evaluated in the context of a real use case which is currently under production in Abinsula. The use case count almost two hundred requirements, related to customer requirements, applicable standards, hardware provided by the customer, and technical assumption. For NDA reasons details about the use case cannot be provided, however results demonstrated that the ReqV and ReqT are efficient in verifying the requirements consistency and generating the test suite, saving effort. This collaboration is going to be carried on further in the context of other AIDOaRt European Project, to develop procedures, based on the application of formal methods and AI/ML techniques, to enhance the automated verification of systems applied in real safety critical applications.