In the following picture we describe our testing approach.

Structural correctness of the specification is tackled in the
*BlockLibrary instance verification* page, such correctness is mandatory but not
sufficient in order to prove the full correctness of a BlockLibrary
specification. In order to provide such confidence, the semantic given for
each Block must be checked according to the one expected by the user/specifier.

We propose here to rely on test generation and simulation in order to achieve this objective. This process is detailed here:

BlockMode Signature generation:For eachBlockMode, a set ofBlockModeSignaturesis generated. For a BlockMode, the set of its BlockModeSignatures is taken as a TestCase. Generation of signatures is detailed inMode resolution.Input data generation:According to each Signature, a set ofinput datais generated. These data are inputs for blocks instances (value on inputs ports, values of parameters). SeeInput data generation for test casesfor more details.Execute test procedure:Generated source code produced by the Automatic code generator implementation is executed witSimplePDL-EMF-Java-manipuler-tp.exoh input data produced in test cases. This execution producestest results. These results need to be compared to a reference result for this mode of computation.BL_TR_3.2:For each BlockMode and its corresponding Signatures, we generate aSimulinkBlockcalled: Matlab function. These blocks holds a Matlab function that is possible to execute in aSimulink environment. By feeding this Simulink block with in previously described input data, we obtain a reference result (oracleor also known asExpected test results). SeeMatlab Function generationfor more details.Checking for correspondanceComparison betweentest resultsandexpected test resultsprovide a validation result for the semantic expressed in the BlockLibrary specification.

For each BlockMode signature we can get the complete set of inputs and parameters with their respective datatypes and the corresponding constraints expressed at the specification level in the BlockLibrary Model.

A CSP solver (cf: Choco) can be used in order to generate condidates for the input data.

We developped a prototype implementation of model transformation taking as input a BlockLibrary model and providing for each signature of each BlockMode a .mzn file. This implementation can be found in the org.geneauto.blocklibrary.validationGeneration.toMZN project. An example of such generation is provided in the following sections.

```
library Simulink_Basic {
typeDef realDouble double
typeDef enum onoff {'ON', 'OFF'}
typeDef array h1type of double [16,2]
blockType OneDInter {
variant OneDInter_Root isDynamic {
out data s1 : double
in data e1 : double
parameter exth1 : onoff
}
variant H1asParameter extends and OneDInter_Root {
parameter h1 : h1type {
struct as fol # forall i:int. (0 <= i < 15) -> h1[i][0] <. h1[i+1][0] #
}
struct
as eml # exth1 = OFF #
as fol # exth1 = OFF #
}
variant H1asInput extends and OneDInter_Root {
in data h1 : h1type {
struct as fol # forall i:int. (0 <= i < 15) -> h1[i][0] <. h1[i+1][0] #
}
struct
as eml # exth1 = ON #
as fol # exth1 = ON #
}
mode OneDInter_inf implements uxor H1asInput, H1asParameter {
struct as fol # e1 <. h1[0][0] #
// compute as fol # s1 = h1[0][1] #
compute as eml # s1 = h1(1,2); #
}
mode OneDInter_sup implements uxor H1asInput, H1asParameter {
struct as fol # e1 >=. h1[15][0] /\ e1 >=. h1[0][0] #
// compute as fol # s1 = h1[15][1] #
compute as eml # s1 = h1(16,2); #
}
mode OneDInter_mid implements uxor H1asInput, H1asParameter {
struct
as fol # e1 <. h1[15][0] /\ e1 >=. h1[0][0] #
// compute as fol # exists i:int. 0 <= i <= 14 -> h1[i][0] <=. e1 <. h1[i+1][0] #
// compute as fol # s1 = h1[i][1] +. ((e1-h1[i][0])*.((h1[i+1][1]-.h1[i][1])/.(h1[i+1][0]-.h1[i][0]))) #
compute as eml #
tmp = find(h1(1,:) < e1);
i = tmp(end);
s1 = h1(i,2) + ((e1-h1(i,1))*((h1(i+1,2)-h1(i,2))/(h1(i+1,1)-h1(i,1)))) ; #
}
}
}
```

This mzn file is generated for the BlockMode OneDInter_mid and the BlockVariants H1asParameter and OneDInter_Root.

```
% Enumerations
set of int: onoff = 1..2;
int: ON = 1;
int: OFF = 2;
% Inputs
var float: e1;
% Parameters
var onoff: exth1;
array[ 1..16, 1..2] of var float: h1;
% Inputs linked constraints
% Parameters linked constraints
constraint forall (i in 1..15) (h1[i,1] < h1[i+1,1]);
% BlockVariants linked constraints
constraint exth1 = OFF;
constraint e1 < h1[15,1] /\ e1 >= h1[1,1];
% Solving
solve satisfy;
% Output
output [
"e1 = ", show(e1), "\n",
"exth1 = ", show(exth1), "\n",
"h1 = ", show(h1), "\n",
]
```

We decide to use G12 miniZinc implementation v1.6 in order to interpret the generated mzn files.

Calling the solver is done with the following command:

mzn-g12mip OneDInter_OneDInter_mid_Sig2.mzn

Calling the solver results in the following output:

```
e1 = -2e-06
exth1 = 2
h1 = [-1.5000000000000004e-05, 0.0, -1.4000000000000003e-05, 0.0, -1.3000000000000003e-05, 0.0, -1.2000000000000002e-05, 0.0, -1.1000000000000001e-05, 0.0, -1e-05, 0.0, -9e-06, 0.0, -8e-06, 0.0, -6.999999999999999e-06, 0.0, -5.999999999999999e-06, 0.0, -4.9999999999999996e-06, 0.0, -4e-06, 0.0, -3e-06, 0.0, -2e-06, 0.0, -1e-06, 0.0, 0.0, 0.0]
----------
==========
```

We use the previously presented input bls file. The EML functions generator is provided in the org.geneauto.blocklibrary.validationGeneration.toEML project.

The result of the generation of the EML function in the same case (BlockMode OneDInter_mid and the BlockVariants H1asParameter and OneDInter_Root) is provided in the next listing.

```
function [s1] = OneDInter_OneDInter_mid_Sig2(e1)
% This is the documentation for the signature of BlockType: OneDInter
% The BlockMode implemented here is: OneDInter_mid
%% Parameters
param1 = 'exth1';
param1_value = 'This has to be generated by constraint solver';
param2 = 'h1';
param2_value = 'This has to be generated by constraint solver';
params = struct(param1,param1_value,param2,param2_value) ;
%% Computation
tmp = find(h1(1,:) < e1); i = tmp(end);
s1 = h1(i,2) + ((e1-h1(i,1))*((h1(i+1,2)-h1(i,2))/(h1(i+1,1)-h1(i,1)))) ;
end
```

The results of the data generation from the CSP solver must be fed in this generation in order to fill the ‘This has to be generated by constraint solver’ sections of the generation.