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

Lessons Learned Model Checking an Industrial Communications Library

  • September 2005
  • By James Ivers
  • This 2005 report describes the application of a reasoning framework to the design of an industrial communications library and the problems that were found.
  • Software Architecture
  • Publisher: Software Engineering Institute
    CMU/SEI Report Number: CMU/SEI-2005-TN-039
  • 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.

  • Download

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://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=7549

IEEE

Ivers. James, "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://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=7549

APA

Ivers, James. (2005). Lessons Learned Model Checking an Industrial Communications Library (CMU/SEI-2005-TN-039). Retrieved September 28, 2016, from the Software Engineering Institute, Carnegie Mellon University website: http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=7549

CHI

James Ivers. Lessons Learned Model Checking an Industrial Communications Library (CMU/SEI-2005-TN-039). Pittsburgh, PA: Software Engineering Institute, Carnegie Mellon University, 2005. http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=7549

MLA

Ivers, James. 2005. Lessons Learned Model Checking an Industrial Communications Library (Technical Report CMU/SEI-2005-TN-039). Pittsburgh: Software Engineering Institute, Carnegie Mellon University. http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=7549

BibTex

@techreport{IversLessonsLearned2005,
title={Lessons Learned Model Checking an Industrial Communications Library},
author={James Ivers},
year={2005},
number={CMU/SEI-2005-TN-039},
institution={Software Engineering Institute, Carnegie Mellon University},
address={Pittsburgh, PA},
url={http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=7549} }