A method to refine time constraints in event B framework

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 : Some software or hardware system involves time constraints. When those constraints are required to express the behaviour of the system, we need to write them in the corresponding formal model. We show in this short paper the general method used to deal with time constraints with a simple application example. This applies for event B formal method which does not have specific notions for time and uses the refinement to introduce it.
Type de document :
Communication dans un congrès
Stephan Merz and Tobias Nipkow. Automatic Verification of Critical Systems - AVoCS 2006, Sep 2006, Nancy/France, pp.173-177, 2006, Automatic Verification of Critical Systems (AVoCS 2006)
Liste complète des métadonnées

Littérature citée [2 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00091665
Contributeur : Stephan Merz <>
Soumis le : mercredi 6 septembre 2006 - 19:25:29
Dernière modification le : jeudi 11 janvier 2018 - 06:19:52
Document(s) archivé(s) le : jeudi 20 septembre 2012 - 10:21:11

Fichier

Identifiants

  • HAL Id : inria-00091665, version 1

Collections

Citation

Joris Rehm. A method to refine time constraints in event B framework. Stephan Merz and Tobias Nipkow. Automatic Verification of Critical Systems - AVoCS 2006, Sep 2006, Nancy/France, pp.173-177, 2006, Automatic Verification of Critical Systems (AVoCS 2006). 〈inria-00091665〉

Partager

Métriques

Consultations de la notice

219

Téléchargements de fichiers

155