arXiv CSopen access

Bit-Precise Conformance Testing of Simulink Model Checkers

Bit-Precise Conformance Testing of Simulink Model Checkers Daisuke Ishii1,∗ , Takashi Tomita1 , Toshiaki Aoki1 , and Hideaki Takai2

arXiv:2606.24719v1 [cs.SE] 23 Jun 2026

1

Japan Advanced Institute of Advanced Science, Ishikawa, Japan 2 GAIO Technology Co. Ltd., Tokyo, Japan {dsksh,tomita,toshiaki}@jaist.ac.jp, [email protected] *corresponding author

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. Keywords–MATLAB/Simulink; Conformance testing; Model checking; SMT solver; Numerical computation 1. Introduction An efficient development method for cyber-physical systems (CPSs) [1] is to mimic real-world systems using models constructed from blocks and deepen understanding through simulation and analysis. MATLAB/Simulink (Sect. 2) provides a language for describing models as block diagrams and a toolchain including a numerical simulator and additional toolboxes. For the quality assurance of safety-critical Simulink models, as demanded by standards such as ISO 26262 for automotive and DO-178C for aircraft domain [2], the Simulink Design Verifier toolbox (SLDV) provides a model checking (MC) function (Sect. 2-B). Namely, it analyzes the contents of models in a formal manner and determines whether certain properties are satisfied. Third-party tools are also available to supplement the functions and perfor-

mance of the standard tools. For example, numerous MC methods and tools using SMT solvers have been proposed, e.g., [3]–[6]. An important detail in Simulink MC is analyzing numerically interpreted models at bit-level precision (Sect. 2-A). Although models are mathematically hybrid systems of continuous and discrete behaviors, Simulink simulates them based on machine-representable numbers (e.g. double and int8) and discrete steps. SLDV interprets models in the same way, meaning that the results of MC are expected to match those of the simulation. However, third-party methods often interpret them as idealized mathematical models. While many formalization and MC methods have been proposed, research considering bitprecise behavior is scarce (Sect. 7-C). Although the quality of the tools is important (Sect. 7-B), Simulink and its toolchain have issues that come with their proprietary nature. First, the documentation and semantics of the Simulink language are available (Sect. 7-A), but the corner cases and bit-precise semantics are often unclear. Simulink blocks have many parameters for each block type and it results in a wide variety of instances; it is difficult to comprehensively describe how each instance operates in each step. Second, there is a room for improvement in the reliability of official tools (SLDV is the target of our test). As stated in the release notes, bugs that may lead to incorrect results have been fixed in almost every version. When we try using SLDV, it is not uncommon to encounter errors or “undecided” outputs. In addition, SLDV has scalability issues to analyze large models. Finally, when third-party tools are used in a development (we also target an SMT-based tool), it becomes difficult to check and qualify the conformance of the tools to the semantics and the behavior of Simulink models. Although most methods have been verified for correctness through their formalization in technical documents and through testing of their implementations, it is common practice to check the detailed conformance by comparing the results with the Simulink simulator. In this work, we aim to formalize the Simulink language and clarify the conformance degree of the Simulink MC tools, i.e., SLDV and an SMT-based model checker (SmtMC) [5]. In particular, we examine the underlying numerical computations at the bit level and carry out precise formalization and testing. Our contributions are summarized as follows.

MCs

SmtMC

Simulink

SLDV

SL

+ 1

Figure 1. Tested conformance relations among tools.

Inport

+ Gain

3) Experimental results (Sect. 4 and Sect. 5). Our experimental results provided the tools with new quantitative evaluation metrics, i.e., the degree of bit-precise conformance (RQ1). Regarding confSL , we confirmed that SmtMC passed all test cases; SLDV failed to achieve an all-pass result, with average pass rates of 94% and 96% for version R2020b and R2025b, respectively. Regarding confMCs , the average pass rates when comparing SmtMC with SLDV are 80% and 90% for R2020b and R2025b, respectively. Notably, while SmtMC was able to process all TCs efficiently on average, a few percent of SLDV tests resulted in timeouts or errors. Accordingly, we analyzed the results to clarify the criteria for model instances supported by the tools (RQ2), and identified sets of TCs that produce incorrect results, TCs that cause errors, and TCs that take a long time; this thorough analysis ruled out many bugs in SmtMC. In addition, we compared the execution times when processing concrete TCs and abstract TCs with SmtMC and SLDV (RQ3); as a result,

>0

Z-1

1 Outport

Sum

Delay Switch

1) Formalization of basic Simulink block types. We specify a subset of the Simulink language through two efforts: First, we extract block type feature models (Sect. 3-B) from the official documentation for 10 block types. Second, we describe the bit-precise operational semantics of blocks as an extended SmtMC encoder (Sect. 2-B) that encodes blocks into predicate logic formulas. It replicates Simulink’s interpretation by describing the behavior of each block with logic formulas involving machinerepresentable integers and real numbers, represented by bit vectors. 2) A bit-precise testing method for checking the conformance among Simulink, SmtMC and SLDV (Sect. 3). We define confSL to ensure that SmtMC and SLDV interpret Simulink models in exactly the same way as the Simulink simulator does, and confMCs to ensure the conformance of the MC functionality, as shown in Fig. 1. To verify confSL and confMCs , we propose a combinatorial testing method using the Simulink simulator as oracle to make bit-precise comparison of the results (we also use SmtMC as oracle for confMCs ). It assumes a subset of block type instances and a subset of input signals, generates test cases (TCs) covering the subsets in a pairwise combinatorial manner, and checks each TC does not violate the conformance; as a result, it outputs the percentage of passed TCs in the test suite. Our method systematically tests the correctness and performance of model-based development tools based on detailed comparison among them. We are not aware of many other examples of tool evaluation that can inspect this level of precision.

Constant

(a) A model diagram.

Inport Outport

(b) An execution. Figure 2. Example Simulink model.

SmtMC was fast in most cases, but SLDV was faster in cases where the Product block contained uncertainty. 2. Simulink Simulink1 is a popular MATLAB toolbox for the modelbased design and prototyping of CPSs. It provides a graphical modeling language to describe dynamical systems that consist of interacting blocks and subsystems, and a numerical simulator that computes model behaviors on discrete steps, which correspond to either fixed or variable sample time. Simulink models are diagrams structured as hierarchical directed graphs with lines (edges) and blocks (vertices). Each component of models, i.e., blocks and user-defined models (subsystems), represents a function that maps between sets of input and output signals, and behaves as reactive systems interacting in a synchronous manner. An example Simulink model is shown in Fig. 2a, which describes an accumulator for input values that may be reset if a condition is met. The counter is described by a feedback loop that consists of block instances of types Inport, Gain, Sum, Constant, Switch, Delay, and Outport. Each block type has parameters such as Value setting the output value −1 of Constant, Inputs setting the number of arguments 2 of Sum, and InitialCondition setting the initial output value 0 of Delay. We can interpret Simulink models as transition systems. Definition 1: Let I, O and S be input, output, and state variables. For a (vector-valued) variable V = (v1 , . . . , vn ), we denote its domain D1 ×· · ·×Dn by D(V ). A transition system (I, O, S, I, T ) consists of an initial condition I ⊆ D(S) and a transition relation T ⊆ D(S)×D(S)×D(I)× D(O). Variables are typed as double (double-precision floatingpoint (FP) numbers), int32 (32-bit signed integers), string, 1 https://www.mathworks.com/products/simulink.html

etc. Not only do they represent scalar values, they can also have a composite type such as vectors of n values, m × n matrices, higher-dimension arrays and buses. For example, the model in Fig. 2 is interpreted with variables i1 and o1 , representing the input and output values of the Inport and Outport blocks, and s1 , representing the next output values of Delay. Let e be the expression 0.1i1 + s1 . Then, the initial condition is I :↔ (s1 = 0) and the transition relation is T :↔ (o1 = if e > 0 then −1 else e ∧ s′1 = o1 ) where s′1 represents the next state. Each variable are typed as double, etc. (it can also be typed as a composite). We assume M is deterministic, i.e. T (s1 , i1 , o1 , s′1 ) represents a map from any value (s1 , i1 ) to a single value (o1 , s′1 ). For a variable V , we call a finite sequence β(0) · · · β(k − 1) of k values in the domain D(V ) a signal and denote it by β [k] ∈ D(V )k . Numerical simulation using the Simulink tool computes the output signals of models, given input signals. They are formalized as executions of transition systems. Definition 2: Assume a model M = (I, O, S, I, T ) and an input signal ι[k] ∈ D(I)k . Let σ [k+1] and o[k] be signals in D(S)k+1 and D(O)k , respectively. Then, an execution is ι(0)/o(0)

ι(k−1)/o(k−1)

σ(0) −−−−−−→ σ(1) · · · σ(k−1) −−−−−−−−−→ σ(k), where I(σ(0)) holds and T (σ(j), ι(j), o(j), σ(j + 1)) holds for every j ∈ {0, . . . , k −1}. We denote the output signal o[k] by [[M ]](ι[k] ). Input and output signals of the example model are shown in Fig. 2b. When actually simulating with Simulink, we need to specify the input signal using a harness outside the description of Fig. 2a. In this work, we assume a fixed sample time. The transitions described above are based on discrete steps, each of which corresponds to the step time, and signals can be regarded as functions of time; in Fig. 2b, step time is set as 0.1. 2.1 Product Block Type and its Bit-Precise Semantics This work addresses the detailed semantics of basic block types. Here, we explain one of them, Product. Its block instance has one or more variable input ports i1 ,…, in and one output port o1 , and represents a multiplication of the input signal values. Depending on the values of the Inputs parameter, an instance takes various shapes as shown in Fig. 3. The operation changes depending on whether the inputs are composite (e.g. vector) signals or not (it is also depending on parameters Multiplication and CollapseMode, but we assume default settings i.e. Element-Wise and All dimensions). The instances in the figure represents o1 = i1 × i2 (Fig. 3a), o1,j = (1 ÷ i1 ) ÷ i2,j for 1 ≤ j ≤ 3 (Fig. 3b), and o1 = (i1,1 ×i1,2 )×i1,3 (Fig. 3c). By default, Simulink handles signal values as double type, and 64-bit FP arithmetic is performed, following the IEEE-754 standard [7]. The result of each arithmetic operation is rounded to a representable FP number according to the specified mode. Special values e.g. +∞ and NaN are

÷

x

÷

(c) “1” or “*” (a) “2” or “**”

(b) “//”

Figure 3. Instances of Product corresponding to the values of Inputs.

TABLE I int8 operation examples of Product. Inputs “2” “2” “/*” “/*” “//”

i1

i2

o1

127 2 −2 127 2 127 0 2 127 3 12 4 2 2 0

Saturate RndMeth false true – – –

– – – – Floor

used to represent special operation results. For example, when the result of multiplication exceeds the expression range, it becomes +∞ with a rounding mode toward the positive direction. Operations with other FP types, float (32 bits) and half (16 bits), also conform to the standard. Simulink handles (signed or unsigned) integers from 8 bits to 64 bits. Integer arithmetic overflows can result in a variety of outcomes. The behavior is controlled via setting the parameters, e.g., SaturateOnIntegerOverflow (we abbreviate it as Saturate) that takes a boolean value, and RndMeth (rounding method) that takes one of six modes. Some tricky examples are shown in the Tab. I; the first column shows the values of the Inputs parameter; each row represent an int8 scalar operation with a setting of three parameters (‘–’ indicates that the values make no difference). As shown in the first two cases, the value of Saturate determines whether the results are wrapped or saturated. In the third example, the first input is interpreted as a division by zero and it results in 127, but in that case, the result of multiplication with i2 is not wrapped; further operation results after division by zero are not wrapped. In the fourth example, the first division number is applied to the second argument as 12/3; it is not immediately operated or rounded, but is sorted in order to improve accuracy. However, it is not the case for the last example, the operations in (1/2)/2 are operated with left associativity. We suspect that sufficiently accurate real number representations (e.g. double values for int8) are used internally for integer operations; then, operations are performed simply by left associativity. The third example can be explained as the result of such an accurate operation; the last example internally results in 0.25 and then rounded to 0.

2.2 Simulink Model Checking 2

SLDV and tools based on SMT solvers such as [3]– [6] provide functionality for formally analyzing Simulink models; we refer to such tools collectively as Simulink model checkers or MC tools. They are given additional descriptions that specify properties on the behavior (signals) of models. Many tools support the MC of safety properties. Given a model M and a property φ, a model checker returns whether M satisfies φ, i.e., every (finite an infinite) trace of M satisfies φ; we denote this fact checked by a tool MC by M |=MC φ. In our method, we consider only bounded safety properties, where both the satisfiability and unsatisfiability of a property can be confirmed by bounded-length executions. Let M = (I, O, S, I, T ) be a Simulink model and φ a property. The properties we consider are in the form of □(C(I [k] ) → C ′ (O[k] )) where I [k] and O[k] are variables representing length-k input and output signals, and C and C ′ are constraints that refer only to values at specific steps within the initial k steps of the argument signal. Obviously, we can check them by examining the executions with k steps. We are interested in verifying the basic functions of the MC tools, so we will limit ourselves to this bounded fragment.

Test suite specification

u

Input signal value samples

Feature models of block types

Delay

Inputs

...

1 0 1 2 ...

Z-2

Output

d

ICSource

...

1

...

Simulink documentation

Oracle

Simulink

1

in

out

Expect output as a Simulation result

k

Simulink model w/ an input

0 1 2 ...

Description ... Input ...

Parameters

Pairwise TV generation

PICT

Oracle

SLDV

...

Z-2

1

in

out

k

Delay z-2

Formalize

T_float: [float, double] T_int: [int32, uint32] T_bool: boolean ... V_float: [v1, v2, ...] V_int: [v3, ...] V_bool: [true, false] ...

0 1 2

...

k

SmtMC

Precisely check

Harnessed Simulink model (TC)

SL 2%

Correct bugs in the encoder

20% 78%

Mutate

...

1 0 1 2 ...

Z-2

in

Pass rate

SmtMC

...

1 out

k

0 1 2

...

k

Model w/ an abstracted input/output

Expect output as an MC result

Pseudooracle

2.2.1 SLDV The toolbox provides property blocks that can specify safety properties to annotate models. Using its “Property Proving” function, users can analyze the annotated properties of a model and obtain reports on their validity. The results are displayed in the GUI and output as HTML reports and binary files. The underlying MC algorithm is not public but it seems to involve multi-stage analysis and model approximation. It is acknowledged by Mathworks that it is based on a model checking module,3 which appears to employ a formal proof method [8]. SLDV interprets models conforming to the Simulink tool, and for numerical operations, it first appears to analyze using a rational approximation, and then more precisely. 2.2.2 SmtMC It is an SMT-based model checker provided as a supplemental functionality in PROMPT V2 [5], a thirdparty tool for the automated testing of Simulink models.4 It supports invariants (formulas on input and output variables enclosed within the □ operator) attached to the input Simulink model. SmtMC encodes the model and the property into a predicate logic formula in the SMT-LIB format [9] (an encoding example is shown in Fig. 7); For the behaviors involving Floating-point numbers, we describe them based on the FloatingPoint theory of SMT-LIB. For Integers, we describe based on the 2 https://www.mathworks.com/products/simulink-design-verifier. html 3 https://se.mathworks.com/help/sldv/ug/acknowledgments.html 4 https://www.en.gaio.co.jp/products/prompt-2/

...

1 0 1 2 ...

Z-2

in

...

SLDV

1 out

k

0 1 2

...

k

TFT ... F

Abstracted TC

Precisely check MCs 2% 20% 78%

TOs: ... OOMs: ... Errors: ... Undecided cases: ... Infinity cases: ...

Pass rate & breakdown

Figure 4. Overview of the testing process.

FixedSizeBitVectors theory, using user-defined arithmetic and rounding operators. SmtMC then checks its satisfiability using the Z3 SMT solver. The encoder of SmtMC offers two options, one that approximates numerical values and one that handles them exactly based on bit vectors; we use solely the latter one in this work. Furthermore, through our experiments, the encoder is gradually replaced with a modified version. 3. Proposed Method We aim at providing a means to check the conformance among Simulink and MC tools. We consider two kinds of conformance, confSL and confMCs (Sect. 3-A). The relation confSL (MC ) expresses that the result of analyzing a Simulink model using an MC tool MC conforms to the behaviors of the model simulated with Simulink (which is considered the the oracle). The relation confMCs (MC 1 , MC 2 ) represents whether the properties of a model checked by MC 1 can also be checked by MC 2 and vice versa; this allows us to compare the range of properties

that MC tools can handle, bit-level precision, and performance. Because the space of arbitrary input models and signals is enormous, the proposed method checks the conformance partially with combinatorial testing [10], [11] which measures the pass rate. As a result, our method cannot guarantee the conformance, but it can detect non-conforming examples. Definition 3: Consider a test suite specification that provides a set F of test factors, i.e. block features and input signal parameters. Let S be a set of TCs that covers all pairwise combinations of factor levels in F , and n be the number of TCs in S that satisfy the condition (confSL ) or (confMCs ). The pass rate is the percentage of n in |S|. The process illustrated in Fig. 4 checks confSL (SmtMC), confSL (SLDV) and confMCs (SmtMC, SLDV). Prior to testing, we prepare a test suite specification (Sect. 3-C) that describes subsets of the Simulink language and input signal values, in which the former subset is specified with a block type feature model (Sect. 3-B). We execute a combinatorial testing procedure (Sect. 3-D) in two ways for each of confSL and confMCs ; it generates TCs in a pairwise combinatorial manner on the test suite factors, and outputs a pass rate (Def. 3). The procedure consists of the following steps. 1) A source of TCs is a test vector generated in a combinatorial manner (we use PICT [10]) based on a test suite specification. We first prepare a Simulink model that consists of a single target block instance and an input signal builder from a test vector. 2) Next, we feed the model to an oracle; depending on the conformance to be verified, we use Simulink or SmtMC as an oracle. Accordingly, we add a conformance verdict based on the output from the oracle to the TC model. 3) Once the TC is fed to the MC tool under test, the output (whether the MC result is not violating the conformance) is aggregated in the pass rate. We also manually analyze all failure cases comprehensively. For the first test, we fix bugs in SmtMC accordingly; in the second test, we classify the results and identify the causes. Sect. 3-E describes some details of the implementation. 3.1 Conformance Relations Following Def. 2, Simulink interprets a model M = (I, O, S, I, T ) as a map [[M ]]SL : D(I)k → D(O)k from input signals to output signals. As described in Sect. 2-B, MC tools (denoted by “MC ”) are fed M and check whether a safety property φ is satisfied (it is denoted by M |=MC φ). Accordingly, we consider two kinds of conformance relations among Simulink and MC tools. Definition 4: The conformance confSL (MC ) of an MC tool MC to Simulink is to satisfy M |=MC □(I [k] = ι[k] → O[k] = [[M ]]SL (ι[k] )) (confSL )

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25

BlockType: Product2 BlockPath: ’simulink/Math Operations/Product’ Inputs: - { Name: ’Port_1’, Multiplicity: [’ scalar’ , ’vector’] , Domain: [T_float, T_int, T_bool] } - { Name: ’Port_2’, Multiplicity: [’ scalar’ , ’vector’] , Domain: ’<Port_1>’ } Output: { Multiplicity: [’ scalar’ , ’vector’] , Domain: ’<Port_1>’, Constraint: ’IF (<im(Port_1)> = ”vector” OR <im(Port_2)> = ”vector”) THEN <om(Output)> = ”vector” ELSE <om(Output)> = ”scalar”’ } Parameters: - { Name: ’Inputs’, Domain: [’2’, ’*/’ , ’/*’ , ’//’] } - { Name: ’SaturateOnIntegerOverflow’, Domain: [’off’, ’on’] } - { Name: ’RndMeth’, Domain: [’Ceiling’,’Nearest’ ,... ] # Some values are omitted. } # Other parameters are omitted. Figure 5. Example block type specification.

for arbitrary models M and input signals ι[k] of arbitrary lengths k. I [k] and O[k] are variables representing input and output signal values from step 0 to k−1. Let MC 1 and MC 2 be MC tools. The conformance confMCs (MC 1 , MC 2 ) between MC 1 and MC 2 is to satisfy M |=MC 1 φ

↔

M |=MC 2 φ

(confMCs )

for arbitrary models M and arbitrary safety properties φ. Reliable conformance checking will be possible if bitprecise MC tools and bit-precise comparisons of signal values in the condition (confSL ) are assumed. Many of existing conformance relations [12]–[15] are defined between models M1 and M2 (i.e. state transition systems) based on the sets L(M1 ) and L(M2 ) of their traces (e.g. input and output signals). In confSL and confMCs , we compare the results of tools T1 and T2 , each of which analyzes models M by interpreting the trace sets LT1 (M ) or LT2 (M ), respectively. 3.2 Block Type Feature Models Each Simulink block type is specified with input and output interfaces and various parameters. The official documentation5 provides specifications for inports, outports and parameters for each block type in natural language. We formally re-describe the content of each block document as a feature model [16], [17] by identifying a set of features; for example, parameter settings, enabled ports, and port data types are regarded as interdependent features. Example (partial) specification for the Product block type, formatted in YAML style, is shown in Fig. 5. 5 https://www.mathworks.com/help/simulink/block-libraries. html

Specifications mainly consist of three sections, Inputs, Output and Parameters, each containing a list of mappings. For blocks that take a variable number of inputs, we describe them separately for each number of inputs; here, we consider blocks with two inports named Port_1 and Port_2. Each mapping is named with a key Name (except for a single Output item), and also has a key Domain whose value is a set of data types (e.g. Port_1) or a list of values (e.g. Inputs). We abbreviate the Simulink data types with T_float (representing double, float , etc.), T_int (representing int8, uint8, int32, etc.) and T_bool (i.e. boolean). Each of input and output ports has a key Multiplicity to specify whether possible signal values are scalar, vector, etc. Items may have dependencies or additional constraints. For example, the dependency of the domain of the outport being the same as inport Port_1 is specified by referencing “<Port_1>.” The key Constraint specifies how its multiplicity is determined depending on the multiplicity of Port_1 and Port_2. Overall, we formalized 10 block types, three of which were specified in two ways for instances of unary and binary operations. The first section of Tab. III summarizes the specified block type feature models. 3.3 Test Suite Specifications Test suites for confSL are specified by the following items. • Block type feature model. Each TC is an instance of a feature model, which is a minimal Simulink model that mainly consist of a block. • Input signal specification. We consider fixed-length (k) input signals to the target block. We manually prepare a table that collects scalar values for each data type for the entire test process. • Simulink as oracle. Checking confMCs involves comparison of the results of SmtMC and SLDV, and we use the results from SmtMC as a pseudo-oracle because it is more efficient and does not produce errors (as we will see in Sect. 4). The Simulink model generated from a test vector is harnessed with an input signal builder; then, it is simulated with Simulink to obtain the output signal, which is embedded in the verdict subsystem of the TC. Test suites for confMCs are also specified by the following items, while uncertain aspects on signal values are additionally introduced. In the experiment, we assume a test suite once prepared for confSL and mutate the TCs so as to introduce uncertainties in the harnessed property monitors. • Block type feature model. • Input signal specification. For every step l ∈ {0, . . . , k− 1} and for every j-th element of the input variable vector I = (i1 , . . . , in ), the input signal builder for the first test specifies the value as ij (l) = ιj (l), where ιj (l) is a prescribed constant. To make it uncertain, we either change it randomly to constraint ij (l) ≤ ιj (l), change it to ij (l) ≥ ιj (l), or leave it unchanged. In the following,

Algorithm 1: A conformance testing procedure. Input : Specification spec, # steps k, Flag doAbst ∈ {true, false} indicating whether to check confMCs Output: Test statistic stat TV := runPICT(spec); stat := ∅; for t ∈ TV do 3 M := generateModel(t); 4 o[k] := runSimulink(M, k); 5 M := addVerdict(M, o[k] ); 6 if doAbst then M := abstractHarness(M ); end 7 stat := updateStat(stat, runMC(M )); 8 end 9 return stat;

1

2

we denote the conjunction of equalities and inequalities for all elements by I [k] ≈ ι[k] . • SmtMC as oracle. Also for the comparison of output signals with expected values [[M ]]SL (ι[k] ), we randomly make some element-wise comparisons into inequalities (the overall conjunction is denoted by O[k] ≈ [[M ]]SL (ι[k] )). We then verify the property φ :↔ □(I [k] ≈ ι[k] → O[k] ≈ [[M ]]SL (ι[k] )) with SmtMC and obtain an expected value in {true, false}. 3.4 Testing Procedure Alg. 1 shows the procedure for each test. When we test confSL of either SmtMC or SLDV, it is supposed to set doAbst as false, and when we test confMCs between SmtMC and SLDV, we set the flag as true. The algorithm measures the pass rate by counting the number of TCs that satisfy the condition (confSL ) or (confMCs ) in Def. 4. First, it generates a set TV of test vectors using a combinatorial testing tool. In advance, we translate the block type feature model and the input signal specification in the format of the testing tool so that the set of generated vectors covers pairwise combinations of test factors. Second, the algorithm generates a Simulink model M that instantiates t ∈ TV ; it also embeds a concrete input signal specified by t using Constant blocks. Third, it runs Simulink to obtain expected output signal values (o[k] ) and construct a verdict that compares output signals from the test block with the values in o[k] . Finally, it runs the target MC tool to check confSL when doAbst is false; accordingly, the overall test result is updated. When doAbst is true, the process checks confMCs for SLDV under uncertainties; namely, we assume a set of input signals instead of a concrete one and test whether or not SLDV can verify conditions on the output signals as SmtMC. The abstractHarness procedure transforms a model M for that purpose. Given concrete input and output signals for M , it first introduces some uncertainties as explained in Sect. 3-C and encodes them in the harness

true == 0

A B

2

Guard1_1_1

Z-1

In1_1_2

A ==> B

Implies1_1_1

> 1.797693134862316e+308

true

Delay1_1_1

1

...

1

Rel1_1_2

x ÷ Target

...

Compare1_1_1

1

true == 0.1

1

B

Guard1_1_2

2

Const1_1_2

In1_1_1 true

A ==> B

Implies1_1_2

>= -10.1

2

1

A

Compare1_1_2

...

true

Test Unit

== 0

Size-Type

B

Guard1_2_1

Rel1_1_1

... ... ...

Const1_1_1

A A ==> B

Implies1_2_1

Compare1_2_1

Figure 6. Simulink harness using SLDV property blocks. 1 2 3 4

(define-fun trans ( (i#1#1 Float64) (i#1#2 Float64) (i#1#3 Float64) (i#2#1 Float64) (o#1#1 Float64) (o#1#2 Float64) (o#1#3 Float64) ) Bool (and (= o#1#1 (fp.div RNE i#1#1 i#2#1)) (= o#1#2 (fp.div RNE i#1#2 i#2#1)) (= o#1#3 (fp.div RNE i#1#3 i#2#1)) ))

5 6 7 8 9 10 11 12 13 14 15 16

(declare-const i#1#1@0 Float64) (declare-const i#1#2@0 Float64) (declare-const i#1#3@0 Float64) (declare-const i#2#1@0 Float64) (declare-const o#1#1@0 Float64) (declare-const o#1#2@0 Float64) (declare-const o#1#3@0 Float64) (assert (fp.leq i#1#1@0 (fp #b0 #b01111111111 #b0001100110011001100110011001100110011001100110011010))) (assert (= i#1#2@0 (_ +zero 11 53))) (assert (fp.geq i#1#3@0 (fp #b1 #b11111111110 #b1111111111111111111111111111111111111111111111111111))) (assert (= i#2#1@0 (_ +zero 11 53))) (assert (trans i#1#1@0 i#1#2@0 i#1#3@0 i#2#1@0 o#1#1@0 o#1#2@0 o#1#3@0)) (check-sat-assuming (not (= o#1#1@0 (_ +oo 11 53)))) (check-sat-assuming (not (= o#1#2@0 (_ NaN 11 53)))) ; ; ... Other checks are omitted. Figure 7. SMT-LIB encoding of the bounded execution.

of M . It then verifies the consistency between the input and output constraints using SmtMC and records the result in the harness as a verdict. 3.5 Implementation We have implemented the conformance testing method (Alg. 1) in the MATLAB scripting language. This implementation integrates Simulink, SLDV, and the SmtMC tool, which is also implemented as a MATLAB script and connected with the Z3 SMT solver [18] (version 4.13.0 or 4.14.1). We used PICT [10] (commit 7d2ed98)6 for combinatorial testing. 3.5.1 Testing of SLDV When the MC tool under test is SLDV, our implementation generates a Simulink harness model and feeds it to SLDV. An example harness model is shown in Fig. 6. The target block in the Test Unit subsystem is an instance of Product representing an element-wise division of type 6 https://github.com/microsoft/pict

F × F3 → F3 where F denotes the set of double FP numbers. The model is modified with abstractHarness to check confMCs . The fragment on the left of Fig. 6 describes the following assumption on the input variable i1 and the signals of length 2. i1 (0) ≤ dbl(10.1) ∧ i1 (1) ≥ dblmax ∧ . . . , where ij (l) represents the j-th element of the value at step l. In the initial step 0, each inport is fed the input value to the target block for all steps, e.g., In1_1_2 is initially fed i1 (1) for the step 1; the values are then concatenated using delay blocks, e.g., Delay1_1_1 receives a signal to be delayed and an initial value. We have an inequality (or equality) for each signal value. Blocks labeled as true in the diagram are SLDV assumption blocks, so the inequality expressions are interpreted as the conditions on the input signals by SLDV. Constant numerals are encoded exactly using the hexadecimal notations. The Size-Type block combines the scalar signals into vector signals if necessary. On the right side of Fig. 6, the model fragment specifies a verdict based on the following condition on the output

TABLE II Data types and the sampled values. Category

Simulink type

#

Values

T_float T_int T_uint T_bool T_string

double int8 uint8 boolean string

10 9 6 2 2

∓realmax(’double’), 0, 1, etc. −127, −10, −1, 0, 1, 2, 19, 127, 128 0, 1, 2, 23, 254, 255 true and false “” and “123”

variables o1,1 and o1,2 . o1,1 (0) = dbl(+∞) ∧ o1,1 (1) ≤ dbl(−10.1) ∧ o1,2 (0) = dbl(NaN) ∧ . . . The model assumes that one step is 0.1 seconds, and conditions are described using SLDV implication blocks; for example, o1,1 (0) is expected to be greater than the largest normal number by Compare1_1_1. The constant numerals are again encoded exactly but rounded decimals are shown in the diagram. To detect NaN, it uses an inequality block (Compare1_2_1) due to that NaN = NaN evaluates to false. 3.5.2 Testing of SmtMC For SmtMC, our implementation modifies its process and adds test verdict formulas to the encoded formula of the target Simulink model. Fig. 7 shows an SMT-LIB description for the example TC in Fig. 6 associated with verdict formulas. The upper part defines predicate trans representing the transition predicate of the Product block. Next, the first transition is described by asserting the predicate with the constant symbols e.g. i#1#1@0; each input value is constrained by comparing it with a constant FP number. In the last part, the constraints are checked for each output symbol. To validate ψ :↔ o1 (0) = dbl(+∞), we check the unsatisfiability by assuming ¬ψ. 4. Experimental Result We experimented to answer the following research questions. RQ1: What are the pass rates for confSL and confMCs achieved by SmtMC and SLDV? RQ2: If the test results are not conformant, what are the reasons? RQ3: What is the difference in test execution time between tools? Experiments were conducted on Docker containers (under the limitation of using up to 4 cores and 8GB RAM), running on a 4.5GHz AMD Ryzen 9 7950X processor. We ran SmtMC and SLDV on MATLAB R2025b. SLDV was also run on R2020b for comparison; we refer to the two versions as SLDV20 and SLDV25, respectively. SLDV was basically set to default settings, but the some parameters were set as follows: MaxTestCaseSteps to 10000; MaxViolationSteps to 1 or 3; DetectInfNaN enabled; DetectDivisionByZero disabled.

The input signal specifications were prepared as follows. Note that, we deliberately prepared a small specification to allow for manual analysis of failure cases in the experiment. Testing using expanded block specifications and enhanced test signals remains a future challenge. First, we set the signal length to 3 for stateful blocks (Delay, UnitDelay and DiscreteIntegrator) and 1 for other stateless blocks (length 1 is sufficient to verify the correctness of the interpretation of such blocks). Second, the test vectors enumerated by PICT included the Domain and Multiplicity attributes. For each data type category in the specification, we map a Simulink data type as shown in Tab. II. As sampled values, among 2 to 10 values for each category were prepared. For example, list of values for type double contained some integers around 0, maximal normal FP numbers, and other normal FP numbers. The Multiplicity attribute specified whether the values are scalar or vector (we do not handle other composite signals e.g. matrices and buses, leaving them for future work). Experimental results are shown in Tab. III. Each row of the table corresponds to a block type (we abbreviate DiscreteIntegrator as DiscInteg). The second section shows basic statistical data: The numbers of inports, block parameters, and the test vectors generated by PICT. The following sections show the results for each tool: The columns “# confSL ” and “# confMCs ” show the numbers of TCs (and the pass rates) that were confirmed to satisfy the condition (confSL ) or (confMCs ). The time taken to process the passed TCs is aggregated in the “Time” column. Although we needed not to test confMCs by targeting SmtMC, we show the time required to check the same abstracted test conditions in the column “Time∗ .” The results for confMCs are presented in the sections for SLDV20 and SLDV25; note that these results represent comparisons between SmtMC and the two versions of SLDV, respectively. As analyzed below, some of the nonconforming TCs were due to SLDV20 or SLDV25 not terminating successfully. SmtMC terminated normally in all TCs. For both SLDV20 and SLDV25 and all TCs, with the exception of test for DiscInteg on SLDV20, the cause of non-conforming cases for relation (confSL ) was due to the failure of compatibility checking, which verifies whether the target model is described with the constructs supported by the model analysis process of SLDV. Unsuccessful DiscInteg TCs on SLDV20 were due to timeouts. Tests for confMCs failed due to various causes. The “Breakdown” column lists the causes in the form “i / j / k,” meaning that: i failures are due to time running out; j tests terminate with an internal error reports; k failures are due to non-conforming results. The TC Simulink models, the encoded SMT-LIB files, and the experimental data are made public at https://doi.org/10.5281/zenodo.19464651.

0/0/0 0/0/0 0/0/9 0/0/0 0/0/0 3 / 0 / 25 0/0/0 0/0/0 0/0/0 0 / 0 / 21 3 / 0 / 34 1 / 0 / 34 97 / 0 / 0

Answer to RQ1: SmtMC passed all test cases for all blocks. We consider the implementation of its encoder to be part of the block specification, so this result was necessary. We repeated the test and debug loop multiple times to improve the tool’s conformance to Simulink. As explained in Sect. 2-A, we analyzed the detailed semantics of each block type and the details of each numerical operations, and implemented them in the encoding process from blocks into logic formulas. All TCs that yielded results different from SLDV were inspected, and we found a number of bugs for the earlier versions; at last, no bugs were found for the latest version. 5.2 Pass Rate of SLDV for confSL (RQ1 and RQ2) Answer to RQ1: The average overall pass rates for SLDV20 and SLDV25 were 94% and 96%, respectively. Answer to RQ2: All TCs (but one) were representing computation that results in the infinity FP numbers, and SLDV failed with a message “Simulink Design Verifier does not support non-finite numbers.” The 1 TC that passed only with SLDV25 was for Product1, and its expected output value was NaN. We did not describe any non-finite numeric literals in all TCs. For example, for a TC describing the addition o1 := i1 + i2 , we only set finite numbers as i1 and i2 and if +∞ was expected for o1 , we monitored it by checking o1 > MV , where MV is a maximum finite number. The number of TCs that passed in both versions differed by 35, mainly due to that some TCs for DiscInteg timed out. By block type, there were non-conforming cases in Sum, Gain and Product. 5.3 Pass Rate of confMCs (SmtMC, SLDV) (RQ1 and RQ2)

A pass-all result was not achieved for most block types except for simple ones (i.e. Constant, Sum1, Abs and Logic). Answer to RQ2: Some of non-conformant TCs were due to timeouts, errors, and “undecided” outputs by SLDV as broken down in Tab. III. Others were due to the handling of infinity FP values.

Total

Answer to RQ1: The average pass rate when comparing SmtMC with SLDV20 or SmtMC with SLDV25 was 80% and 90%, respectively.

124 70 175 138 128 170 126 123 183 243 300 209 179 2 5 6 2 3 3 3 3 3 5 8 3 4

2168 2168(100%) 7190s 15400s 2039( 94%) 16300s 1724( 80%) 178 / 8 / 258 56400s 2075( 96%) 27600s 1941( 90%) 104 / 0 / 123 47100s

Time

1680s 960s 3010s 2690s 2360s 3650s 2220s 1810s 3110s 3650s 10700s 5950s 5290s

Breakdown

124(100%) 70(100%) 166( 95%) 138(100%) 128(100%) 142( 84%) 126(100%) 123(100%) 183(100%) 222( 91%) 263( 88%) 174( 83%) 82( 46%) 1300s 812s 2090s 1210s 1170s 1960s 1480s 1540s 2350s 3120s 3950s 3080s 3470s 124(100%) 70(100%) 169( 97%) 95( 69%) 106( 83%) 148( 87%) 126(100%) 123(100%) 183(100%) 243(100%) 300(100%) 209(100%) 179(100%) 717s 690s 2150s 1900s 1990s 1840s 1360s 1530s 2700s 3890s 8690s 10600s 18300s 0/0/0 0/0/0 0/4/9 11 / 2 / 0 1 / 0 / 12 38 / 0 / 34 0/0/0 0/0/0 0/0/0 0 / 0 / 21 35 / 2 / 75 26 / 0 / 84 67 / 0 / 23 676s 470s 1270s 721s 569s 1140s 754s 864s 1380s 1850s 2730s 2040s 1800s

5.1 Pass Rate of SmtMC for confSL (RQ1)

0 1 2 1 1 2 1 1 2 3 1 or 2 1 1

212s 66s 412s 257s 4400s 5940s 209s 116s 268s 407s 1350s 926s 840s

In this section, we consider the pass rate to be the degree of conformance and confirm it for each tool. We classify the test results and analyze their causes. In particular, we report the result of manual analysis of all TCs that failed with SLDV. In addition, we compare performance of the MC tools in terms of test execution time.

Constant Sum1 Sum2 Gain Product1 Product2 Abs Logic1 Logic2 Switch Delay UnitDelay DiscInteg

124(100%) 213s 70(100%) 75s 175(100%) 429s 138(100%) 290s 128(100%) 167s 170(100%) 413s 126(100%) 270s 123(100%) 178s 183(100%) 462s 243(100%) 680s 300(100%) 1780s 209(100%) 1160s 179(100%) 1070s

124(100%) 70(100%) 169( 97%) 95( 69%) 105( 82%) 148( 87%) 126(100%) 123(100%) 183(100%) 243(100%) 300(100%) 209(100%) 144(80%)

124(100%) 70(100%) 162( 93%) 125( 91%) 115( 90%) 98( 58%) 126(100%) 123(100%) 183(100%) 222( 91%) 188( 63%) 99( 47%) 89( 50%)

SLDV25

# confMCs Time Time Breakdown

# confSL SLDV20

# confMCs Time # confSL Time∗ Time

SmtMC

# confSL

# # # inputs paramsTCs Block type

TABLE III Experimental result.

5. Discussion

Conclusiveness. SmtMC completed all TCs successfully within the time limit, although there were some discrepancies with the results from SLDV in several cases. Timeouts. The tests for Product2, Delay, UnitDelay and DiscInteg took a long time to run on average and a total of 166 with SLDV20 and 104 with SLDV25 resulted in timeouts. The main reason for the 3 blocks was probably that the number of steps was set to 3 instead of 1, which resulted in the tripled number of properties and a large search space. Also, nonlinear multiplication terms will require special handling in the MC process, so we consider that checking Product and DiscInteg blocks was more expensive than checking others. Errors. In tests on several blocks, 8 errors in total occurred with SLDV20. The exact reason was unknown but SLDV reported that they were “internal error” and were annotated as “data_graph_err_internal.” With SLDV25, this error did not occur, but whenever we ran more than about 100 TCs in a row, the program would crash in a way that was difficult to reproduce. Non-conforming results. In other TCs, the results of checking the property blocks by SLDV did not match the results with SmtMC, or SLDV outputted “Undecided.” According to our analysis, the reason for the former case, i.e., when the results were conclusive but non-conforming, was due to ignoring executions where the results became infinite FP numbers. SLDV concluded these TCs as valid although an execution that resulted in an infinity value was violating the property. These cases were the most common causes of non-conforming cases for block types Sum2, Prod2, Switch, Delay, UnitDelay and DiscInteg. There were 57 such TCs with SLDV20 and 101 with SLDV25; many such TCs with SLDV25 were inconclusive with SLDV20. In addition, we found that TCs for other block types contained similar executions and MC was performed as expected. Other non-conforming test results were caused by some properties being judged as “Undecided.” From the output, these can be classified into one of the followings. “Undecided due to division by zero.” It occurred when a TC for Product expressed such execution. There were 41 such TCs with SLDV20 and 16 with SLDV25. • “Undecided with counterexample.” This happened in some TCs (2 with SLDV20 and 6 with SLDV25) for Product2. For example, it occurred for a TC describing an operation o1 := (1/i1 ) × i2 where i1 and i2 are assumed to be the maximum finite FP number and −1.1, respectively, and o1 is expected to be less than a positive normal FP number. The actual cause was unknown to us. • “Undecided.” Most of failed TCs for Delay, UnitDelay and DiscInteg with SLDV20 outputted no additional information and the reasons were unclear. These TCs were conclusive with SLDV25 but ignoring the infinity •

cases. 5.4 Comparison of Execution Times (RQ3) Answer to RQ3: In tests other than Product, SmtMC was several times to several tens of times faster than SLDV. The main reason is probably the simplicity of the process. 5.4.1 Comparison of test processes for confSL and confMCs In the testing of SmtMC, checking TCs with uncertainty generated for confMCs was slightly faster than checking concrete TCs for confSL for all block types except Product. In contrast, TCs of Product for confMCs took a considerable amount of time; we believe this is due to the large number of operation patterns resulting from overflow etc. SLDV took slightly to three times longer to process abstracted TCs for confMCs than TCs for confSL (SLDV20/SLDV25 was 4.9/1.9 times longer on average). SLDV seemed to have difficulty handling uncertainty. 5.4.2 Comparison between SLDV20 and SLDV25 SLDV25 resulted in higher pass rates due to that it could handle more cases within the time limit without outputting “Undecided” compared to SLDV20. In the test process for confSL , SLDV20 had a shorter execution time than SLDV25. On average, it was 1.7 times faster. In the test of confMCs , SLDV20 was faster for the first 9 and slower for the last 4 block types. With SLDV25, the number of test that run out of time decreased except for DiscInteg, and the tests of UnitDelay and DiscInteg, which were relatively resource-intensive, were processed 2–3 times faster in average. It was suggested the MC algorithms might be different. 6. Threats to Validity We point out two threats to internal validity (I-1 and I-2) and a threat to external validity (E-1). I-1) Diversity and completeness of test cases. The number of prepared TCs can be insufficient due to that the factors in the block type specifications and the samples for the input signals are limited. Therefore, it is possible that we have overlooked some bugs or non-conforming processes in the model checkers. Considering that we manually analyzed the causes of the failed TCs, we believe that we conducted a sufficient number of them. We also consider that the number of TCs was sufficient to improve the SmtMC encoder through debugging; in the end, it appears that the encoder implements generalized algorithms for each block type. Nevertheless, further testing is a future task. I-2) Adequacy of the testing approach. Another threat is that, our approach may not be adequate for testing the quality of MC tools. Other approaches include testing using artificial evaluation kits, as well as fuzzing and mutation testing based on practical Simulink models, as

described in Sect. 7. In comparison, we apply automated testing methods to the Simulink toolchain with minimal manual intervention within a basic scope, and we consider this engineering effort to be reasonable. There are threats that testing of key features may be insufficient, or that bugs which only appear within large models may go undetected. There are threats regarding the test oracles. The Simulink simulator used as a basis of confSL might have bugs, compromising the consistency of the specifications we have formalized. SmtMC used for confMCs was just validated with the first test with a limited number of TCs, so its reliability might be doubtful; however, it should be noted that SmtMC is used as a pseudo-oracle in the process, and the two tools are being compared equally. E-1) Formalization of basic Simulink block types. Inappropriate choice of the domain of TC generation can be a threat to external validity. There is concern as to whether the practically developed models align with the set of models we have generated in this work. We focused on the basic block types, but other block types or combinations of several blocks can be more important factors for checking the correctness of the model checkers. As a first step from the simplest form, we dealt with the 10 basic block types. 7. Related Work 7.1 Formalization of Simulink Tripakis et al. [19] and Bourbouh et al. [4] propose to convert a subset of the Simulink language to Lustre, a synchronous programming language. Bouissou and Chapoutot [20] formalize the integration process for discrete and continuous models and basic computation by some blocks. Zhan et al. [21] propose a formalization based on process algebra (CSP). Bourke et al. [22] formalize a Simulink-like language in Coq and provide a validated code generation method. Some [4], [19], [22] consider to translate Simulink models into transition systems, which are similar to our method, but differ in that they do not consider conforming them to bit-precise numerical computation implemented in Simulink. We are also unique in that we focus on the diversity of block instances and attempt to cover all parameter settings. 7.2 Qualification of Simulink, SLDV, etc. As the standards e.g. ISO 26262 and DO-178C demand, confidence in the toolchain used and qualification of each tool are important in the model-based development of safety-critical systems [2], [23]. There is research on testing and verifying the practicality of the tools for modeling and MC, respectively; our work belongs to the latter. Chowdhury et al. [24]–[26] propose a series of testing methods and tools, CyFuzz, SLforge and SLEMI, for finding bugs in Simulink. Their methods are based on random testing and a collection of models, and some methods also employ techniques such as EMI-based mutation

testing and differential testing. SLforge and SLEMI have reported finding 8 and 9 new bugs, respectively. Jiang et al. [27] propose a method for finding bugs in Simulink code generation by performing differential testing on multiple code generation processes; as a result, they have reported 11 new bugs. In this paper, we do not target Simulink but use it as an oracle as is, and conduct random tests to verify the conformance of model checkers. The standard DO-330 recommends certifying the tool when the correctness of the tool output alone is not clear; also, DO-333 describes how to use formal methods in development [2], [23]. The result of a SWOT analysis [28] organizes the perspectives for qualification of formal method tools used in CPS development. In response, certification kits for MC tools, including ones from Mathworks,7 have been developed. For example, the qualification package of the Kind2 model checker includes TCs that take into account the features of the modeling language [23]. The test suite generated by our proposed method addresses the basic features of the Simulink language and can be regarded as a kind of qualification kit, but the features it covers are limited; on the other hand, it is more precise than other kits to consider the numerical semantics of each block type. There are several case studies that evaluate the usefulness and shortcomings of SLDV functions and performance. Nellen et al. [29] have attempted verification using SLDV against an in-vehicle system and pointed out gaps between industry needs and functions; similar to this work, they found that checking several properties took a long time and obtained many inconclusive results; they also obtained one spurious counterexample and pointed out reliability issues in numerical analysis. Nejati et al. [30] have collected 10 industrial Simulink models and analyzed the verification results of applying a test method and an SMT-based MC tool; as a result, they pointed out that MC guarantees the exhaustiveness not like testing, but has issues with scalability. Murray et al. [31] have compared the MC functions of SLDV and RoboTool; they also faced the analysis time issues and needed to simplify their models. In this paper, we deal with the artificial Simulink models that are prepared in a minimalist manner and do not evaluate scalability with respect to model size. However, we have confirmed that the execution time of SLDV increases when properties are made uncertain. We have also conducted precise tests on numerical computation, which differs from other case studies. 7.3 Bit-Precise Verification Methods Numerical systems have been verified based on formalized FP numbers [32]–[35] and fixed-point numbers [36], [37]. None of them but SmtMC [5] tested in this paper verify Simulink models in a bit-precise way; its analysis is based on a bit-blasting FP solver [34], [35] and integer 7 https://www.mathworks.com/products/iec-61508.html

arithmetic operators implemented as in [36] based on the bit-vector theory. The verification with our testing method is incomplete, so future tasks include verifying the numerical operation of the block types more exhaustively and formally, and generating provable certificates from the MC process. 8. Conclusion We have described an empirical evaluation targeting two Simulink model checkers, SmtMC and SLDV. Our evaluation method is based on automatically measuring pass rates through block instantiation and checking the conformance conditions for confSL and confMCs . As deliverables, we developed block-type feature models, a modified bit-precise encoder of SmtMC, and the test suite. As a result of the evaluation, SmtMC passed all test cases and confirmed the conformance to Simulink within the scope of the specification, albeit incompletely. We found some issues with the standard tool SLDV. In the testing for confSL , the pass rate was 94–96%, due to the nonconforming TCs in the handling of infinity FP numbers. For confMCs , certain numbers of TCs were inconclusive (186 for R2020b and 104 for R2025b), causing the pass rate to drop by a few percent. Overall, as the version number increased, the conformance rate between tools improved, and we identified the causes of failed TCs. As a result, we were able to obtain the implementation of SmtMC that formally describes the language specification. Currently limited to a subset of blocks and their features, we were able to verify whether the tools replicate the Simulink simulator with bit-level precision. We expect that this approach will improve reliability in CPS engineering. As future work, more comprehensive specification descriptions and testing are required. Specifically, we need to handle additional block types, generalize each block type specification, and improve the encoder. In addition, testing requires consideration of a larger number of sampled signals, combinations of several block instances, and verification of more generic properties. This will provide a test suite that can be used as a qualification kit for the toolchain. References [1] E. A. Lee and S. A. Seshia, Introduction to Embedded Systems. A Cyber-Physical Systems Approach, 2nd ed. MIT Press, 2017. [2] M. Ibrahim and U. Durak, “State of the Art in Software Tool Qualification with DO-330: A Survey,” in Software Engineering 2021 Satellite Events, ser. LNI, 2021, pp. 1–23. [3] P. Schrammel, D. Kroening, M. Brain, R. Martins, T. Teige, and T. Bienmüller, “Incremental bounded model checking for embedded software,” Formal Aspects of Computing, vol. 29, pp. 911–931, 2017.

[4] H. Bourbouh, P.-l. Garoche, T. Loquen, E. Noulard, and C. Pagetti, “CoCoSim, a code generation framework for control/command applications,” in ERTS, 2020, pp. 1–11. [5] D. Ishii, T. Tomita, T. Aoki, T. Q. Ngo, T. B. N. Do, and H. Takai, “SMT-Based Model Checking of Industrial Simulink Models,” in ICFEM, ser. LNCS 13478, 2022, pp. 156–172. [6] R. Cleaveland, D. Hansel, S. Sims, and S. A. Smolka, “Two Decades of Industrializing Formal Verification: The Reactis Story,” in Model Checking Software, vol. 14624. Cham: Springer Nature Switzerland, 2025, pp. 87–105. [7] IEEE, 754-2008 – IEEE Standard for Floating-Point Arithmetic, 2008. [8] M. Sheeran and G. Stålmarck, “A tutorial on Stlåmarck’s proof procedure for propositional logic,” in FMCAD, ser. LNCS 1522, 2002. [9] C. Barrett, P. Fontaine, and C. Tinelli, “The SMTLIB Standard,” 2025. [10] J. Czerwonka, “Pairwise Testing in Real World,” in PNSQC, 2006, pp. 419–430. [11] D. R. Kuhn, R. Bryce, F. Duan, L. S. Ghandehari, Y. Lei, and R. N. Kacker, “Combinatorial Testing. Theory and Practice,” in Advances in Computers. Elsevier, 2015, vol. 99, pp. 1–66. [12] G. J. Tretmans, “A Formal Approach to Conformance Testing,” Ph.D. dissertation, 1992. [13] M. Broy, B. Jonsson, J. P. Katoen, M. Leucker, and A. Pretschner, Model-Based Testing of Reactive Systems, ser. LNCS. Springer, 2005, no. 3472. [14] R. M. Hierons, K. Bogdanov, J. P. Bowen, R. Cleaveland, J. Derrick, J. Dick, M. Gheorghe, M. Harman, K. Kapoor, P. Krause, G. Lüttgen, A. J. H. Simons, S. Vilkomir, M. R. Woodward, and H. Zedan, “Using formal specifications to support testing,” ACM Computing Surveys, vol. 41, no. 2, pp. 1–76, 2009. [15] A. Aerts, M. Reniers, and M. Mousavi, “ModelBased Testing of Cyber-Physical Systems,” in CyberPhysical Systems. Elsevier, 2017, pp. 287–304. [16] D. Benavides, S. Segura, and A. Ruiz-Cortés, “Automated analysis of feature models 20 years later: A literature review,” Information Systems, vol. 35, no. 6, pp. 615–636, Sep. 2010. [17] M. F. Johansen, Ø. Haugen, and F. Fleurey, “Properties of Realistic Feature Models Make Combinatorial Testing of Product Lines Feasible,” in Model Driven Engineering Languages and Systems, ser. LNCS 6981. Springer, 2011, pp. 638–652. [18] L. de Moura and N. Bjørner, “Z3: An Efficient SMT Solver,” in TACAS, ser. LNCS 4963, 2008, pp. 337– 340. [19] S. Tripakis, C. Sofronis, P. Caspi, and A. Curic, “Translating Discrete-Time Simulink to Lustre,” ACM Transactions on Embedded Computing Systems, vol. 4, no. 4, pp. 779–818, 2005.

[20] O. Bouissou and A. Chapoutot, “An operational semantics for Simulink’s simulation engine,” ACM SIGPLAN Notices, vol. 47, no. 5, pp. 129–138, 2012. [21] N. Zhan, S. Wang, and H. Zhao, Formal Verification of Simulink/Stateflow Diagrams. Springer, 2017. [22] T. Bourke, L. Brun, and M. Pouzet, “Mechanized semantics and verified compilation for a dataflow synchronous language with reset,” in POPL, vol. 4, 2020, pp. 1–29. [23] L. Wagner, D. Cofer, K. Slind, C. Tinelli, and A. Mebsout, “Formal Methods Tool Qualification,” Tech. Rep. NASA/CR-2017-219371, 2017. [24] S. A. Chowdhury, T. T. Johnson, and C. Csallner, “CyFuzz: A Differential Testing Framework for Cyber-Physical Systems Development Environments,” in CyPhy, ser. LNCS 10107. Springer, 2017, pp. 46–60. [25] S. A. Chowdhury, M. Soumik, S. Mehra, S. Gawsane, T. T. Johnson, and C. Csallner, “Automatically finding bugs in commercial cyber-physical system development tool chain with SLforge,” in ICSE, 2018, pp. 981–992. [26] S. A. Chowdhury, S. L. Shrestha, T. T. Johnson, and C. Csallner, “SLEMI: Equivalence modulo input (EMI) based mutation of CPS models for finding compiler bugs in Simulink,” in ICSE, 2020, pp. 335– 346. [27] H. Jiang, H. Cheng, S. Guo, and X. Li, “Partition Based Differential Testing for Finding Embedded Code Generation Bugs in Simulink,” in Design Automation Conference (DAC). IEEE, Jul. 2023, pp. 1–6. [28] M. Gleirscher, R. Sachtleben, and J. Peleska, “Qualification of proof assistants, checkers, and generators: Where are we and what next?” Science of Computer Programming, vol. 226, Mar. 2023. [29] J. Nellen, T. Rambow, M. T. B. Waez, E. Ábrahám, and J.-P. Katoen, “Formal Verification of Automotive Simulink Controller Models: Empirical Technical Challenges, Evaluation and Recommendations,” in FM, ser. LNCS 10951. Springer, 2018, pp. 382–398. [30] S. Nejati, K. Gaaloul, C. Menghi, L. C. Briand, S. Foster, and D. Wolfe, “Evaluating model testing and model checking for finding requirements violations in Simulink models,” in ESEC/FSE. ACM, 2019, pp. 1015–1025. [31] Y. Murray, D. A. Anisi, M. Sirevåg, P. Ribeiro, and R. S. Hagag, “Safety Assurance of a High Voltage Controller for an Industrial Robotic System,” in SBMF, vol. LNCS 12475. Springer, 2020, pp. 45–63. [32] J. Harrison, “Floating-Point Verification Using Theorem Proving,” in SFM, ser. LNCS 3965, 2006, pp. 211–242. [33] S. Boldo and G. Melquiond, “Flocq: A unified library for proving floating-point algorithms in Coq,” in ARITH, 2011, pp. 243–252.

[34] A. Brillout, D. Kroening, and T. Wahl, “Mixed Abstractions for Floating-Point Arithmetic,” in FMCAD. IEEE, 2009, pp. 69–76. [35] M. Brain, C. Tinelli, P. Rüemmer, and T. Wahl, “An Automatable Formal Semantics for IEEE-754 Floating-Point Arithmetic,” in ARITH, 2015, pp. 160–167. [36] M. Baranowski, S. He, M. Lechner, T. S. Nguyen, and Z. Rakamarić, “An SMT Theory of Fixed-Point Arithmetic,” ser. LNCS 12166, 2020, pp. 13–31. [37] G. Devadze, L. Flessing, and S. Streif, “Formal Verification of a Controller Implementation in FixedPoint Arithmetic,” in European Control Conference (ECC). IEEE, Jun. 2023, pp. 1–6.