Graphical Interval Logic (GIL) is a visual language for temporal reasoning that provides an intuitive notation for representing the relative ordering of events in a system and the manner in which the predicates that represent system properties change with time. The high-level constructs provided by GIL together with its visual appeal result in specifications that are easier to understand and to use than traditional temporal logics. A prototype graphical toolkit that supports the use of GIL has been implemented. It includes a graphical syntax-directed editor that enables one to construct and edit GIL formulas. The toolkit is intended for the formal specification and verification of concurrent and real-time systems. It supports a unique verification methodology in which the specifications, proofs and counterexamples are all represented pictorially. The visual interface of the toolkit and the syntax-directed editor are implemented using Garnet.
Kutty, G. et al., ``Visual tools for temporal reasoning,'' Proc. IEEE Symposium on Visual Languages, Bergen, Norway, pp. 152-159, August 1993.