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.
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
Liste complète des métadonnées

Littérature citée [12 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00516164
Contributeur : Hehua Zhang <>
Soumis le : samedi 11 septembre 2010 - 07:35:38
Dernière modification le : vendredi 25 mai 2018 - 12:02:06
Document(s) archivé(s) le : dimanche 12 décembre 2010 - 02:28:10

Fichier

final.pdf
Fichiers éditeurs autorisés sur une archive ouverte

Identifiants

  • HAL Id : inria-00516164, version 1

Collections

Citation

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〉

Partager

Métriques

Consultations de la notice

427

Téléchargements de fichiers

323