Lessons Learned Model Checking an Industrial Communications Library
• Technical Note
Publisher
Software Engineering Institute
CMU/SEI Report Number
CMU/SEI-2005-TN-039DOI (Digital Object Identifier)
10.1184/R1/6575129.v1Topic or Tag
Abstract
Model checking is a fully automated formal verification technology that can be used to determine whether models of software satisfy behavioral requirements in such areas as safety, reliability, and security. This report explores the packaging of model checking technology in a reasoning framework. The goal of a reasoning framework is to simplify the analysis of software designs by nonexperts. This report describes the application of such a reasoning framework to the design of an industrial communications library and the problems that were found. This report also notes the tasks that were unreasonably complex or time-consuming and concludes with thoughts on techniques that could be used to develop a model checking reasoning framework that better supports use by nonexperts.
Cite This Technical Note
Ivers, J. (2005, September 1). Lessons Learned Model Checking an Industrial Communications Library. (Technical Note CMU/SEI-2005-TN-039). Retrieved December 22, 2024, from https://doi.org/10.1184/R1/6575129.v1.
@techreport{ivers_2005,
author={Ivers, James},
title={Lessons Learned Model Checking an Industrial Communications Library},
month={{Sep},
year={{2005},
number={{CMU/SEI-2005-TN-039},
howpublished={Carnegie Mellon University, Software Engineering Institute's Digital Library},
url={https://doi.org/10.1184/R1/6575129.v1},
note={Accessed: 2024-Dec-22}
}
Ivers, James. "Lessons Learned Model Checking an Industrial Communications Library." (CMU/SEI-2005-TN-039). Carnegie Mellon University, Software Engineering Institute's Digital Library. Software Engineering Institute, September 1, 2005. https://doi.org/10.1184/R1/6575129.v1.
J. Ivers, "Lessons Learned Model Checking an Industrial Communications Library," Carnegie Mellon University, Software Engineering Institute's Digital Library. Software Engineering Institute, Technical Note CMU/SEI-2005-TN-039, 1-Sep-2005 [Online]. Available: https://doi.org/10.1184/R1/6575129.v1. [Accessed: 22-Dec-2024].
Ivers, James. "Lessons Learned Model Checking an Industrial Communications Library." (Technical Note CMU/SEI-2005-TN-039). Carnegie Mellon University, Software Engineering Institute's Digital Library, Software Engineering Institute, 1 Sep. 2005. https://doi.org/10.1184/R1/6575129.v1. Accessed 22 Dec. 2024.
Ivers, James. Lessons Learned Model Checking an Industrial Communications Library. CMU/SEI-2005-TN-039. Software Engineering Institute. 2005. https://doi.org/10.1184/R1/6575129.v1