Skip to Main content Skip to Navigation
Conference papers

Specifying time-sensitive systems with TLA+

Hehua Zhang 1 Ming Gu 1 Xiaoyu Song 1 
1 FORMES - Formal Methods for Embedded Systems
LIAMA - Laboratoire Franco-Chinois d'Informatique, d'Automatique et de Mathématiques Appliquées, Inria Paris-Rocquencourt
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.
Document type :
Conference papers
Complete list of metadata

Cited literature [12 references]  Display  Hide  Download
Contributor : Hehua Zhang Connect 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


Publisher files allowed on an open archive


  • HAL Id : inria-00516164, version 1



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⟩



Record views


Files downloads