Bit-Precise Conformance Testing of Simulink Model Checkers

• URL: http://arxiv.org/abs/2606.24719v2
• Date: Fri, 26 Jun 2026 06:31:15 GMT
• Title: Bit-Precise Conformance Testing of Simulink Model Checkers
• Abstract summary: Simulink provides a practical modeling language and a simulation engine for the development of cyber-physical systems.<n>There are formal verification tools available, such as Simulink Design Verifier (SLDV) and third-party SMT-based model checkers (SmtMC)<n>This work aims to verify the quality of the Simulink model checkers by addressing the following items.
• Score: 0.09332987715848712
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: MATLAB/Simulink provides a practical modeling language and a simulation engine for the development of cyber-physical systems. To ensure the quality of the developed models, there are formal verification tools available, such as Simulink Design Verifier (SLDV) and third-party SMT-based model checkers (SmtMC). However, due to the absence of a semantics of Simulink that covers every element of models and the details of its numerical behavior, the reliability of the model checkers themselves is often doubtful, potentially analyzing models differently from the simulator. This work aims to verify the quality of the Simulink model checkers by addressing the following items. 1) Formalization of the basic block types of Simulink. It involves defining block type feature sets and the bit-precise behavior of the blocks. 2) A method for testing bit-precise conformance relations among the tools for each block type. The pass rate of our test suite measures (i) conformance of model checking results with simulation results by Simulink and (ii) conformance between the results of SmtMC and SLDV. 3) Experiment to perform tests on 10 block types. We confirmed that SmtMC efficiently passed all test cases, while SLDV achieved pass rates of only 94-96% and 80-90% for conformance (i) and (ii), respectively. We analyzed the causes of failed tests, such as errors, corner cases, and timeouts.

Related papers

• CIAware-Bench: Benchmarking Control Intervention Awareness Across Frontier LLMs [100.38986535324284]
  We introduce textbfCIAware-Bench, a benchmark for measuring textbfcontrol textbfintervention (CI) awareness across frontier models.<n>CIAware-Bench tests whether models can distinguish their own trajectories from those modified by a control intervention.
  arXiv  Detail & Related papers  (2026-06-09T16:24:16Z)
• Multi-Agent Specification-based Metamorphic Testing of FMU-Based Simulations [1.58310730488265]
  In industrial domains, Functional Mock-up Interface (FMI) is used to exchange simulation models as Functional Mock-up Units (FMUs)<n> deriving effective test oracles for these simulation models remains challenging due to the absence of explicit expected outputs.<n>We propose an LLM-powered multi-agent workflow for specification-based metamorphic testing of FMU-based simulation models.
  arXiv  Detail & Related papers  (2026-05-24T14:30:56Z)
• Scalable Simulation-Based Model Inference with Test-Time Complexity Control [12.86778906492369]
  PRISM is a simulation-based encoder-decoder that infers a joint posterior over both discrete model structures.<n>We evaluate PRISM on biophysical modeling for diffusion MRI data, showing the ability to perform model selection across several multi-compartment models.
  arXiv  Detail & Related papers  (2026-03-16T13:54:15Z)
• Agentic Scientific Simulation: Execution-Grounded Model Construction and Reconstruction [0.0]
  This paper investigates agentic scientific simulation, where model construction is organized as an execution-grounded interpret-act-validate loop.<n>We present JutulGPT, a reference implementation built on the fully differentiable Julia-based reservoir simulator JutulDarcy.
  arXiv  Detail & Related papers  (2026-02-27T15:42:05Z)
• Every Step Counts: Decoding Trajectories as Authorship Fingerprints of dLLMs [63.82840470917859]
  We show that the decoding mechanism of dLLMs can be used as a powerful tool for model attribution.<n>We propose a novel information extraction scheme called the Directed Decoding Map (DDM), which captures structural relationships between decoding steps and better reveals model-specific behaviors.
  arXiv  Detail & Related papers  (2025-10-02T06:25:10Z)
• Independence Tests for Language Models [47.0749292650885]
  Given the weights of two models, can we test whether they were trained independently?<n>We consider two settings: constrained and unconstrained.<n>We propose a new test which matches hidden activations between two models, and which is robust to adversarial transformations and to changes in model architecture.
  arXiv  Detail & Related papers  (2025-02-17T20:01:08Z)
• SYNTHEVAL: Hybrid Behavioral Testing of NLP Models with Synthetic CheckLists [59.08999823652293]
  We propose SYNTHEVAL to generate a wide range of test types for a comprehensive evaluation of NLP models. In the last stage, human experts investigate the challenging examples, manually design templates, and identify the types of failures the taskspecific models consistently exhibit. We apply SYNTHEVAL to two classification tasks, sentiment analysis and toxic language detection, and show that our framework is effective in identifying weaknesses of strong models on these tasks.
  arXiv  Detail & Related papers  (2024-08-30T17:41:30Z)
• Type-level Property Based Testing [0.0]
  We present an automated framework for solidifying the cohesion between software specifications, their dependently typed models, and implementation at compile time. We are able to model several interesting systems and network protocols, have the type checker verify that our implementation behaves as specified, and test that our model matches the specification's semantics.
  arXiv  Detail & Related papers  (2024-07-17T16:43:41Z)
• A Comprehensive Evaluation and Analysis Study for Chinese Spelling Check [53.152011258252315]
  We show that using phonetic and graphic information reasonably is effective for Chinese Spelling Check. Models are sensitive to the error distribution of the test set, which reflects the shortcomings of models. The commonly used benchmark, SIGHAN, can not reliably evaluate models' performance.
  arXiv  Detail & Related papers  (2023-07-25T17:02:38Z)
• Benchmarking Model Predictive Control Algorithms in Building Optimization Testing Framework (BOPTEST) [40.17692290400862]
  We present a data-driven modeling and control framework for physics-based building emulators. Our approach consists of: (a) Offline training of differentiable surrogate models that accelerate model evaluations, provide cost-effective gradients, and maintain good predictive accuracy for the receding horizon in Model Predictive Control (MPC) We extensively evaluate the modeling and control performance using multiple surrogate models and optimization frameworks across various test cases available in the Building Optimization Testing Framework (BOPTEST)
  arXiv  Detail & Related papers  (2023-01-31T06:55:19Z)
• Learning continuous models for continuous physics [94.42705784823997]
  We develop a test based on numerical analysis theory to validate machine learning models for science and engineering applications. Our results illustrate how principled numerical analysis methods can be coupled with existing ML training/testing methodologies to validate models for science and engineering applications.
  arXiv  Detail & Related papers  (2022-02-17T07:56:46Z)
• Calibrating Over-Parametrized Simulation Models: A Framework via Eligibility Set [3.862247454265944]
  We develop a framework to develop calibration schemes that satisfy rigorous frequentist statistical guarantees. We demonstrate our methodology on several numerical examples, including an application to calibration of a limit order book market simulator.
  arXiv  Detail & Related papers  (2021-05-27T00:59:29Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.