Intégration de contraintes temps-réel au sein d'un processus de développement incrémental basé sur la preuve (Livrable 2)

Dominique Cansell (1) , Dominique Méry (1) , Joris Rehm (1)

1 MOSEL - Proof-oriented development of computer-based systems

The report investigates the integration of time constraintes in the refinement-based development in Event B. Specific proof-based patterns are proposed for developing models including time-oriented aspects.

Ce livrable est un rapport sur l'intégration de contraintes temporelles dans les modèles Event-B. Nous entendons par contraintes temporelles, les propriétés que possède, ou que l'on veut imposer à, un système, par rapport à son déroulement dans le temps. On parle aussi de propriétés temps- réel. Les systèmes seront en particulier des systèmes distribués, en effet : mis à part une mesure de la performance, les propriétés temps-réel ne sont utiles que si l'on s'intéresse à un ensemble de systèmes fonctionnant de manière concurrente ou distribuée. Nous allons donc étudier des systèmes dynamiques, qu'ils soient logiciels ou matériels, les définir et démontrer des propriétés, en particulier temps-réel, sur ces modèles.

Mots clés: real-time; model; refinement; proof-based patterns

Domaines: Informatique et langage [cs.CL]

Dominique Cansell, Dominique Méry, Joris Rehm. Intégration de contraintes temps-réel au sein d'un processus de développement incrémental basé sur la preuve (Livrable 2). [Rapport de recherche] 2008. ⟨inria-00593372⟩