Pattern Based Integration of Time applied to the 2-Slots Simpson Algorithm

Joris Rehm 1
1 MOSEL - Proof-oriented development of computer-based systems
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Event-B is a formal method used to do model driven engineering correct by construction. We propose a pattern to integrate time in this method. This pattern integrates elements from the theory of timed automata and event-clock automata. As experimentation of our ideas, we present a case study: an algorithm for asynchronous communication from H.R. Simpson. We prove this formal development with the software tool Rodin.
Type de document :
Communication dans un congrès
Integration of Model-based Formal Methods and Tools - IM_FMT'2009 - in IFM'2009, Feb 2009, Düsseldorf, Germany. 2009
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00362715
Contributeur : Joris Rehm <>
Soumis le : jeudi 19 février 2009 - 10:30:18
Dernière modification le : jeudi 11 janvier 2018 - 06:19:52
Document(s) archivé(s) le : vendredi 12 octobre 2012 - 11:55:16

Fichier

2009_rehm_simpson2slots.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00362715, version 1

Collections

Citation

Joris Rehm. Pattern Based Integration of Time applied to the 2-Slots Simpson Algorithm. Integration of Model-based Formal Methods and Tools - IM_FMT'2009 - in IFM'2009, Feb 2009, Düsseldorf, Germany. 2009. 〈inria-00362715〉

Partager

Métriques

Consultations de la notice

183

Téléchargements de fichiers

112