Overview of ComFoRT: A Model Checking Reasoning Framework

Abstract

Component technologies are gaining acceptance in the software community as effective tools to quickly assemble increasingly complex systems from components. Most of the current component technologies, however, fail to help developers predict important software qualities like performance, safety, and reliability. A prediction-enabled component technology (PECT) augments the capabilities of a component technology with one or more reasoning frameworks that package quality-specific analyses and the means to apply them to component-based systems. Model checking is an automated approach for exhaustively analyzing whether systems satisfy specific behavioral claims that can be used to characterize safety and reliability requirements. This technical note describes ComFoRT, a reasoning framework that packages the effectiveness of state-of-the-art model checking in a form that enables users to apply the analysis technique without being experts in its use, and its incorporation in a PECT.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Apr 01, 2004
Accession Number
ADA442864

Entities

People

  • James Ivers
  • Natasha Sharygina

Organizations

  • Carnegie Mellon University

Tags

Communities of Interest

  • Autonomy

DTIC Thesaurus Topics

  • Algorithms
  • Computer Programming
  • Computer Programs
  • Computer Science
  • Computers
  • Construction
  • Engineering
  • Formal Languages
  • Language
  • Microarchitecture
  • New York
  • Operating Systems
  • Programming Languages
  • Reliability
  • Software Design
  • Software Development
  • Theoretical Computer Science

Fields of Study

  • Computer science
  • Engineering

Readers

  • Software Engineering.