Formalizing Timing Diagram Requirements in Discrete Duration Calculus

摘要

Several temporal logics have been proposed to formalise timing diagram requirements over hardware and embedded controllers. However, succintness and visual structure of a timing diagram are not adequately captured by their formulae [6]. Interval temporal logic QDDC is a highly succint and visual notation for specifying patterns of behaviours [15]. In this paper, we propose a practically useful notation called SeCeNL which enhances the quantifier and negation free fragment of QDDC with features of nominals and limited liveness. We show that for SeCeNL, the satisfiability and model checking problems have elementary complexity as compared to the non-elementary complexity for the full logic QDDC. Next we show that timing diagrams can be naturally, compositionally and succintly formalized in SeCeNL as compared with PSL-Sugar and MTL. We give a linear time translation from timing diagrams to SeCeNL. As our second main result, we propose a linear time translation of SeCeNL into QDDC. This allows QDDC tools such as DCVALID [15,16] and DCSynth [17] to be used for checking consistency of timing diagram requirements as well as for automatic synthesis of property monitors and controllers. We give an example of a minepump controller to illustrate our tools.