PaperlayerView exact revision on arXiv

Source-linked AI summary

Formal Specifications with Data-Driven Signal Analysis

Roderick Bloem, Benedikt Maderbacher, Cristinel Mateis, Dejan Ničković, Sergii Tkachov, Björn Ziegler

arXiv:2610.39007v1cs.AIcs.LG

TL;DR

Formal specifications can miss subtle analog-system anomalies that experts find difficult to characterize mathematically. SIGMA combines specification-guided signal analysis with data-driven anomaly detection, and its voltage-regulator evaluation reports detection of subtle stabilization anomalies and robustness under moderate distribution shifts.

  • Problem

    Formal specifications can miss subtle oscillations within nominal limits, which may affect long-term reliability and be difficult for experts to characterize mathematically.

    Source: §1 · p. 1

  • Method

    SIGMA uses SIGMA-Spec to localize relevant signal segments and extract features for machine-learning anomaly detection.

    Source: §1 · pp. 1–2

  • Results

    SIGMA detected subtle voltage-regulator stabilization anomalies difficult to characterize symbolically and was robust under moderate distribution shifts, including transfer across regulator designs.

    Source: §6 · p. 12

  • Takeaways & Limitations

    SIGMA is presented as a framework combining formal signal analysis and data-driven anomaly detection for CPS monitoring workflows.

    Source: §6 · pp. 11–12

    The evaluation covers a single industrial voltage-regulator case study, so generalizability to other analog or mixed-signal systems remains to be demonstrated.

    Source: §5.8 · p. 11

Abstract

from arXiv · show

Developing analog and hybrid systems requires substantial domain knowledge that is hard to articulate in a formal specification; without additional effort, this domain knowledge is also inaccessible to machine learning methods. We propose a hybrid approach for analyzing and monitoring real-valued signals that integrates specification-based and data-driven techniques. We use regular expressions with interval operations to identify regions of interest in a signal, classical signal processing methods to extract semantically meaningful features, and semi-supervised machine learning to infer complex relationships that distinguish correct from faulty behaviors. The relationships learned from normal behavior data can automatically detect incorrect behavior in the same system or variants thereof. We evaluate the method on a voltage regulator, demonstrating its effectiveness in detecting undesired system behaviors.

1 Introduction

Analog and hybrid systems combine discrete-event logic with continuous-time dynamics, making correctness difficult to ensure at scale. SIGMA integrates formal signal specifications with data-driven anomaly detection, using specification-derived features and demonstrating the approach on a voltage regulator.

1 Introduction

  • Formal specifications can miss subtle oscillations that remain within nominal limits but may affect long-term reliability and resist precise mathematical characterization.Experts may distinguish benign from harmful oscillations visually while struggling to formalize them.Source: §1 · p. 1
  • SIGMA combines formal specifications with data-driven anomaly detection, using SIGMA-Spec to identify relevant signal segments and extract meaningful features for machine learning.This combines explicit domain knowledge encoded in behavioral patterns with implicit knowledge learned from data.Source: §1 · pp. 1–2
  • A prototype implementation demonstrates the approach on a voltage regulator case study.Source: §1 · p. 2

2 Related Work

Related work includes formal trace specifications, machine-learning anomaly detection, specification learning, and quantitative logic. SIGMA's distinction is to localize semantically relevant intervals before extracting signal features and applying learned classification.

2 Related Work

  • Ferrere et al. use regular expressions with expressive signal measures, while signal logics such as STL specify constraints on signal values [7, 12].Source: §2 · p. 2
  • SIGMA combines symbolic localization of meaningful intervals with signal-processing features and machine learning, rather than requiring correctness to be specified explicitly.Finite, potentially irregularly sampled runtime traces allow standard regular-expression matching instead of expensive zone-based algorithms.Source: §2 · p. 2
  • Matrix Profile methods mine recurring or unusual patterns from raw time series, whereas SIGMA-Spec first localizes semantically relevant intervals such as stabilization regimes.Source: §2 · p. 2
  • Many signal-anomaly methods use machine learning without logical representations, leaving domain knowledge to be incorporated ad hoc.Source: §2 · p. 2
  • Kong et al. learn parameterized specification formulas and values that distinguish good traces from bad ones.Source: §2 · p. 2
  • Quantitative-logic approaches focus on robustness semantics; SIGMA instead handles robustness through machine-learning confidence estimates.Source: §2 · p. 2

3 SIGMA-Spec Specification Language

SIGMA-Spec is a stream-processing language that combines regular-expression interval matching with interval processing, feature extraction, learned scoring, and aggregation.

3.1 Language

  • SIGMA-Spec processes traces through timed-regular-expression interval extraction, interval adjustment, feature extraction, machine-learning robustness scoring, and trace-level aggregation.Source: §3.1 · pp. 2–3

3.2 Interval Recognition

  • Timed regular expressions match signal predicates and events over time to extract intervals, with syntax including intersection and time-restriction operators.Source: §3.2 · p. 3

3.3 Interval Adjustment

  • Interval-adjustment operators modify matched intervals; linefit partitions an interval into l segments and returns a selected segment of its best-fit piecewise-linear approximation.Source: §3.3 · p. 4

3.4 Feature Extraction

  • Feature extraction spans direct statistics, linear-fit and spectral descriptors, and symbolic anomaly predicates; irregularly sampled traces use linear approximation for difficult features.Source: §3.4 · p. 4

3.5 ML-based Anomaly Scoring Functions

  • Externally trained anomaly detectors score interval feature valuations, and those scores can serve as features in subsequent interval conditions, including threshold comparisons.Source: §3.5 · pp. 4–5

3.6 Aggregation of Interval Streams

  • Aggregators combine interval features using maxima, minima, addition, and subtraction; trace anomaly scores can rank traces or support threshold-based classification to focus manual inspection.Source: §3.6 · p. 5

3.7 Example

  • The oscillator example selects rise/fall-delimited s > 0.3 intervals, keeps matches two and three, takes each interval’s final 30%, and aggregates the slope range.Figure 2 applies the specification to four oscillator simulations, showing the signal, event markers, retained intervals, and slope fits.Source: §3.7 · p. 5

4 ML-based Predicates in SIGMA-Spec

SIGMA-Spec localizes signal segments and computes measurements, while a learned predicate judges whether their feature vectors match nominal behavior. The paper uses a semi-supervised one-class setting because faults are scarce and expensive to label.

Motivation and learning setting

  • Sustained oscillations and abnormal stabilization patterns can be easier for experts to label from examples than to characterize completely with symbolic predicates.The approach uses normal samples to fit the predicate; anomalous samples are reserved for feature selection and evaluation.Source: §4 · pp. 5–6

Learned interval predicates

  • SIGMA-Spec determines where to look and which measurements to compute; the learned predicate assesses whether the resulting feature vector is consistent with nominal behavior.The predicate is based on an anomaly-scoring function and threshold.Source: §4 · p. 5

Learning algorithms

  • The evaluation instantiates learned predicates with autoencoders and One-Class SVMs, comparing models on the same SIGMA-Spec-derived feature vectors.This comparison concerns the learned-predicate model, not the shared localization and feature-extraction stages.Source: §4 · p. 6

5 Evaluation

The evaluation uses a voltage-regulator case study to examine anomaly detection in stabilization behavior, which is difficult to formalize despite the availability of symbolic analysis for transients and overshoots. It asks about in-domain accuracy, generalization, learned versus symbolic predicates, and sensitivity to the learning algorithm.

5.1 Case Study: Voltage Regulator

  • The case study observes sampled output voltage in behavioral and transistor-level regulator designs through simulation, with input-voltage or load-current perturbations.It targets sustained oscillations, excessive residual periodicity, and abnormal noise after the transient.Source: §5.1 · pp. 6–7

5.2 Research Questions

  • The evaluation asks whether SIGMA detects anomalies in-domain, generalizes across trace and model variants, improves on symbolic predicates, and depends on the chosen learning algorithm.The transfer settings include multi-parameter traces, changed parameters, and a transistor-level implementation.Source: §5.2 · p. 7

5.3 Experimental Setup

The setup combines behavioral-model traces for training with more costly transistor-level traces for evaluation, then extracts and expert-validates stabilization intervals and their features. Parameter sweeps and transfer datasets support the study’s in-domain and generalization questions.

Trace generation

  • The experiments vary internal design, operating, stimulus, and reference-voltage parameters to represent deteriorated behavior and different input-voltage or load-current perturbations.Single-parameter sweeps vary one parameter up to ±50% in 5% steps, while additional traces randomly sample multiple parameters.Source: Voltage Regulator Models · p. 7

Simulation environments

  • Transistor-level simulations provide more physically representative behavior but are substantially more expensive, so they are used for evaluation rather than training.InfineonSpice behavioral modeling provides inexpensive trace generation for training monitors.Source: Voltage Regulator Models · p. 7

Stabilization extraction

  • SIGMA-Spec segments perturbations, fits each output-voltage interval with three linear segments, and uses the third to represent stabilization; extraction can fail if stabilization is absent or the fit retains transient behavior.Features from valid segments include fit error, slope, offset, spectral energy, spectral flatness, and periodicity.Source: Stabilization Specification and Labeling · p. 8, Figure 4 · p. 8, Figure 5 · p. 8

Labeling and dataset preparation

Learned-predicate setup

5.4 RQ1: In-Domain Accuracy

Both retained autoencoder configurations achieve balanced in-domain performance, and the compact set uses half as many features with less than a one-percentage-point accuracy loss.

In-domain accuracy

  • F1 scores are around 0.87–0.88 for both classes across the two retained autoencoder configurations in-domain.The compact feature set loses less than one percentage point in accuracy while using half as many features.Source: §5.4 · p. 9

5.5 RQ2: Generalization Analysis

SIGMA predicates transfer reasonably to multi-parameter traces of the same design and to the nearby 3.3 V design, but large design and simulator shifts require calibration.

5.5 RQ2: Generalization Analysis

  • The G1–G3 evaluations use the same trained models and thresholds, with no retraining or target-domain calibration.The comparison therefore evaluates transfer without adapting models to the target domain.Source: §5.5 · p. 9
  • On G1, both autoencoder models degrade from the in-domain test, especially on anomalies, but AE-C substantially outperforms AE-R1.Training uses 5.0 V single-parameter sweeps; G1 tests 5.0 V traces with multiple parameters varying simultaneously.Source: §5.5 · p. 9
  • On the 3.3 V InfineonSpice design, AE-C performs best; on the 1.5 V design, both models perform poorly as normal-class F1 collapses.The text attributes the 1.5 V result to a substantial shift in normal stabilization behavior not compensated by current normalization and features.Source: §5.5 · p. 10
  • Transfer from InfineonSpice to transistor-level simulation is the most challenging setting because normal stabilization features shift enough to leave models poorly calibrated.The passage identifies threshold recalibration with a small set of transistor-level normal samples or feature-distribution alignment as possible responses.Source: §5.5 · p. 10
  • Transfer is mixed: learned predicates handle same-design multi-parameter traces and the nearby 3.3 V design reasonably, while large design and simulator shifts require calibration.The evaluation applies the same trained models and thresholds without retraining or target-domain calibration.Source: §5.5 · p. 10

5.6 RQ3: Symbolic-only Predicate

The symbolic-only predicate misses most anomalous intervals, while learned predicates perform better in this setting. Among learned predicates, OCSVM is competitive in-domain, but does not remove the effects of distribution shift.

5.6 RQ3: Symbolic-only Predicate

  • 14 of 48 anomalous intervals are detected by the symbolic baseline, supporting the reported advantage of learned predicates over this threshold-based approach.Table 4 covers the symbolic-only baseline on the 5.0 V behavioral model.Source: §5.6 · p. 10

5.7 RQ4: Robustness to ML Methods

  • The OCSVM comparison keeps SIGMA-Spec interval detection, stabilization localization, feature extraction, data splits, and normalization fixed while varying the learned predicate.Controlled OCSVM variants retain the AE-R1 and AE-C feature sets; OCSVM-B uses a subset selected by nested cross-validation.Source: §5.7 · p. 10
  • The compact AE and best OCSVM feature sets both select slope, spectral centroid, and band energy, but differ in their fourth feature.AE selects stabilization offset; OCSVM selects FFT peak-to-mean ratio.Source: §5.7 · p. 11
  • In-domain, OCSVM with its selected four-feature subset achieves the best accuracy and F1 scores, but it does not systematically improve generalization.The comparison includes the in-domain test and all three transfer scenarios; in-domain results alone would suggest OCSVM is preferable.Source: §5.7 · pp. 10–11, Table 5 · p. 11
  • AE-C is strongest on G1 in accuracy and normal-class F1, best on all reported metrics for the 3.3 V G2 design, and most effective at preserving normal-class behavior in G3.All models perform poorly on the 1.5 V design, which the passage attributes to domain shift rather than the choice between AE and OCSVM.Source: §5.7 · p. 11

5.8 Threats to Validity

The evaluation has limitations related to labels and feature selection, stabilization-interval extraction, case-study scope, and small expert-labeled test sets.

5.8 Threats to Validity

  • Expert-provided labels may introduce labeling noise, and using labeled anomalies to rank feature subsets may bias selection toward observed anomaly types.The one-class models are trained exclusively on normal samples; future work could select features using only normal samples or expert-defined criteria.Source: §5.8 · p. 11
  • The approach assumes SIGMA-Spec can identify stabilization intervals, but some candidate intervals are discarded when piecewise-linearization fails to find a valid regime.The evaluation may therefore miss behaviors outside the segmentation operator’s assumptions.Source: §5.8 · p. 11
  • The empirical evaluation is limited to one industrial voltage-regulator case study, so generalizability to other analog or mixed-signal systems remains un demonstrated.The passage also notes that domain shifts can degrade detection and practical deployment may require target-domain calibration.Source: §5.8 · p. 11
  • Several evaluations, especially out-of-domain experiments, use relatively small expert-labeled test sets, so results are indicative trends rather than statistically definitive estimates.This caveat is particularly relevant to anomaly detection because only a limited number of anomalous traces are available.Source: §5.8 · p. 11

6 Conclusion and Future Work

SIGMA combines formal signal analysis and data-driven anomaly detection for analog and hybrid systems. The voltage-regulator case study demonstrates detection of subtle stabilization anomalies, while the framework and its measurement operators remain open to extension.

6 Conclusion and Future Work

  • SIGMA combines formal signal analysis with data-driven anomaly detection for analog and hybrid systems.The paper presents this combination as showing synergies between formal methods and machine learning for CPS monitoring workflows.Source: §6 · p. 11
  • In an industrial voltage-regulator case study, SIGMA detects subtle stabilization anomalies that are difficult to characterize using purely symbolic specifications.The experiments report robustness under moderate distribution shifts and no dependence on a particular learning architecture.Source: §6 · p. 12
  • The framework could address systematic shifts between learning and evaluation domains, improve its measurement-operator set, and be integrated into a verification loop that selects simulation parameters.The paper presents the work as a framework rather than a definitive set of measurement operators.Source: §6 · p. 12

Related papers

Loading 2610.39007v1…