Title :
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
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;
Conference_Titel :
Software Engineering and Knowledge Engineering, 1992. Proceedings., Fourth International Conference on
Conference_Location :
Capri
Print_ISBN :
0-8186-2830-8
DOI :
10.1109/SEKE.1992.227975
