Software Engineering Institute | Carnegie Mellon University
Software Engineering Institute | Carnegie Mellon University

Digital Library

Javascript is currently disabled for your browser. For an optimal search experience, please enable javascript.

Advanced Search

Basic Search

Content Type

Topics

Publication Date

Technical Note

Model-Based Verification: Abstraction Guidelines

  • Abstract

    Model-Based Verification (MBV) is a systematic approach to finding defects (errors) in software requirements, designs, or code. The approach judiciously incorporates mathematical formalism, in the form of models, to provide a disciplined and logical analysis practice, rather than a "proof of correctness" strategy. This technical note presents a number of abstraction techniques that can be used to build essential models of system behavior in the context of MBV and details a methodology for creating state machine models using those techniques. In building essential models, abstraction is used to hide details and expose the entities, variables, states, and transitions needed to construct a state machine model. Through illustrative examples, this technical note identifies the types of simplifications that are useful and effective and highlights the importance of the perspective in determining what are the important elements to include in an abstracted model.

  • Download

Cite This Report

SEI

Hudak, John; Comella-Dorda, Santiago; Gluch, David; Lewis, Grace; & Weinstock, Charles. Model-Based Verification: Abstraction Guidelines (CMU/SEI-2002-TN-011 ). Software Engineering Institute, Carnegie Mellon University, 2002. http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=5915

IEEE

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

APA

Hudak, John., Comella-Dorda, Santiago., Gluch, David., Lewis, Grace., & Weinstock, Charles. (2002). Model-Based Verification: Abstraction Guidelines (CMU/SEI-2002-TN-011 ). Retrieved December 26, 2014, from the Software Engineering Institute, Carnegie Mellon University website: http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=5915

CHI

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

MLA

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