MT: A Toolset for Specifying and Analyzing Real-Time Systems
NAVAL RESEARCH LAB WASHINGTON DC CENTER FOR HIGH ASSURANCE COMPUTING SYSTEMS (CHACS)
Pagination or Media Count:
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.
- Computer Programming and Software