A Timed Graphical Interval Logic

Silvano Dal Zilio (1) , Nouha Abid (1)

1 LAAS-VERTICS - Équipe Verification de Systèmes Temporisés Critiques

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.

Domaines: Systèmes embarqués; Logique en informatique [cs.LO]

Silvano Dal Zilio, Nouha Abid. A Timed Graphical Interval Logic. Rapport LAAS n° 12368. 2012. ⟨hal-01790214⟩