Skip to Main content Skip to Navigation
New interface
Conference papers

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
Abstract : In a context of certification, the relationship between formal methods and "correct" soft- ware is fuzzy. To formalists, it is the logical consistency (proof), to certification authorities, it is the appropriate fulfilment of needs and constraints of the anticipated usage (validation). We present and discuss an analysis of difficulties and solutions we encountered while writing specifications in Event-B. We propose a development process which takes into account cer- tification issues. It is still based on the refinement of functional properties as supported by Event-B. Refinement steps should be extended with sub-processes whose aims are: to refine the physical and mathematical model to cast it in a form compatible with proof tools, to check non functional and temporal constraints, and to validate the behaviour of the specification.
Document type :
Conference papers
Complete list of metadata

Cited literature [23 references]  Display  Hide  Download
Contributor : Jean-Pierre Jacquot Connect in order to contact the contributor
Submitted on : Monday, June 14, 2010 - 11:34:55 AM
Last modification on : Friday, February 26, 2021 - 3:28:07 PM
Long-term archiving on: : Friday, October 19, 2012 - 2:05:31 PM


Files produced by the author(s)


  • HAL Id : inria-00491747, version 1



Faqing Yang, Jean-Pierre Jacquot. Prouvé ? Et après ?. 10es Journées Francophones Internationales sur les Approches Formelles dans l'Assistance au Développement de Logiciels - AFADL 2010, Jun 2010, Poitiers, France. pp.133-147. ⟨inria-00491747⟩



Record views


Files downloads