Service interruption on Monday 11 July from 12:30 to 13:00: all the sites of the CCSD (HAL, Epiciences, SciencesConf, AureHAL) will be inaccessible (network hardware connection).
Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata

Cited literature [9 references]  Display  Hide  Download
Contributor : Joris Rehm Connect in order to contact the contributor
Submitted on : Thursday, February 19, 2009 - 10:30:18 AM
Last modification on : Friday, February 4, 2022 - 3:30:22 AM
Long-term archiving on: : Friday, October 12, 2012 - 11:55:16 AM


Files produced by the author(s)


  • HAL Id : inria-00362715, version 1



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⟩



Record views


Files downloads