GeneSyst: A tool to reason about behavioral aspects of B event specifications. Application to security properties 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
Keywords for this software
References in zbMATH (referenced in 4 articles , 1 standard article )
Showing results 1 to 4 of 4.
- Vu, Dieu-Huong; Chiba, Yuki; Yatake, Kenro; Aoki, Toshiaki: Checking the conformance of a Promela design to its formal specification in Event-B (2015)
- Plagge, Daniel; Leuschel, Michael: Seven at one stroke: LTL model checking for high-level specifications in B, Z, CSP, and more (2010)
- Idani, Akram; Ledru, Yves: Object oriented concepts identification from formal $B$ specifications (2007)
- Bert, Didier; Potet, Marie-Laure; Stouls, Nicolas: GeneSyst: A tool to reason about behavioral aspects of B event specifications. Application to security properties (2005)