Lessons Learned Model Checking an Industrial Communications Library

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Sep 01, 2005
Accession Number
ADA443503

Entities

People

  • James Ivers

Organizations

  • Carnegie Mellon University

Tags

Communities of Interest

  • Autonomy

DTIC Thesaurus Topics

  • Algorithms
  • Case Studies
  • Computer Programming
  • Computer Programs
  • Computer Science
  • Computers
  • Engineering
  • Language
  • Lessons Learned
  • Microarchitecture
  • New York
  • Packaging
  • Reasoning
  • Reliability
  • Software Design
  • Software Development
  • United States

Fields of Study

  • Computer science
  • Engineering

Readers

  • Software Engineering.
  • Systems Analysis and Design
  • Theoretical Analysis.