Showing 1–3 of 3 results for author: Bert, D

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

Authors: Didier Bert, Marie-Laure Potet, Nicolas Stouls

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… ▽ More 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. △ Less

Submitted 9 April, 2010; originally announced April 2010.

Journal ref: Formal Specification and Development in Z and B, 4th International Conference of B and Z Users, Guildford : United Kingdom (2005)

A Fixpoint Semantics of Event Systems with and without Fairness Assumptions

Authors: Hector Ruiz Barradas, Didier Bert

Abstract: We present a fixpoint semantics of event systems. The semantics is presented in a general framework without concerns of fairness. Soundness and completeness of rules for deriving "leads-to" properties are proved in this general framework. The general framework is instantiated to minimal progress and weak fairness assumptions and similar results are obtained. We show the power of these results by… ▽ More We present a fixpoint semantics of event systems. The semantics is presented in a general framework without concerns of fairness. Soundness and completeness of rules for deriving "leads-to" properties are proved in this general framework. The general framework is instantiated to minimal progress and weak fairness assumptions and similar results are obtained. We show the power of these results by deriving sufficient conditions for "leads-to" under minimal progress proving soundness of proof obligations without reasoning over state-traces. △ Less

Submitted 21 December, 2005; originally announced December 2005.

Report number: RR 1081-L LSR 21

Proof obligations for specification and refinement of liveness properties under weak fairness

Authors: Hector Ruiz Barradas, Didier Bert

Abstract: In this report, we present a formal model of fair iteration of events for B event systems. The model is used to justify proof obligations for basic liveness properties and preservation under refinement of general liveness properties. The model of fair iteration of events uses the dovetail operator, an operator proposed by Broy and Nelson to model fair choice. The proofs are mainly founded in fix… ▽ More In this report, we present a formal model of fair iteration of events for B event systems. The model is used to justify proof obligations for basic liveness properties and preservation under refinement of general liveness properties. The model of fair iteration of events uses the dovetail operator, an operator proposed by Broy and Nelson to model fair choice. The proofs are mainly founded in fixpoint calculations of fair iteration of events and weakest precondition calculus. △ Less

Submitted 9 February, 2005; originally announced February 2005.

Report number: Rapport LSR IMAG : RR 1071-I LSR 20 ACM Class: ACM: F3.1