A compositional proof system for real-time systems based on explicit clock temporal logic

Author

Hooman, J. ; Kuiper, R. ; Zhou, P.

Author_Institution

Dept. of Math. & Comput. Sci., Eindhoven Univ. of Technol., Netherlands

fYear

1991

fDate

25-26 Oct 1991

Firstpage

110

Lastpage

117

Abstract

To specify timing properties of real-time systems, the authors consider explicit clock temporal logic. Programs are written in an Occam-like real-time language. A proof system is provided to formally verify that a program satisfies a specification expressed in the real-time version of temporal logic. The proof system is compositional, sound, and relatively complete

Keywords

Occam; formal specification; formal verification; real-time systems; temporal logic; Occam-like real-time language; compositional proof system; explicit clock temporal logic; formal verification; proof system; real-time systems; real-time version; timing properties; Clocks; Communication standards; Computer languages; Formal specifications; Logic programming; Mathematics; Message passing; Real time systems; Safety; Timing;

fLanguage

English

Publisher

ieee

Conference_Titel

Software Specification and Design, 1991., Proceedings of the Sixth International Workshop on

Conference_Location

Como

Print_ISBN

0-8186-2320-9

Type

conf

DOI

10.1109/IWSSD.1991.213070

Filename

213070

Link To Document

https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=3142472