Skip to Main content Skip to Navigation
Conference papers

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

Cited literature [20 references]  Display  Hide  Download

https://hal.inria.fr/inria-00384189
Contributor : Nicolas Stouls <>
Submitted on : Friday, April 9, 2010 - 8:31:57 AM
Last modification on : Tuesday, May 26, 2020 - 3:54:03 PM
Long-term archiving on: : Tuesday, September 14, 2010 - 5:05:28 PM

Files

spb.pdf
Files produced by the author(s)

Identifiers

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

Collections

IMAG | CNRS | 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.. Formal Specification and Development in Z and B, 4th International Conference of B and Z Users, Apr 2005, Guildford, United Kingdom. pp.299--318. ⟨inria-00384189⟩

Share

Metrics

Record views

201

Files downloads

811