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 <>
Submitted on : Thursday, February 19, 2009 - 10:30:18 AM
Last modification on : Friday, February 26, 2021 - 3:28:05 PM
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