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.
Type de document :
Communication dans un congrès
COMPSAC 2010 : 34th Annual IEEE Computer Software and Applications Conference, Jul 2010, Seoul, South Korea. pp.425-430, 2010
https://hal.inria.fr/inria-00516164
Contributeur : Hehua Zhang
<>
Soumis le : samedi 11 septembre 2010 - 07:35:38
Dernière modification le : mardi 17 avril 2018 - 11:28:09
Document(s) archivé(s) le : dimanche 12 décembre 2010 - 02:28:10
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, 2010. 〈inria-00516164〉
