Software Engineering
Researchers Test Model Checkers for MATLAB Simulink, Find Gaps in Formal Verification Tools
A new conformance testing approach reveals that MATLAB's own Simulink Design Verifier falls short of the simulator's behavior, while third-party model checkers perform more reliably.
Researchers have developed a systematic method to test whether formal verification tools for MATLAB/Simulink accurately match the behavior of the simulator itself—and their findings expose concerning reliability gaps in one of the industry's most widely used verification tools.
The Problem: Unverified Verification Tools#
Cyber-physical systems modeled in MATLAB/Simulink rely on formal verification tools to catch design errors before deployment. However, these verification tools operate without a complete, formally defined semantics for Simulink's numerical behavior and feature set. This mismatch raises a critical question: are the verification tools themselves analyzing models correctly, or might they produce results that diverge from what the actual simulator would do?
The gap in semantic definition has left practitioners uncertain about the trustworthiness of tools like Simulink Design Verifier (SLDV) and third-party SMT-based model checkers (SmtMC).
Testing Approach: Bit-Precise Conformance#
The research team addressed this by establishing a three-part framework:
- Formalizing the bit-level behavior of ten basic Simulink block types
- Developing a test methodology to measure conformance between simulators and model checkers
- Running experiments comparing how these tools handle the same models
The tests measure two kinds of conformance: whether model checker results align with Simulink's simulation output, and whether different model checkers agree with each other.
Results: SLDV Underperforms#
The findings were mixed. SmtMC passed all test cases across the block types examined. By contrast, SLDV achieved pass rates of only 94–96% when conforming to Simulink simulation results and dropped to 80–90% when compared against SmtMC.
The researchers identified the root causes of failures as numerical errors, handling of corner cases, and computation timeouts—suggesting that SLDV's implementation diverges from the simulator's actual behavior in subtle but measurable ways.