A Study of Practice Issues in Model-Based Verification Using the Symbolic Model Verifier (SMV)
• Technical Report
Publisher
Software Engineering Institute
CMU/SEI Report Number
CMU/SEI-98-TR-013Topic or Tag
Abstract
This report presents the results of a study on the practice issues involved in using the Symbolic Model Verifier (SMV) for model checking software systems. The case study is of a Simplex implementation: the Simplex coordinated demonstration system for reliable system upgrade. The investigation consisted of generating a system model (using both statechart and SMV notations), specifying claims (expected properties) of the system as temporal logic formulae, and checking those formulae with respect to the SMV model. The various steps involved in the modeling process are described. Examples of the claims, their results, and a description of how the SMV tool analyzed them are detailed. Key engineering decisions made during the modeling process and a work breakdown of the effort are also presented.
Cite This Technical Report
Gluch, D., & Srinivasan, G. (1998, November 1). A Study of Practice Issues in Model-Based Verification Using the Symbolic Model Verifier (SMV). (Technical Report CMU/SEI-98-TR-013). Retrieved December 22, 2024, from https://insights.sei.cmu.edu/library/a-study-of-practice-issues-in-model-based-verification-using-the-symbolic-model-verifier-smv/.
@techreport{gluch_1998,
author={Gluch, David and Srinivasan, Grama},
title={A Study of Practice Issues in Model-Based Verification Using the Symbolic Model Verifier (SMV)},
month={{Nov},
year={{1998},
number={{CMU/SEI-98-TR-013},
howpublished={Carnegie Mellon University, Software Engineering Institute's Digital Library},
url={https://insights.sei.cmu.edu/library/a-study-of-practice-issues-in-model-based-verification-using-the-symbolic-model-verifier-smv/},
note={Accessed: 2024-Dec-22}
}
Gluch, David, and Grama Srinivasan. "A Study of Practice Issues in Model-Based Verification Using the Symbolic Model Verifier (SMV)." (CMU/SEI-98-TR-013). Carnegie Mellon University, Software Engineering Institute's Digital Library. Software Engineering Institute, November 1, 1998. https://insights.sei.cmu.edu/library/a-study-of-practice-issues-in-model-based-verification-using-the-symbolic-model-verifier-smv/.
D. Gluch, and G. Srinivasan, "A Study of Practice Issues in Model-Based Verification Using the Symbolic Model Verifier (SMV)," Carnegie Mellon University, Software Engineering Institute's Digital Library. Software Engineering Institute, Technical Report CMU/SEI-98-TR-013, 1-Nov-1998 [Online]. Available: https://insights.sei.cmu.edu/library/a-study-of-practice-issues-in-model-based-verification-using-the-symbolic-model-verifier-smv/. [Accessed: 22-Dec-2024].
Gluch, David, and Grama Srinivasan. "A Study of Practice Issues in Model-Based Verification Using the Symbolic Model Verifier (SMV)." (Technical Report CMU/SEI-98-TR-013). Carnegie Mellon University, Software Engineering Institute's Digital Library, Software Engineering Institute, 1 Nov. 1998. https://insights.sei.cmu.edu/library/a-study-of-practice-issues-in-model-based-verification-using-the-symbolic-model-verifier-smv/. Accessed 22 Dec. 2024.
Gluch, David; & Srinivasan, Grama. A Study of Practice Issues in Model-Based Verification Using the Symbolic Model Verifier (SMV). CMU/SEI-98-TR-013. Software Engineering Institute. 1998. https://insights.sei.cmu.edu/library/a-study-of-practice-issues-in-model-based-verification-using-the-symbolic-model-verifier-smv/