EXPLICIT STATE MODEL CHECKING OF SL/SF MODELS USING THE AUTO-GENERATED CODE
A system and a method for validating a model for a control system as per a set of specifications. The method includes obtaining a model code corresponding to the model, where the model-code is generated by a modeling tool. Further, a test-code capable of monitoring one or more model parameters that need to be validated is generated using a testing tool. The model-code and the test-code are combined to obtain an integrated-code. The integrated code is executed in the testing tool that compares the obtained output values with the expected output values as provided in the specifications. Further, the model is identified as valid or invalid based on the comparison based on the results of the comparison.
1 . A method 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 method comprising:
obtaining a model-code corresponding to the model, where the model-code is obtained using a modeling tool;
using a testing tool to generate a test-code capable of monitoring one or more model-parameters to be validated;
integrating the model-code and the test-code to obtain an integrated-code;
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; and
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.
2 . The method according to claim 1 further comprising using the testing tool to check for temporal relationships between the input conditions and the output values.
3 . The method according to claim 2 wherein the input conditions and the output values are specified in linear temporal logic.
4 . The method according to claim 1 wherein the model of the control system is a Simulink/Stateflow (SL/SF) model.
5 . The method according to claim 1 wherein the modeling tool is a real-time workshop (RTW) code generator.
6 . The method according to claim 1 wherein the model-code and the test-code are integrated using a composer.
7 . The method according to claim 1 further comprising generating a counter-example by the testing tool when the model is identified as invalid.
8 . The method according to claim 6 wherein the counter-example is used to trace an error in the model.
9 . 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.
10 . The system according to claim 9 wherein the second module uses the testing tool to check for temporal relationships between the input conditions and the output values.
11 . The system according to claim 10 wherein the input conditions and the output values are specified in linear temporal logic.
12 . The system according to claim 9 wherein the model of the control system is a Simulink/Stateflow (SL/SF) model.
13 . The system according to claim 9 wherein the modeling tool is a real-time workshop (RTW) code generator.
14 . The system according to claim 9 wherein the testing tool generates a counter-example when the model is identified as invalid.
15 . The system according to claim 14 wherein the counter-example is used to trace an error in the model.
16 . 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.
17 . The product according to claim 16 wherein the model of the control system is a Simulink/Stateflow (SL/SF) model.
18 . The product according to claim 16 wherein the modeling tool is a real-time workshop (RTW) code generator.
19 . The product according to claim 16 wherein the testing tool generates a counter-example when the model is identified as invalid.
20 . The product according to claim 19 wherein the counter-example is used to trace an error in the model.