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

https://hal.inria.fr/inria-00362715
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

File

2009_rehm_simpson2slots.pdf
Files produced by the author(s)

Identifiers

  • 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. ⟨inria-00362715⟩

Share

Metrics

Record views

119

Files downloads

76