Tools

Verification of Neural Network with Geometric Perturbations
Acronym: SORA
License: BSD3
Status in FOCETA: New
Relevant WPs: WP3
Relevant UCs: UC1
Description: Sora is designed for the scalable blackbox reachability analysis of deep neural networks (DNNs). It verifies the reachability property of DNNs with a novel optimisation algorithm and has global convergence guarantee. It works with a broad class of neural network structures, including those networks with very deep layers and a huge number of neurons with nonlinear activation functions.

LiMP- Lightweight Monitoring for Perception
Acronym: LiMP
License: MIT license
Status in FOCETA: developed
Relevant WPs: WP4, WP5
Relevant UCs: UC1
Description: A Low-Cost Strategic Monitoring Approach for Scalable and Interpretable Error Detection in Deep Neural Networks:
This is a highly compact run-time monitoring approach for deep computer vision networks that extracts selected knowledge from only a few (down to merely two) hidden layers, yet can efficiently detect silent data corruption originating from both hardware memory and input faults. Building on the insight that critical faults typically manifest as peak or bulk shifts in the activation distribution of the affected network layers, we use strategically placed quantile markers to make accurate estimates about the anomaly of the current inference as a whole.
Compared to state-of-the-art anomaly detection techniques, this approach requires minimal compute overhead (as little as 0.3%
with respect to non-supervised inference time) and contributes to the explainability of the model.
(Details in https://doi.org/10.1007/978-3-031-40923-3_7 ).

Mining Temporal Hyperproperties
Acronym: HyTeM
License: MIT
Status in FOCETA: developed
Relevant WPs: WP2
Relevant UCs: UC1
Description: Tool for mining hyperproperties from data.

Mining Shape Expressions
Acronym: ShapeIt
License: MIT
Status in FOCETA: developed
Relevant WPs: WP2
Relevant UCs: UC2
Description: Tool for mining rich temporal patterns in the form of Shape Expression specifications.

NN Activation Pattern Monitoring
Acronym: NN-APM
License: n/a
Status in FOCETA: extended
Relevant WPs: WP4
Relevant UCs: UC1
Description: NN-APM constructs abstractions over neural network activation patterns from design-time and apply them during run-time to filter extreme cases. It also considers formal symbolic reasoning to provide robustness guarantees. It has been evaluated in a small-scale automotive application for waypoint prediction.

Abstraction-based Monitoring for Object Detection
Acronym: AMOD
License: n/a
Status in FOCETA: developed
Relevant WPs: WP4
Relevant UCs: UC1
Description: AMOD offers a framework to build spatial and temporal abstractions to monitor object detectors during run-time. It is used in UC1 to detect anomalous situations included image corruption and unknown objects.

Safe Object Detection
Acronym: SafeOD
License: n/a
Status in FOCETA: developed
Relevant WPs: WP3
Relevant UCs: UC1
Description: SafeOD evaluates and finetunes object detectors via spatial properties between the predictions and the labels. It is used in UC1 to improve the safety of object detection models.

Robustness Verification for Transformers
Acronym: RV-Transformer
License: n/a
Status in FOCETA: developed
Relevant WPs: WP3
Relevant UCs: UC1
Description: RV-Transformer proposes a method to find the maximum robustness of given Transformers (an emerging type of neural networks) by encoding them into Mixed Integer Programming optimization problems. It has been evaluated in a small-scale automotive application for lane departure warning.

Tempest – Synthesis Tool for Reactive Systems and Shields in Probabilistic Environments
Acronym: Tempest
License: GPL 3.0
Status in FOCETA: new
Relevant WPs: WP4, WP5
Relevant UCs: UC1
Description: Tempest is a synthesis tool to automatically create correct-by-construction reactive systems and shields from qualitative or quantitative specifications in probabilistic environments. It is used in UC1 as a collision avoidance enforcer, overwritting the path follower’s output when it could lead to collision with a pedestrian.

Pytorch application-level fault injection
Acronym: pytorchALFI
License: MIT license
Status in FOCETA: developed
Relevant WPs: WP6, WP4, WP5, WP3
Relevant UCs: UC1
Description: pytorchALFI is a tool to run efficient fault injection campaigns to simulate hardware faults (bit flips) in deep neural networks. So far, convolution and fully connected layers are supported for fault injection. We further provide evaluation examples for image classification and object detection scenarios.

Range supervision in OpenVino POT (Post Training Quantization with OpenVino Toolkit)
Acronym: Ranger
License: Apache License 2.0
Status in FOCETA: used; partially developed scientific foundation in FOCETA
Relevant WPs: WP6, WP4, WP5, WP3
Relevant UCs: UC1
Description: We have implemented an error detection and mitigation method for deep neural networks based on activation range supervision. This feature inserts protection layers at strategic points in the network which suppress large outlier values originating from underlying platform faults. The technique is based on the following original publication: https://arxiv.org/pdf/2003.13874.pdf.

Requirement Formalisation Tool
Acronym: RFT
License: GPL v3.0
Status in FOCETA: Developed
Relevant WPs: WP2, WP5
Relevant UCs: UC1 (could be applied in UC2 as well)
Description: RFT is a web-based tool that assists with the specification and formalization of system requirements. The specification is based on an ontology-driven approach that supports the semantic validation of a set of requirements and the formalization takes place through deriving logic-based specifications of monitorable properties, from the requirements. In the aspect of FOCETA it is used to (1) specify a set of requirements of the UC1 and validate through the semantic analysis, and (2) extract monitorable properties in the proposed first-order temporal logic language.

Neural Network Equivalence Checking Tool
Acronym: NNECT
License: GPL v3.0
Status in FOCETA: Developed
Relevant WPs: WP3
Relevant UCs: — (none yet, could be used in both)
Description: The tool can check if two neural networks are equivalent or approximate equivalent with respect to a given criterion. It is used in FOCETA as an oracle during neural network design and as a means for neural network abstraction and compression.

FMU Generator for BIP models
Acronym: —
License: GPL v3.0
Status in FOCETA: Developed
Relevant WPs: WP2, WP4, WP5
Relevant UCs: — (none yet, could be used in both)
Description: The tool can transform a BIP model into an FMU (standard version 2). It is used in FOCETA as a translator/generator for BIP and assists with interoperability.

A Runtime Verification Toolkit for Co-simulation
Acronym: RVcosim
License: GPL v3.0
Status in FOCETA: Developed
Relevant WPs: WP2, WP4, WP5
Relevant UCs: UC1 and UC2
Description: The RVcosim toolkit contains different runtime verification schemes and implementations for co-simulation; with an emphasis on master-slave architectures. It is used in FOCETA to support property evaluation tailored to component-based systems.

An open-source framework for the application of search-based testing for Automated and Autonomous Driving Systems
Acronym: OpenSBT
License: Apache 2.0
Status in FOCETA: created
Relevant WPs: WP3
Relevant UCs: UC1
Description: OpenSBT provides a modular and extandable code base for the application of search-based testing approaches for the safety assessment of AD/ADAS systems. It is used in FOCETA to apply an AI-driven search-based testing algorithm to identiy critical scenarios for the AVP system.

Simcenter Prescan – Virtual verification and validation of ADAS and autonomous vehicles
Acronym: Prescan
License: commercial
Status in FOCETA: used and extended
Relevant WPs: WP2, WP3 and WP5
Relevant UCs: UC1
Description: Prescan is a physics-based simulation platform which allows design, verification and validation of autonomous vehicles functionalities. It is used in FOCETA as one of the main simulation and testing engines, applied for safety validation of AVP use-case, with special focus on vulnerable road users.

Simcenter HEEDS – design space exploration and optimization software
Acronym: HEEDS
License: commercial
Status in FOCETA: used
Relevant WPs: WP5
Relevant UCs: UC1
Description: HEEDS is used for traffic scenario generation, including critical scenarios in UC1 of automated valet parking testing environment.

Simcenter Amesim – integrated, scalable mechatronic system simulation platform
Acronym: Amesim
License: commercial
Status in FOCETA: used and extended
Relevant WPs: WP2, WP4 and WP5
Relevant UCs: UC1, UC2
Description: Amesim is a system simulation platform that allows design engineers to virtually assess and optimize the systems’ performance. It is used in both use cases: UC1 for vehicle dynamics and UC2 for healthcare modeling and control development.

Extendible Probabilistic Model Checker
Acronym: EPMC
License: one of the free ones
Status in FOCETA: extended
Relevant WPs: WP3, WP4
Relevant UCs: UC1 and UC2 —
Description: It is a model checker, you can use e.g. wherever you can use PRISM.

Mungorerrie
Acronym: Mungojerrie
License: one of the free ones
Status in FOCETA: extended
Relevant WPs: WP3, WP4
Relevant UCs: UC1 or UC2 (I think)
Description: A tool for reinforcement learning of temporal / omega-regular properties and some related things.

PAVE360 Veloce System Interconnect
Acronym: PAVE360-VSI
License: Commercial
Status in FOCETA: Used (also, new components were developed with requirements coming from our partners)
Relevant WPs: WP2 and WP5
Relevant UCs: UC1, UC2
Description: The Veloce System Interconnect App is an optimized interconnect framework enabling heterogeneous clients connections in a PAVE360 ecosystem to create digital twins in area of automotive, avionics, robotics and medical.

Real-time analog monitoring tool
Acronym: RTAMT
License: BSD3
Status in FOCETA: extended
Relevant WPs: WP4 and WP5
Relevant UCs: UC1
Description: RTAMT is a runtime verification tool for quantitative monitoring of Signal Temporal Logic (STL) specifications. It is used in FOCETA as (1) an oracle during design, and (2) as the objective function for search-based testing.

Hyper-Temporal Miner
Acronym: HyTeM
License: BSD3
Status in FOCETA: new
Relevant WPs: WP2
Relevant UCs: UC1
Description: HyTeM is a tool for mining (hyper)-temporal specifications, supporting template-free and template-based mining of LTL, HyperLTL, STL and HyperSTL.

THREATGET – THREAT ANALYSIS AND RISK MANAGEMENT
Acronym: THREATGET
License: Commercial (free academic license)
Status in FOCETA: extended
Relevant WPs: WP2
Relevant UCs: UC1
Description: THREATGET is a tool for thread analysis and risk management. The tool was extended in FOCETA with the threat repair functionality.