Real-Time Future Interval Logic (RTFIL) is a visual logic with formulae that resemble timing diagrams. It is a dense real-time temporal logic that is based on two simple temporal primitives: interval modalities for the purely qualitative part and duration predicates for the quantitative part. We present the logic, and illustrate its use in specifying the railroad crossing example and in proving some of its properties. The logic is decidable by reduction to the emptiness problem of Timed Buchi Automata. An automated theorem prover based on this decision procedure has been implemented as part of a graphical proof environment. The proofs of the railroad crossing example have been verified using this theorem prover. An automated theorem prover and a graphical specification language greatly facilitate the task of verifying real-time proofs. This convenience apart, RTFIL is invariant under real-time stuttering and does not admit instantaneous states. These properties facilitate proof methods based on abstraction and refinement.
展开▼
