Creating sequential programs from Event-B models - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2010

Creating sequential programs from Event-B models

Résumé

Event-B is an emerging formal method with good tool support for various kinds of system modelling. However, the control flow in Event-B consists only of non-deterministic choice of enabled events. In many applications, notably in sequential program construction, more elaborate control flow mechanisms would be convenient. This paper explores a method, based on a scheduling language, for describing the flow of control. The aim is to be able to express schedules of events; to reason about their correctness; to create and verify patterns for introducing correct control flow. The conclusion is that using patterns, it is feasible to derive efficient sequential programs from event-based specifications in many cases.
Fichier non déposé

Dates et versions

inria-00522651 , version 1 (11-10-2010)

Identifiants

  • HAL Id : inria-00522651 , version 1

Citer

Pontus Boström. Creating sequential programs from Event-B models. Integrated Formal Methods - IFM 2010, INRIA Nancy Grand Est, Oct 2010, Nancy, France. ⟨inria-00522651⟩
18 Consultations
1 Téléchargements

Partager

Gmail Facebook X LinkedIn More