Vérification Observationnelle

Ahmed Jebali 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Résumé : Les méthodes formelles sont un moyen pour la validation des logiciels. Une étude formelle passe par une abstraction des détails d'implémentation, en modélisant les entités comme des objets dynamiques qui sont identifiés par leurs réactions à certaines actions (méthodes, messages, transitions). l'approche observationnelle est alors adaptée à ce cadre : les objets sont considérés comme égaux si dans un contexte d'observation donné ils se comportent de la même manière. Notre objectif est de construire et d'implanter cette technique de validation observationnelle. En premier lieu nous décrivons notre système d'inférence en terme de schéma d'induction et de règles de transition et nous prouvons sa correction et sa complétude réfutationnelle, puis nous exposons l'implantation de cette technique sur le prouveur SPIKE, pour finir avec quelques expérimentations. || Formal methods provide a tool for the validation of softwares. Formal study permits to do an abstraction of internal implementation details by modelling entities into dynamic objects identified by their reactions to some actions (method, message, transiti
Type de document :
Rapport
[Stage] 99-R-144 || jebali99a, 1999, 38 p
Liste complète des métadonnées

https://hal.inria.fr/inria-00099012
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 08:41:25
Dernière modification le : jeudi 11 janvier 2018 - 06:19:58

Identifiants

  • HAL Id : inria-00099012, version 1

Collections

Citation

Ahmed Jebali. Vérification Observationnelle. [Stage] 99-R-144 || jebali99a, 1999, 38 p. 〈inria-00099012〉

Partager

Métriques

Consultations de la notice

153