Abstraction and Refinement of Concurrent Programs and Formal Specification

Dominique Cansell 1 Dominique Méry 1 Christophe Tabacznyj 1
1 MODEL - MODEL (Méthodes formelles et applications)
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Formal methods allow to model systems and systems properties by providing accurate mathematical notations (type theory, set theory, . . . ). Implementations can be derived from a formal specification using methods based on refinement. Therefore, from a pragmatic industrial point of vue, the dual work based on abstraction is very important too for verifying safety critical systems, but also for addressing questions like maintenance, reverse ingineering of codes, modifications of programming language, code evolution, inspection of open codes to ensure their correctness with respect to the specification, program comprehension.
Type de document :
Communication dans un congrès
Jose Rolim et al. Workshop on Formal Methods for Parallel Programming - FMPPTA'2000, 2000, Cancun, Mexico, Springer-Verlag, 1800, pp.1037-1038, 2000, Lecture Notes in Computer Science
Liste complète des métadonnées

https://hal.inria.fr/inria-00099262
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 08:52:13
Dernière modification le : mardi 24 avril 2018 - 13:34:46

Identifiants

  • HAL Id : inria-00099262, version 1

Collections

Citation

Dominique Cansell, Dominique Méry, Christophe Tabacznyj. Abstraction and Refinement of Concurrent Programs and Formal Specification. Jose Rolim et al. Workshop on Formal Methods for Parallel Programming - FMPPTA'2000, 2000, Cancun, Mexico, Springer-Verlag, 1800, pp.1037-1038, 2000, Lecture Notes in Computer Science. 〈inria-00099262〉

Partager

Métriques

Consultations de la notice

86