MT: A Toolset for Specifying and Analyzing Real-Time Systems

Abstract

This paper introduces MT, a collection of integrated tools for specifying and analyzing real-time systems using the Mode chart language. The toolset includes facilities for creating and editing Modechart specifications. Users may symbolically execute the specifications with an automatic simulation too! to make sure that the specified behavior is what was intended. They may also invoke a verifier that uses model-checking to determine whether the specifications imply (satisfy) any of a broad class of safety assertions. To illustrate the toolset's capabilities as well as several issues that arise when formal methods are applied to real-world systems, the paper includes specifications and analysis procedures for a software component taken from an actual Navy real-time system.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jan 01, 1993
Accession Number
ADA465119

Entities

People

  • A. T. Rose
  • B. G. Labaw
  • C. L. Heitmeyer
  • P. C. Clements

Organizations

  • United States Naval Research Laboratory

Tags

DTIC Thesaurus Topics

  • Abstracts
  • Automatic
  • Availability
  • Buildings And Structures
  • Classification
  • Computers
  • Contracts
  • Information Operations
  • Instructions
  • Language
  • Military Research
  • Monitoring
  • Observatories
  • Research Facilities
  • Simulations
  • Specifications
  • Standards

Fields of Study

  • Computer science
  • Engineering

Readers

  • Database Systems and Applications
  • Mathematical Modeling and Probability Theory.