Accession Number:

ADA465119

Title:

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

Descriptive Note:

Corporate Author:

NAVAL RESEARCH LAB WASHINGTON DC CENTER FOR HIGH ASSURANCE COMPUTING SYSTEMS (CHACS)

Report Date:

1993-01-01

Pagination or Media Count:

12.0

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 toolsets 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.

Subject Categories:

  • Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE