search menu icon-carat-right cmu-wordmark

Model-Based Verification: Abstraction Guidelines

Technical Note
This 2002 report presents 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.
Publisher

Software Engineering Institute

CMU/SEI Report Number
CMU/SEI-2002-TN-011
DOI (Digital Object Identifier)
10.1184/R1/6575570.v1

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.

Cite This Technical Note

Hudak, J., Comella-Dorda, S., Gluch, D., Lewis, G., & Weinstock, C. (2002, October 1). Model-Based Verification: Abstraction Guidelines. (Technical Note CMU/SEI-2002-TN-011). Retrieved February 27, 2024, from https://doi.org/10.1184/R1/6575570.v1.

@techreport{hudak_2002,
author={Hudak, John and Comella-Dorda, Santiago and Gluch, David and Lewis, Grace and Weinstock, Charles},
title={Model-Based Verification: Abstraction Guidelines},
month={Oct},
year={2002},
number={CMU/SEI-2002-TN-011},
howpublished={Carnegie Mellon University, Software Engineering Institute's Digital Library},
url={https://doi.org/10.1184/R1/6575570.v1},
note={Accessed: 2024-Feb-27}
}

Hudak, John, Santiago Comella-Dorda, David Gluch, Grace Lewis, and Charles Weinstock. "Model-Based Verification: Abstraction Guidelines." (CMU/SEI-2002-TN-011). Carnegie Mellon University, Software Engineering Institute's Digital Library. Software Engineering Institute, October 1, 2002. https://doi.org/10.1184/R1/6575570.v1.

J. Hudak, S. Comella-Dorda, D. Gluch, G. Lewis, and C. Weinstock, "Model-Based Verification: Abstraction Guidelines," Carnegie Mellon University, Software Engineering Institute's Digital Library. Software Engineering Institute, Technical Note CMU/SEI-2002-TN-011, 1-Oct-2002 [Online]. Available: https://doi.org/10.1184/R1/6575570.v1. [Accessed: 27-Feb-2024].

Hudak, John, Santiago Comella-Dorda, David Gluch, Grace Lewis, and Charles Weinstock. "Model-Based Verification: Abstraction Guidelines." (Technical Note CMU/SEI-2002-TN-011). Carnegie Mellon University, Software Engineering Institute's Digital Library, Software Engineering Institute, 1 Oct. 2002. https://doi.org/10.1184/R1/6575570.v1. Accessed 27 Feb. 2024.

Hudak, John; Comella-Dorda, Santiago; Gluch, David; Lewis, Grace; & Weinstock, Charles. Model-Based Verification: Abstraction Guidelines. CMU/SEI-2002-TN-011. Software Engineering Institute. 2002. https://doi.org/10.1184/R1/6575570.v1