A graph proof procedure for real time logic

Author

Kao, Jung-Hong ; Henschen, Lawrence

Author_Institution

Dept. of Electr. Eng. & Comput. Sci., Northwestern Univ., Evanston, IL, USA

fYear

1992

fDate

15-20 Jun 1992

Firstpage

300

Lastpage

306

Abstract

Real-time logic (RTL) has been successful in specifying and verifying a class of timing requirements in real-time systems. The authors propose a graph proof procedure for RTL formulae. First, they represent the RTL formulae in a connection graph-like structure. Based on this graph, they have found some useful deduction rules and reduction rules. From some preliminary experiments, they show that their proof procedure is very efficient

Keywords

formal logic; formal specification; formal verification; inference mechanisms; real-time systems; connection graph-like structure; deduction rules; graph proof procedure; real time logic; reduction rules; specification; timing requirements; verification; Aerospace electronics; Control systems; Digital control; Industrial plants; Logic; Logic functions; Logic programming; Real time systems; Safety; Temperature; Timing;

fLanguage

English

Publisher

ieee

Conference_Titel

Software Engineering and Knowledge Engineering, 1992. Proceedings., Fourth International Conference on

Conference_Location

Capri

Print_ISBN

0-8186-2830-8

Type

conf

DOI

10.1109/SEKE.1992.227975

Filename

227975

Link To Document

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