Title :
Implementing a verifier for real-time systems
Author :
Stuart, Douglas A.
Author_Institution :
Dept. of Comput. Sci., Texas Univ., Austin, TX, USA
Abstract :
The SARTOR project has as one of its goals the development of an environment for the development of correct real-time systems. Modechart is a specification language for real-time systems developed as part of this project. Verify4 is an implementation of a verifier for certain classes of properties of systems specified using Modechart. The author describes the program Verify4 and addresses implementation issues surrounding three of the key algorithms used in the program
Keywords :
program verification; real-time systems; specification languages; Modechart; SARTOR project; Verify4; real-time systems; specification language; verifier; Arithmetic; Assembly; Contracts; Control systems; Data flow computing; Logic; Real time systems; Scheduling; Specification languages; Timing;
Conference_Titel :
Real-Time Systems Symposium, 1990. Proceedings., 11th
Conference_Location :
Lake Buena Vista, FL
Print_ISBN :
0-8186-2112-5
DOI :
10.1109/REAL.1990.128730