When a Formal Model Rhymes with a Graphical Notation

Akram Idani 1 Nicolas Stouls 2
LIG - Laboratoire d'Informatique de Grenoble
2 DYNAMID - Dynamic Software and Distributed Systems
CITI - CITI Centre of Innovation in Telecommunications and Integration of services
Abstract : Formal methods are based on mathematical notations which allow to rigorously reason about a model and ensure its correctness by proofs and/or model-checking. Unfortunately, these notations are com- plex and often difficult to understand from a human point of view es- pecially for engineers who are not familiar with formal methods. Sev- eral research works have proposed tools to support formal models using graphical views. On the one hand, such views are useful to make for- mal documents accessible to humans, and on the other hand they ease the verification of some behavioral properties. However, links between graphical and formal models proposed by these approaches are often difficult to put into practice and depend on the targeted formal lan- guage. In this paper, we discuss these links from a practical approach and show how a behavioral description can be computed from a formal model based on two complementary paradigms: under-approximation (or animation-based) and over-approximation (or proof-based). We applied these paradigms in order to produce behavioural state/chart views from B models and we carried out an empirical study to assess the quality and relevance of these graphical representations for humans.
Type de document :
Communication dans un congrès
Human-Oriented Formal Methods 2014, Sep 2014, Grenoble, France. Springer, 2014, LNCS
Liste complète des métadonnées

Contributeur : Nicolas Stouls <>
Soumis le : lundi 1 septembre 2014 - 15:29:47
Dernière modification le : mercredi 7 février 2018 - 11:29:48


  • HAL Id : hal-01059677, version 1



Akram Idani, Nicolas Stouls. When a Formal Model Rhymes with a Graphical Notation. Human-Oriented Formal Methods 2014, Sep 2014, Grenoble, France. Springer, 2014, LNCS. 〈hal-01059677〉



Consultations de la notice