Lessons Learned Model Checking an Industrial Communications Library
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.
This report is related to the following area(s) of work:
Software ArchitectureTechnical Note
CMU/SEI-2005-TN-039
September 2005
Cite This Report
SEI:
Ivers, James; Lessons Learned Model Checking an Industrial Communications Library (CMU/SEI-2005-TN-039). Software Engineering Institute, Carnegie Mellon University, 2005. http://www.sei.cmu.edu/library/abstracts/reports/05tn039.cfm
IEEE:
J. Ivers, "Lessons Learned Model Checking an Industrial Communications Library," Software Engineering Institute, Carnegie Mellon University, Pittsburgh, Pennsylvania, Technical Note CMU/SEI-2005-TN-039, 2005. http://www.sei.cmu.edu/library/abstracts/reports/05tn039.cfm
APA:
Ivers, J., (2005). Lessons Learned Model Checking an Industrial Communications Library (CMU/SEI-2005-TN-039). Retrieved May 22, 2013, from the Software Engineering Institute, Carnegie Mellon University website: http://www.sei.cmu.edu/library/abstracts/reports/05tn039.cfm
CHI:
Ivers, James, Lessons Learned Model Checking an Industrial Communications Library (CMU/SEI-2005-TN-039). Pittsburgh, PA: Software Engineering Institute, Carnegie Mellon University, 2005. http://www.sei.cmu.edu/library/abstracts/reports/05tn039.cfm
MLA:
Ivers, J., 2005. Lessons Learned Model Checking an Industrial Communications Library (Technical Report CMU/SEI-2005-TN-039). Pittsburgh: Software Engineering Institute, Carnegie Mellon University. http://www.sei.cmu.edu/library/abstracts/reports/05tn039.cfm
Find Us Here
Share This Page
For more information
