Model-Based Verification: Claim Creation Guidelines

October 2001 • Technical Note

Santiago Comella-Dorda, David P. Gluch, John J. Hudak, Grace Lewis, Charles B. Weinstock

This 2001 report describes a pattern-based approach to facilitate claim generation.

Publisher:

Software Engineering Institute

CMU/SEI Report Number

CMU/SEI-2001-TN-018

Subjects

Performance and DependabilityPerformance and Dependability

Abstract

Model Based Verification (MBV) is a systematic approach to finding defects (errors) in software requirements, designs, or code. MBV involves creating essential models of system behavior and analyzing these models against formal representations of expected properties, known as claims. Claim generation has been identified as a particularly complex activity within model-based verification. This technical note describes a pattern-based approach to facilitate claim generation. The report includes a list of directly usable patterns for the most frequent expected properties found in system specifications.

Download PDF

Cite This Report

SEI

Comella-Dorda, Santiago; Gluch, David; Hudak, John; Lewis, Grace; & Weinstock, Charles. Model-Based Verification: Claim Creation Guidelines. CMU/SEI-2001-TN-018. Software Engineering Institute, Carnegie Mellon University. 2001. http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=5513

IEEE

Comella-Dorda. Santiago, Gluch. David, Hudak. John, Lewis. Grace, and Weinstock. Charles, "Model-Based Verification: Claim Creation Guidelines," Software Engineering Institute, Carnegie Mellon University, Pittsburgh, Pennsylvania, Technical Note CMU/SEI-2001-TN-018, 2001. http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=5513

APA

Comella-Dorda, Santiago., Gluch, David., Hudak, John., Lewis, Grace., & Weinstock, Charles. (2001). Model-Based Verification: Claim Creation Guidelines (CMU/SEI-2001-TN-018). Retrieved June 08, 2023, from the Software Engineering Institute, Carnegie Mellon University website: http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=5513

CHI

Santiago Comella-Dorda, David Gluch, John Hudak, Grace Lewis, & Charles Weinstock. Model-Based Verification: Claim Creation Guidelines (CMU/SEI-2001-TN-018). Pittsburgh, PA: Software Engineering Institute, Carnegie Mellon University, 2001. http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=5513

MLA

Comella-Dorda, Santiago., Gluch, David., Hudak, John., Lewis, Grace., & Weinstock, Charles. 2001. Model-Based Verification: Claim Creation Guidelines (Technical Report CMU/SEI-2001-TN-018). Pittsburgh: Software Engineering Institute, Carnegie Mellon University. http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=5513

BibTex

@techreport{Comella-DordaModelBasedVerification2001,
title={Model-Based Verification: Claim Creation Guidelines},
author={Santiago Comella-Dorda and David Gluch and John Hudak and Grace Lewis and Charles Weinstock},
year={2001},
number={CMU/SEI-2001-TN-018},
institution={Software Engineering Institute, Carnegie Mellon University},
address={Pittsburgh, PA},
url={http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=5513} }

Ask a question about this Technical Note

Software Engineering Institute