Abstract : 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.
https://hal.inria.fr/inria-00516164 Contributor : Hehua ZhangConnect in order to contact the contributor Submitted on : Saturday, September 11, 2010 - 7:35:38 AM Last modification on : Thursday, February 3, 2022 - 11:16:09 AM Long-term archiving on: : Sunday, December 12, 2010 - 2:28:10 AM
Hehua Zhang, Ming Gu, Xiaoyu Song. Specifying time-sensitive systems with TLA+. COMPSAC 2010 : 34th Annual IEEE Computer Software and Applications Conference, Jul 2010, Seoul, South Korea. pp.425-430. ⟨inria-00516164⟩