Circuit Generation for Verification of ESTEREL Programs

Alain Girault 1 Gérard Berry
1 BIP - Biped Robot
Inria Grenoble - Rhône-Alpes
Abstract : We propose in this paper a method that takes external Boolean variables into account for the verification of ESTEREL programs. The intermediate code that we use is a circuit that drives an action table. The circuit represents the control of the program, and the action table manipulates its external variables. The method transforms the actions into Boolean gates and registers acting on nets instead of variables. This involves encoding the input variables into the circuit and decoding output variables. This expansion method has been implemented within the \scdata\ processor and can be used in conjunction with the ESTEREL compiler.
Type de document :
Rapport
RR-3582, INRIA. 1998
Liste complète des métadonnées

https://hal.inria.fr/inria-00073099
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 11:51:40
Dernière modification le : mercredi 11 avril 2018 - 01:55:01
Document(s) archivé(s) le : dimanche 4 avril 2010 - 23:34:04

Fichiers

Identifiants

  • HAL Id : inria-00073099, version 1

Collections

Citation

Alain Girault, Gérard Berry. Circuit Generation for Verification of ESTEREL Programs. RR-3582, INRIA. 1998. 〈inria-00073099〉

Partager

Métriques

Consultations de la notice

190

Téléchargements de fichiers

163