Domain Modeling with Event-B: An Experience with Transportation Domain

Atif Mashkoor 1 Jean-Pierre Jacquot 1 Jeanine Souquières 1
1 DEDALE - Development of specifications
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : This paper presents preliminary results of utilization of Event-B for domain modeling. The development of new urban transport systems, based on autonomous vehicles, strongly requires the formal description of land transportation domain. Certification, safety, or security, for instance, crucially depend upon formal assessment that systems meet the required properties and constraints of the domain. Though Event-B has not been designed for domain modeling, yet, it was discovered that its notions of events and non determinism are well suited to formalize a domain with many autonomous agents. Refinements and systematically constructed proof obligations work well in this context, but we also need other operations in the modeling process, such as, "abstraction leaps" which have been introduced as a part of domain specification.
Type de document :
Rapport
[Research Report] 2008
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00326253
Contributeur : Atif Mashkoor <>
Soumis le : jeudi 2 octobre 2008 - 12:24:36
Dernière modification le : jeudi 11 janvier 2018 - 06:20:08
Document(s) archivé(s) le : lundi 8 octobre 2012 - 13:50:31

Fichier

mashkoor.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00326253, version 1

Collections

Citation

Atif Mashkoor, Jean-Pierre Jacquot, Jeanine Souquières. Domain Modeling with Event-B: An Experience with Transportation Domain. [Research Report] 2008. 〈inria-00326253〉

Partager

Métriques

Consultations de la notice

97

Téléchargements de fichiers

96