VERT-verification of real-time programs

Author

Beaven, Mike ; Elmore, Brad ; Marinescu, Dan C. ; Stansifer, Ryan

Author_Institution

Dept. of Comput. Sci., Purdue Univ., West Lafayette, IN, USA

fYear

1991

fDate

11-13 Sep 1991

Firstpage

618

Lastpage

625

Abstract

The VERT (verification of real-time programs) project is surveyed. The goal of the project is to assist the development of correct real-time programs. VERT is based on modeling concurrent programs with colored Petri nets. The investigations of the net model of the program reveal static and dynamic properties of the original program. In particular critical path analysis of the nets is used to determine if the program meets the timing constraints. Several aspects of the VERT project are addressed: translation of concurrent programs into colored Petri net models, algorithms for analysis, and visualization of net models

Keywords

Petri nets; graph colouring; parallel programming; program verification; VERT; colored Petri nets; critical path analysis; dynamic properties; modeling concurrent programs; net model; program correctness; program translation; real-time programs verification; static properties; timing constraints; visualization; Aerospace electronics; Algorithm design and analysis; Data visualization; Hardware; Industrial control; Petri nets; Probes; Real time systems; Software testing; Timing;

fLanguage

English

Publisher

ieee

Conference_Titel

Computer Software and Applications Conference, 1991. COMPSAC '91., Proceedings of the Fifteenth Annual International

Conference_Location

Tokyo

Print_ISBN

0-8186-2152-4

Type

conf

DOI

10.1109/CMPSAC.1991.170251

Filename

170251