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. Keywords-real-time; specification; TLA+; refinement

• Type: Journal
• Year: 2010
• Where: COMPSAC
• Authors: Hehua Zhang, Ming Gu, Xiaoyu Song
• Keywords: COMPSAC 2010, Corresponding Functional Description, Pattern-based Method, Software Engineering, Specification