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.
Document type :
Conference papers
Complete list of metadatas

https://hal.inria.fr/inria-00099262
Contributor : Publications Loria <>
Submitted on : Tuesday, September 26, 2006 - 8:52:13 AM
Last modification on : Thursday, September 19, 2019 - 5:00:14 PM

Identifiers

  • HAL Id : inria-00099262, version 1

Collections

Citation

Dominique Cansell, Dominique Méry, Christophe Tabacznyj. Abstraction and Refinement of Concurrent Programs and Formal Specification. Workshop on Formal Methods for Parallel Programming - FMPPTA'2000, Dominique Méry & Beverly Sanders, 2000, Cancun, Mexico, pp.1037-1038. ⟨inria-00099262⟩

Share

Metrics

Record views

104