Pattern Based Integration of Time applied to the 2-Slots Simpson Algorithm - Inria - Institut national de recherche en sciences et technologies du numérique Access content directly
Conference Papers Year : 2009

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

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.
Fichier principal
Vignette du fichier
2009_rehm_simpson2slots.pdf (141.32 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

inria-00362715 , version 1 (19-02-2009)

Identifiers

  • HAL Id : inria-00362715 , version 1

Cite

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. ⟨inria-00362715⟩
124 View
78 Download

Share

Gmail Facebook X LinkedIn More