Sciweavers

B
2007
Springer
14 years 4 months ago
Security Policy Enforcement Through Refinement Process
Abstract. In the area of networks, a common method to enforce a security policy expressed in a high-level language is based on an ad-hoc and manual rewriting process [24]. We argue...
Nicolas Stouls, Marie-Laure Potet
B
2007
Springer
14 years 4 months ago
Automatic Translation from Combined B and CSP Specification to Java Programs
Abstract. A recent contribution to the formal specification and verification of concurrent systems is the integration of the state- and event-based approaches B and CSP, specifical...
Letu Yang, Michael Poppleton
B
2007
Springer
14 years 6 months ago
The B-Method for the Construction of Microkernel-Based Systems
Sarah Hoffmann, Germain Haugou, Sophie Gabriele, L...
B
2007
Springer
14 years 6 months ago
Time Constraint Patterns for Event B Development
Distributed applications are based on algorithms which should be able to deal with time constraints. It is mandatory to express time constraints in (mathematical) models and the cu...
Dominique Cansell, Dominique Méry, Joris Re...
B
2007
Springer
14 years 6 months ago
A Generic Flash-Based Animation Engine for ProB
Abstract. Writing a formal specification for real-life, industrial problems is a difficult and error prone task, even for experts in formal methods. In the process of specifying a...
Jens Bendisposto, Michael Leuschel
B
2007
Springer
14 years 6 months ago
Symmetry Reduction for B by Permutation Flooding
Symmetry reduction is an established method for limiting the amount of states that have to be checked during exhaustive model checking. The idea is to only verify a single represen...
Michael Leuschel, Michael J. Butler, Corinna Sperm...
B
2007
Springer
14 years 6 months ago
Modelling and Proof Analysis of Interrupt Driven Scheduling
Following a brief discussion of uniprocessor scheduling in which we argue the case for formal analysis, we describe a distributed Event B model of interrupt driven scheduling. We ...
Bill Stoddart, Dominique Cansell, Frank Zeyda
B
2007
Springer
14 years 6 months ago
Augmenting B with Control Annotations
Abstract. CSP B is an integration of the process algebra Communicating Sequential Processes (CSP), and the B-Method, which enables consistent controllers to be written for B machin...
Wilson Ifill, Steve A. Schneider, Helen Treharne