Pattern Based Integration of Time applied to the 2-Slots Simpson AlgorithmReportar como inadecuado




Pattern Based Integration of Time applied to the 2-Slots Simpson Algorithm - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

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.

Keywords : formal-method event-b real-time refinement





Autor: Joris Rehm -

Fuente: https://hal.archives-ouvertes.fr/



DESCARGAR PDF




Documentos relacionados