StabilEdge, Formal Verification of Edge AI Applications

This paper addresses the critical need for AI trustworthiness in smart IoT systems by focusing on the stability of Deep Neural Networks (DNNs) in Edge AI. State-of-the-art model checkers guarantee feasibility of a single stability analysis. However, a comprehensive assessment requires multiple runs, considering different noise levels and output targets. This is feasible in Edge AI applications, because of the limited size of the involved DNNs. However, direct user interaction with the model checker via its command-line interface is suboptimal, with a high potential for error and inefficiency. We address this issue by proposing a higher-level tool, namely StabilEdge, that abstracts and automatically manages the technical complexities of the underlying verification engine through a graphical layer. The goal is to help designers to concentrate on application-level logic and constraints, rather than the underlying mechanics of the verification tool. StabilEdge performs parametric stability analysis by modeling realistic input perturbations, such as sensor noise/attacks, to assess if they may cause dangerous mispredictions. StabilEdge operationalizes a novel methodology unifying four complementary Edge-AI stability analyses: local robustness, focused evaluation of specific input features (sensitivity) and output target adherence (targeted robustness and sensitivity). The tool generates three key graphical outputs: stability constraint violations, class transition patterns, and input-output constraint trade-offs. It provides continuous verification feedback and specialized support for time series and vision tasks. Overall, StabilEdge automates the full verification workflow - from perturbation modeling to formal constraint generation and solver-level monitoring -, with no need for expert manual configuration. Evaluations on three edge AI tasks demonstrate that StabilEdge quantifies noise impact on DNN performance at a fine granularity, greatly enhancing the depth of NN performance assessment. This analysis yields also key insights, such as the explicit trade-off between model accuracy and its vulnerability to localized perturbations. We thus argue that the tool fulfills its goal of supporting designers in rigorously specifying DNN stability and making informed decisions on sensor selection and overall system architecture. The current implementation exploits the Marabou model checker and may integrate other engines in the future, especially to address scalability issues due to input/output and model size. To support free research in the field, StabilEdge is released open source at: https://github.com/Elios-Lab/StabilEdge.