Pattern Based Integration of Time applied to the 2-Slots Simpson Algorithm
Résumé
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.
Domaines
Logique en informatique [cs.LO]
Origine : Fichiers produits par l'(les) auteur(s)
Loading...