B événementiel pour la modélisation du domaine: application au transport

Atif Mashkoor (1) , Jean-Pierre Jacquot (1) , Jeanine Souquières (1)

1 DEDALE - Development of specifications

Ce papier rapporte sur l'utilisation de B événementiel pour la modélisation du domaine dans le cas particulier des transports. Le développement de nouveaux systèmes de transports urbains, tels que les véhicules autonomes en libre-service, pose des problèmes difficiles d'homologation, d'acceptabilité, de sécurisation et de certification. La spécification formelle de ces systèmes comme de leur environnement (ou domaine) est incontournable. Nous rapportons les premières observations réalisées lors de la modélisation d'un domaine complexe en utilisant un langage formel non spécifiquement conçu pour cet usage. Au delà des observations techniques sur l'outillage, Rodin en l'occurrence, nous mettons en évidence des points d'ordre méthodologique, en particulier la nécessite de distinguer la notion de raffinement de celle de niveaux d'observation.

Mots clés: B événementiel; domaine du transport; propriétés; vérification

Domaines: Génie logiciel [cs.SE]

Atif Mashkoor, Jean-Pierre Jacquot, Jeanine Souquières. B événementiel pour la modélisation du domaine: application au transport. Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL'2009), Jan 2009, Toulouse, France. pp.19. ⟨inria-00326355v2⟩