Safety Verification and Optimization in Industrial Drive Systems

TL;DR

The paper tackles safety verification and fault-detection optimization in an industrial drive module (BDM) under stochastic faults. It builds a formal Timed Automata model of the BDM in Uppaal Stratego, verifies core functional and safety properties with CTL queries, and uses RL-based strategy synthesis to optimize the Safe Failure Fraction toward a 90% target, achieving 90.9% in experiments. A key result is that 290 faults are detected and 29 undetected under the RL-enhanced strategy, compared to 185 detected and 196 undetected without strategy, with the SFF defined as $SFF = \frac{\lambda_S + \lambda_{DD}}{\lambda_S + \lambda_{DD} + \lambda_{DU}}$. This integrated FV+RL workflow demonstrates practical potential for safety improvements in industrial automation and can be extended to energy efficiency and predictive maintenance, aided by techniques such as a controlled deadlock for verification during model reduction.

Abstract

Safety and reliability are crucial in industrial drive systems, where hazardous failures can have severe consequences. Detecting and mitigating dangerous faults on time is challenging due to the stochastic and unpredictable nature of fault occurrences, which can lead to limited diagnostic efficiency and compromise safety. This paper optimizes the safety and diagnostic performance of a real-world industrial Basic Drive Module(BDM) using Uppaal Stratego. We model the functional safety architecture of the BDM with timed automata and formally verify its key functional and safety requirements through model checking to eliminate unwanted behaviors. Considering the formally verified correct model as a baseline, we leverage the reinforcement learning facility in Uppaal Stratego to optimize the safe failure fraction to the 90 % threshold, improving fault detection ability. The promising results highlight strong potential for broader safety applications in industrial automation.

Figures (3)

• Figure 1: Overview of the functional safety architecture of the BDM
• Figure 2: Overview of the main blocks of the BDM modelled in Stratego
• Figure 3: Fault detection with and without a strategy