Skip to Main content Skip to Navigation
Reports

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
Document type :
Reports
Complete list of metadata

https://hal.inria.fr/inria-00099012
Contributor : Publications Loria <>
Submitted on : Tuesday, September 26, 2006 - 8:41:25 AM
Last modification on : Friday, February 26, 2021 - 3:28:06 PM

Identifiers

  • HAL Id : inria-00099012, version 1

Collections

Citation

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

Share

Metrics

Record views

167