GeneSyst: a Tool to Reason about Behavioral Aspects of B Event Specifications. Application to Security Properties.
Didier Bert (LSR - IMAG), Marie-Laure Potet (LSR - IMAG), Nicolas, Stouls (LSR - IMAG)
TL;DR
GeneSyst is a tool that converts B specifications into symbolic transition systems, enabling analysis of behavioral and security properties through visualization and reasoning about system refinements.
Contribution
It introduces a method and tool for building and visualizing hierarchical symbolic transition systems from B specifications, facilitating behavioral reasoning and security analysis.
Findings
Successfully applied to an electronic purse model
Enables reasoning about security properties
Supports hierarchical state decomposition
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Advanced Malware Detection Techniques · Physical Unclonable Functions (PUFs) and Hardware Security