Real-Time Animation for Formal Specification

Dominique Méry 1 Neeraj Kumar Singh 1
1 MOSEL - Proof-oriented development of computer-based systems
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : A formal specification is a mathematical description of a given system. Writing a formal specification for real-life, industrial problems is a difficult and error prone task, even for experts in formal methods. It is crucial to get the approval and feedback when domain experts have a lack of knowledge of any specification language, to avoid the cost of changing a specification at later stage of development. This paper introduces a new functional architecture, together with a direct and efficient method of using real-time data set, in a formal model without generating the legacy source code in any target language. The implemented architecture consists of six main units. These units are: Data acquisition and preprocessing unit; Feature extraction unit; Database; Graphical animations dedicated tool: Macromedia Flash; Formal model animation tool Brama plug-in to interface between Flash animation and Event-B model; and formal specification system Event-B. These units are invoked independently and allow for simple algorithms to be executed concurrently. All the units of this proposed architecture help to animate the formal model with real-time data set and offer an easy way for specifiers to build a domain specific visualization that can be used by domain experts to check whether a formal specification corresponds to their expectations.
Type de document :
Communication dans un congrès
Marc Aiguier and Francis Bretaudeau and Daniel Krob. Complex Systems Design & Management 2010, Oct 2010, Paris, France. Springer, pp.49-60, 2010, Proceedings of the First International Conference on Complex System Design & Management CSDM 2010. 〈10.1007/978-3-642-15654-0_3〉
Liste complète des métadonnées

Littérature citée [20 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00540005
Contributeur : Neeraj Kumar Singh <>
Soumis le : lundi 21 février 2011 - 17:39:35
Dernière modification le : jeudi 11 janvier 2018 - 06:23:25
Document(s) archivé(s) le : mardi 6 novembre 2012 - 14:30:33

Fichier

Animator_CSDM2010.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Dominique Méry, Neeraj Kumar Singh. Real-Time Animation for Formal Specification. Marc Aiguier and Francis Bretaudeau and Daniel Krob. Complex Systems Design & Management 2010, Oct 2010, Paris, France. Springer, pp.49-60, 2010, Proceedings of the First International Conference on Complex System Design & Management CSDM 2010. 〈10.1007/978-3-642-15654-0_3〉. 〈inria-00540005〉

Partager

Métriques

Consultations de la notice

225

Téléchargements de fichiers

639