Specifying Time-Sensitive Systems with TLA+

We present a pattern-based method to express time specifications in the language TLA⁺. A real-time module RealTimeNew is introduced to encapsulate the definitions of commonly used time patterns. We present a general framework to differentiate the temporal characterizations from system functionality with time constraints. The temporal specification is concise and provably as a refinement of its corresponding functional description without time. The method ameliorates the usability of TLA⁺ in specifying and verifying time-sensitive systems. A case study is harnessed to illustrate and validate the approach.