Explicit state model checking of sl/sf models using the auto-generated code

A system for validating a model of a control system as per a set of specifications of the control system, the specifications including input conditions and corresponding expected output values of one or more model-parameters, the system comprising:

• a first module for obtaining a model-code corresponding to the model, wherein the model-code is obtained from a modeling tool;
• a second module using a testing tool to obtaining a test-code capable of monitoring one or more model-parameters to be validated;
• a composer for integrating the model-code and the test-code to obtain an integrated-code;
• and
• an execution module for executing the integrated-code in the testing tool, wherein the testing tool correlates actual output values of the one or more model-parameters with the expected output values of the one or more model-parameters, wherein the model of the control system is identified as one of valid or invalid based on the correlation between the actual output values of the one or more model-parameters with the expected output values of the one or more model-parameters.

A computer program product for validating a model of a control system as per a set of specifications of the control system, the specifications including input conditions and corresponding expected output values of one or more model-parameters, the computer program product comprising a computer readable medium comprising:

• means for obtaining a model-code corresponding to the model, wherein the model-code is obtained using a modeling tool;
• means for using a testing tool to generate a test-code capable of monitoring one or more model-parameters to be validated;
• means for integrating the model-code and the test-code to obtain an integrated-code;
• means for executing the integrated-code in the testing tool, wherein the testing tool correlates actual output values of the one or more model-parameters with the expected output values of the one or more model-parameters;
• means for using the testing tool to check for temporal relationships between the input conditions and the output values, wherein the input conditions and the output values are specified in linear temporal logic;
• and
• means for identifying the model of the control system as one of valid or invalid based on the correlation between the actual output values of the one or more model-parameters with the expected output values of the one or more model-parameters.