Official websites use .gov
A .gov website belongs to an official government organization in the United States.
Secure .gov websites use HTTPS
A lock (
) or https:// means you’ve safely connected to the .gov website. Share sensitive information only on official, secure websites.
Design/Modeling Verification Tools
[SAMATE Home | IntrO TO SAMATE | SARD | SATE | Bugs Framework | Publications | Tool Survey | Resources]
Software Design/Modeling Verification Tools: Formal modeling of an application prior to implementation can provide great insight into design validity. The usefulness of modeling tools to verify that no vulnerabilities will exist in the finished product is a topic for discussion in the SAMATE project. A limited taxonomy of functions for this class of tool is listed below.
Design/Model verification tools may have any of the following functions:
- simulation
- exhaustive verification
- proof of design
DISCLAIMER: Certain trade names and company products are mentioned in the text or identified. In no case does such identification imply recommendation or endorsement by the National Institute of Standards and Technology (NIST), nor does it imply that the products are necessarily the best available for the purpose.
By selecting almost any of these links, you will be leaving NIST webspace. We provide these links because they may have information of interest to you. No inferences should be drawn because some sites are referenced, or not, from this page. There may be other web sites that are more appropriate for your purpose. NIST does not necessarily endorse the views expressed, or concur with the assertions presented on these sites. Further, NIST does not endorse any commercial products that may be mentioned on these sites.
Please contact us if you think something should be included. If it has all the characteristics of the tool, techniques, etc., we will be happy to add it. You can contact us at samate(at)nist(dot)gov.
- The Perfect specification language, works with a subset of C/C++ (based on MISRA-C) and SPARK Ada. The Escher C Verifier and the Perfect Developer can generate code or verify programs. (9 Apr 2013)
- SDMetrics is a design quality measurement tool for UML.
- Reports design size, coupling, and complexity.
- Detects incomplete or incorrect design, circular dependencies, etc.