論文の概要: Bit-Precise Conformance Testing of Simulink Model Checkers
- arxiv url: http://arxiv.org/abs/2606.24719v1
- Date: Tue, 23 Jun 2026 15:40:49 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-06-24 22:16:49.041899
- Title: Bit-Precise Conformance Testing of Simulink Model Checkers
- Title（参考訳）: シンクリンクモデルチェッカーのビット精度整合性試験
- Authors: Daisuke Ishii, Takashi Tomita, Toshiaki Aoki, Hideaki Takai,
- Abstract要約: Simulinkは、実用的なモデリング言語と、サイバー物理システムの開発のためのシミュレーションエンジンを提供する。
Simulink Design Verifier (SLDV) やサードパーティのSMTベースのモデルチェッカー (SmtMC) など、正式な検証ツールが提供されている。
本研究の目的は、以下の項目に対処することで、Simulinkモデルチェッカーの品質を検証することである。
- 参考スコア（独自算出の注目度）: 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 suites 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.
- Abstract（参考訳）: MATLAB/Simulinkは、実用的なモデリング言語と、サイバー物理システムの開発のためのシミュレーションエンジンを提供する。
開発モデルの品質を保証するため、Simulink Design Verifier (SLDV) やサードパーティのSMTベースのモデルチェッカー (SmtMC) など、正式な検証ツールが提供されている。
しかし、モデルのすべての要素を網羅するSimulinkのセマンティクスが存在しないことと、その数値的な振る舞いの詳細のため、モデルチェッカー自体の信頼性は疑わしいことが多く、シミュレータと異なるモデルを分析する可能性がある。
本研究の目的は、以下の項目に対処することで、Simulinkモデルチェッカーの品質を検証することである。
1) Simulinkの基本ブロック型の形式化。
ブロックタイプの特徴セットとブロックのビット精度動作を定義する。
2) 各ブロックタイプのツール間のビット精度適合関係をテストする方法。
テストスイートの合格率
一 シミュリンクによるシミュレーション結果とモデル検査結果の適合性
(II)SmtMCの結果とSLDVの適合性について検討した。
3) 10ブロックタイプでテストを実行する実験。
SmtMCは全テストケースを効率よく通過し, SLDVは94-96%, 80-90%の通過率を示した。
(i)および
(i) であった。
エラー、コーナーケース、タイムアウトなどのテスト失敗の原因を分析した。
関連論文リスト
- CIAware-Bench: Benchmarking Control Intervention Awareness Across Frontier LLMs [100.38986535324284]
我々は、フロンティアモデル全体でのtextbfcontrol textbfintervention (CI) の認識を測定するベンチマークである textbfCIAware-Bench を紹介する。
CIAware-Benchは、モデルが自身の軌跡を制御介入によって修正されたものと区別できるかどうかをテストする。
論文 参考訳（メタデータ） (2026-06-09T16:24:16Z) - Multi-Agent Specification-based Metamorphic Testing of FMU-Based Simulations [1.58310730488265]
産業領域では、FMI(Functional Mock-up Interface)はシミュレーションモデルをFMU(Functional Mock-up Units)として交換するために使用される。
これらのシミュレーションモデルに有効なオーラクルを導出することは、明確な期待出力がないため、依然として困難である。
本稿では,FMUに基づくシミュレーションモデルの仕様ベースメタモルフィックテストのためのLLMを用いたマルチエージェントワークフローを提案する。
論文 参考訳（メタデータ） (2026-05-24T14:30:56Z) - Scalable Simulation-Based Model Inference with Test-Time Complexity Control [12.86778906492369]
PRISMはシミュレーションベースのエンコーダデコーダであり、両方の離散モデル構造に対して結合後部を推論する。
拡散MRIデータに対する生体物理モデリングにおけるPRISMの評価を行い、複数のマルチコンパートメントモデル間でモデル選択を行う能力を示す。
論文 参考訳（メタデータ） (2026-03-16T13:54:15Z) - Agentic Scientific Simulation: Execution-Grounded Model Construction and Reconstruction [0.0]
そこで本研究では,モデル構築をインタプリタ-アクト-バリデートループとして構成するエージェント科学シミュレーションについて検討する。
完全に微分可能なJuliaベースの貯水池シミュレータJutulDarcyをベースとした参照実装JutulGPTを提案する。
論文 参考訳（メタデータ） (2026-02-27T15:42:05Z) - Every Step Counts: Decoding Trajectories as Authorship Fingerprints of dLLMs [63.82840470917859]
本稿では,dLLMの復号化機構をモデル属性の強力なツールとして利用できることを示す。
本稿では、デコードステップ間の構造的関係を捉え、モデル固有の振る舞いをよりよく明らかにする、DDM(Directed Decoding Map)と呼ばれる新しい情報抽出手法を提案する。
論文 参考訳（メタデータ） (2025-10-02T06:25:10Z) - Independence Tests for Language Models [47.0749292650885]
2つのモデルの重みを考えると、独立してトレーニングされたかどうかテストできますか?
制約付きと制約なしの2つの設定を検討します。
本稿では,2つのモデル間の隠れアクティベーションに一致し,逆変換やモデルアーキテクチャの変更に対して堅牢な新しいテストを提案する。
論文 参考訳（メタデータ） (2025-02-17T20:01:08Z) - Type-level Property Based Testing [0.0]
本稿では,ソフトウェア仕様と依存型付けモデル,コンパイル時の実装の結合を統一する自動フレームワークを提案する。
いくつかの興味深いシステムやネットワークプロトコルをモデル化し、型チェッカーで実装が指定された動作であることを検証し、モデルが仕様のセマンティクスにマッチしていることをテストすることができます。
論文 参考訳（メタデータ） (2024-07-17T16:43:41Z) - A Comprehensive Evaluation and Analysis Study for Chinese Spelling Check [53.152011258252315]
音声とグラフィックの情報を合理的に使用することは,中国語のスペルチェックに有効であることを示す。
モデルはテストセットのエラー分布に敏感であり、モデルの欠点を反映している。
一般的なベンチマークであるSIGHANは、モデルの性能を確実に評価できない。
論文 参考訳（メタデータ） (2023-07-25T17:02:38Z) - Benchmarking Model Predictive Control Algorithms in Building Optimization Testing Framework (BOPTEST) [40.17692290400862]
物理に基づく建築エミュレータのためのデータ駆動モデリングおよび制御フレームワークを提案する。
a)モデル評価を加速し、コスト効率の良い勾配を提供し、モデル予測制御(MPC)における後退地平線に対する良好な予測精度を維持する、微分可能な代理モデルのオフライントレーニング。
ビルディング最適化テストフレームワーク(BOPTEST)で利用可能な様々なテストケースに対して、複数のサロゲートモデルと最適化フレームワークを用いて、モデリングと制御性能を広範囲に評価する。
論文 参考訳（メタデータ） (2023-01-31T06:55:19Z) - Calibrating Over-Parametrized Simulation Models: A Framework via
Eligibility Set [3.862247454265944]
厳密な頻繁な統計的保証を満たす校正手法を開発するための枠組みを開発する。
本手法は,書籍市場シミュレータのキャリブレーションへの応用を含む,いくつかの数値例で実証する。
論文 参考訳（メタデータ） (2021-05-27T00:59:29Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。