Prouvé ? Et après ?

Faqing Yang 1 Jean-Pierre Jacquot 1
1 DEDALE - Development of specifications
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Résumé : Dans un contexte de certification, la relation entre méthodes formelles et logiciel " correct " n'est pas claire. Pour le formaliste, c'est la cohérence lo- gique (preuve), pour le certificateur, c'est la bonne adéquation aux besoins et contraintes de l'usage prévu (validation). Nous présentons et discutons une ana- lyse des difficultés et de leur résolution que nous avons rencontrées lors de la rédaction de spécifications en B événementiel. Nous proposons un processus de développement qui prend en compte la certification. Il est toujours fondé sur la notion de raffinement des propriétés fonctionnelles proposée par B événemen- tiel. Les étapes de raffinement doivent être complétées par des sous-processus qui raffinent le modèle physico-mathématique pour l'amener à une forme ac- ceptable par les outils de preuve, qui vérifient les contraintes non-fonctionnelles, principalement temporelles, et qui valident le comportement de la spécification.
Type de document :
Communication dans un congrès
Yamine Aït-Ameur. 10es Journées Francophones Internationales sur les Approches Formelles dans l'Assistance au Développement de Logiciels - AFADL 2010, Jun 2010, Poitiers, France. LISI/ENSMA, pp.133-147, 2010, Actes des 10es Journées Francophones sur les Approches Formelles au Développement de Logiciels
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00491747
Contributeur : Jean-Pierre Jacquot <>
Soumis le : lundi 14 juin 2010 - 11:34:55
Dernière modification le : mardi 24 avril 2018 - 13:37:33
Document(s) archivé(s) le : vendredi 19 octobre 2012 - 14:05:31

Fichier

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

Identifiants

  • HAL Id : inria-00491747, version 1

Collections

Citation

Faqing Yang, Jean-Pierre Jacquot. Prouvé ? Et après ?. Yamine Aït-Ameur. 10es Journées Francophones Internationales sur les Approches Formelles dans l'Assistance au Développement de Logiciels - AFADL 2010, Jun 2010, Poitiers, France. LISI/ENSMA, pp.133-147, 2010, Actes des 10es Journées Francophones sur les Approches Formelles au Développement de Logiciels. 〈inria-00491747〉

Partager

Métriques

Consultations de la notice

257

Téléchargements de fichiers

111