Page 1 of 1

Simulink Design Verifier

PostPosted: Thu May 08, 2008 6:06 pm
by jack
What is the different between Simulink Tester and Simulink Design Verifier?

Re: Simulink Design Verifier

PostPosted: Fri May 09, 2008 8:42 am
by busser
jack wrote:What is the different between Simulink Tester and Simulink Design Verifier?

In general, the focus of Simulink Design Verifier is to work within the model simulation environment, creating tests to run in simulation, rather than against the target application code. A test that passes in simulation is not guaranteed to pass in the actual application because there is no guarantee that the RTW produces perfect code. The RTW code generator is a completely different application than the Simulation engine. We have found many cases where the results from simulation do not match the results produced in the actual application when the same input values are applied. T-VEC's focus is on producing test vectors that verify that the actual application correctly implements the model.

Also, we believe that T-VEC's test generation technology is superior to that of Design Verifier. T-VEC was initially designed and built in the late 1980's and has been in continuous development and improvement for almost 20 years. In addition, T-VEC's theorem prover engine was designed very specifically and directly for embedded systems application analysis and test generation. Design Verifier is based on a general purpose theorem prover technology called "Prover". It was designed for general purpose application and has only recently been extended to attempt to provide test vector generation capabilities. It is not very good at doing this. It is not good at floating point constraint solving and is also not good at scaling up to large systems and system integration testing. It is restricted to attempting to produce tests primarily at the unit level. It also requires much more work on the part of the user to configure and use. It requires adding special purpose Simulink blocks to the model, for example, which modifies the model itself. So, the tests run in simulation are not even running on the same model as that used for code generation. T-VEC does not require any modification of the model, it operates on exactly the same model that the RTW system produces code from.

Also, Design Verifier's marketing statements such as this

"Simulink Design Verifier proves the validity of functional requirements that you specify with blocks from the Simulink Model Verification and Simulink Design Verifier libraries. These blocks control the permissible values of signals in your model."

are somewhat misleading. It is not possible to "prove the validity" of functional requirements by specifying assertions about signals in a design model. It is sometimes possible to "verify" that a design model is consistent with one or more assertions about the properties of the design model's signals. But this does not prove that the functional requirements are "valid". We believe this to be an incorrect marketing statement.

T-VEC has a complete Functional Requirements specification tool called TTM. Test vectors can be generated from this model completely independently from Simulink and these test vectors can then be run on the code produced by Simulink to verify that the design, and also the target application, is consistent/correct with respect to independently specified functional requirements. This is a stronger verification of the satisfaction of functional requirements than simply adding assertion blocks to specific points in the Simulink model. However, T-VEC's Simulink Tester can ALSO verify property assertions about Simulink signals using the Global and Local assertions mechanism. These mechanisms can perform the same conceptual functionality as Design Verifier, but does not modify the model itself. For this and other reasons, we believe T-VEC's approach is both superior and also provides greater verification capabilities that span across a greater degree of the software development life cycle and requirements/design/implementation information model.

In summary, Design Verifier's purpose is a bit different than T-VEC's and it is approach is very different. In addition, its capabilities are not as extensive and it maturity as a product is very limited, compared with T-VEC. Finally, it is a tool produced by Mathworks to verify the results of using Mathwork's own Simulink tool. There is no independence between the vendor of the tool producing the model and the vendor of the tool verifying the model. Such a lack of independence is problematic at many levels.