GeneSyst: a Tool to Reason about Behavioral Aspects of B Event Specifications. Application to Security Properties.

Abstract : In this paper, we present a method and a tool to build symbolic labelled transition systems from B specifications. The tool, called GeneSyst, can take into account refinement levels and can visualize the decomposition of abstract states in concrete hierarchical states. The resulting symbolic transition system represents all the behaviors of the initial B event system. So, it can be used to reason about them. We illustrate the use of GeneSyst to check security properties on a model of electronic purse.
Type de document :
Communication dans un congrès
H.~Treharne and S.~King and M.~C.~Henson and S.~A.~Schneider. Formal Specification and Development in Z and B, 4th International Conference of B and Z Users, Apr 2005, Guildford, United Kingdom. Springer-Verlag, 3455, pp.299--318, 2005, Lecture Notes in Computer Science
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-00384189
Contributeur : Nicolas Stouls <>
Soumis le : vendredi 9 avril 2010 - 08:31:57
Dernière modification le : jeudi 11 janvier 2018 - 06:14:33
Document(s) archivé(s) le : mardi 14 septembre 2010 - 17:05:28

Fichiers

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

Identifiants

  • HAL Id : inria-00384189, version 1
  • ARXIV : 1004.1472

Collections

IMAG | UGA

Citation

Didier Bert, Marie-Laure Potet, Nicolas Stouls. GeneSyst: a Tool to Reason about Behavioral Aspects of B Event Specifications. Application to Security Properties.. H.~Treharne and S.~King and M.~C.~Henson and S.~A.~Schneider. Formal Specification and Development in Z and B, 4th International Conference of B and Z Users, Apr 2005, Guildford, United Kingdom. Springer-Verlag, 3455, pp.299--318, 2005, Lecture Notes in Computer Science. 〈inria-00384189〉

Partager

Métriques

Consultations de la notice

146

Téléchargements de fichiers

484