Testing and Simulation

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:

  1. BlockMode Signature generation: For each BlockMode, a set of BlockModeSignatures is generated. For a BlockMode, the set of its BlockModeSignatures is taken as a TestCase. Generation of signatures is detailed in Mode resolution.
  2. Input data generation: According to each Signature, a set of input data is generated. These data are inputs for blocks instances (value on inputs ports, values of parameters). See Input data generation for test cases for more details.
  3. 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 produces test results. These results need to be compared to a reference result for this mode of computation.
  4. BL_TR_3.2: For each BlockMode and its corresponding Signatures, we generate a SimulinkBlock called: Matlab function. These blocks holds a Matlab function that is possible to execute in a Simulink environment. By feeding this Simulink block with in previously described input data, we obtain a reference result (oracle or also known as Expected test results). See Matlab Function generation for more details.
  5. Checking for correspondance Comparison between test results and expected test results provide a validation result for the semantic expressed in the BlockLibrary specification.

Input data generation for test cases

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.

Input: a blocklibrary instance

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)))) ; #
		}
	}
}

Output: mzn file

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",
]

Generation of data with a CSP solver

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]
----------
==========

Matlab Function generation

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.