Testing and Validation
Statemate ModelChecker and Statemate ModelCertifier Statemate ModelChecker and Statemate ModelCertifier allow systems designers to validate their Statemate models, ensure that they follow good design practices, and prove that they meet user defined critical properties, such as safety. It allows system engineers to ensure that their designs perform correctly under all circumstances, both those that are expected, as well as those that are unexpected. Statemate ModelChecker and Statemate ModelCertifier, based on the most advanced state-of-the art Formal Verification technologies, are designed to be easy to use, providing push button analysis. These tools not only reduce the time needed to develop a good specification model, which can be used as a "Reference model", but significantly improve its quality above and beyond what is achievable with current design methods. Statemate ATG Statemate Automatic Test Generation (ATG) allows end users to generate Test Vectors directly from the Statemate model. These Test Vectors provide a high degree of coverage for the elements in the Statemate model (such as states, transitions, output toggling etc.). These Test Vectors can then be applied on the implementation, to make sure that the implementation responds the same way as the Statemate model. Statemate Verification Pack Featuring Statemate ModelCertifier and Statemate ATG. Both address different aspects of testing, it is only natural to use these two tools in conjunction with each other. As more customers are inserting both capabilities into their development process, Telelogic decided to provide a package, at an attractive price, that will include both products. Additionally, this package includes a single training for both products, with a focus on using both of them as part of a seamless model based development and testing process. |
