B 2007: Formal Specification and Development in B: 7th International Conference of B Users, Besancon, France, January 7-19, 2007, Proceedings

by Julliand, Jacques; Kouchnarenko, Olga

• ISBN13: 9783540687603
• ISBN10: 3540687602
• Format: Paperback
• Copyright: 2007-02-03
• Publisher: Springer Verlag

Summary

This book constitutes the refereed proceedings of the 7th International Conference of B Users, B 2007, held in Besançon, France in January 2007. The 30 revised full papers presented together with 4 invited contributions were carefully reviewed and selected from numerous submissions. The topics of interest to the conference included: industrial applications and case studies using B, integration of model-based specification methods in the software development lifecycle, derivation of hardware-software architecture from model-based specifications, expressing and validating requirements through formal models, in particular verifying security policies, theoretical issues in formal development, model-based software testing, tools supporting the B method, development by composition of specifications, validation of assembly of COTS by model-based specification methods, B extensions and/or standardization.

Table of Contents

E-voting and the need for rigourous software engineering - the past, present and future	p. 1
Using B machines for model-based testing of smartcard software	p. 2
The design of spacecraft on-board software	p. 3
Interpreting invariant composition in the B method using the spec# ownership relation : a way to explain and relax B restrictions	p. 4
Chorus angelorum	p. 19
Augmenting B with control annotations	p. 34
Justifications for the event-B modelling notation	p. 49
Automatic translation from combined B and CSP specification to Java programs	p. 64
Symmetry reduction for B by permutation flooding	p. 79
Instantiation of parameterized data structures for model-based testing	p. 94
Verification of LTL on B event systems	p. 109
Patterns for B : bridging formal and informal development	p. 125
Time constraint patterns for event B development	p. 140
Modelling and proof analysis of interrupt driven scheduling	p. 155
Refinement of statemachines using event B semantics	p. 171
Formal transformation of platform independent models into platform specific models	p. 186
Refinement of EB[superscript 3] process patterns into B specifications	p. 201
Security policy enforcement through refinement process	p. 216
Integration of security policy into system modeling	p. 232
Experiences in using B and UML in industrial development	p. 248
B in large-scale projects : the canarsie line CBTC experience	p. 252
A tool for firewall administration	p. 255
The B-method for the construction of microkernel-based systems	p. 257
Hardware verification and beyond : using B at AWE	p. 260
A JAG extension for verifying LTL properties on B event systems	p. 262
A generic flash-based animation engine for ProB	p. 266
BE[superscript 4] : the B extensible eclipse editing environment	p. 270
BRAMA : a new graphic animation tool for B models	p. 274
LEIRIOS test generator : automated test generation from B models	p. 277
Meca : a tool for access control models	p. 281
JML2B : checking JML specifications with B machines	p. 285
Plug-and-play nondeterminacy	p. 289
Table of Contents provided by Blackwell. All Rights Reserved.