MT: A toolset for specifying and analyzing real-time systems

Author

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

Author_Institution

US Naval Res. Lab., Washington, DC, USA

fYear

1993

fDate

1-3 Dec 1993

Firstpage

12

Lastpage

22

Abstract

This paper introduces MT, a collection of integrated tools for specifying and analyzing real-time systems using the Modechart language. The toolset includes facilities for creating and editing Modechart specifications. Users may symbolically execute the specifications with an automatic simulation tool 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 Naval real-time system

Keywords

formal specification; programming environments; real-time systems; software tools; specification languages; systems analysis; MT; Modechart language; Modechart specifications; Naval real-time system; analysis procedures; automatic simulation tool; formal methods; integrated tools; model-checking; real-time systems; safety assertions; software component; symbolically execute; verifier; Collision avoidance; Computational modeling; Error correction; FAA; Laboratories; Programming; Real time systems; Software engineering; Software safety; Timing;

fLanguage

English

Publisher

ieee

Conference_Titel

Real-Time Systems Symposium, 1993., Proceedings.

Conference_Location

Raleigh Durham, NC

Print_ISBN

0-8186-4480-X

Type

conf

DOI

10.1109/REAL.1993.393519

Filename

393519