A Timed Graphical Interval Logic


We define a graphical language for expressing timed requirements on concurrent systems. This formal language, called Timed Graphical Interval Logic (TGIL), is inspired by realtime extensions of Dillon’s et al Graphical Interval Logic and can be used as an alternative to timed extensions of temporal logic. We define the semantics of TGIL as a set of timed traces (using a dense time semantics) and illustrate its use in formal verification by describing a method for generating an observer from a TGIL specification.

Research Report 12368, LAAS