B 2007: Formal Specification and Development in B : 7th International Conference of B Users, Besancon, France, January 7-19, 2007, Proceedings / edited by Jacques Julliand, Olga Kouchnarenko.

Format:

Book

Contributor:

Julliand, Jacques, editor.

Kouchnarenko, Olga, editor.

SpringerLink (Online service)

Series:

Computer Science (Springer-11645)

LNCS sublibrary. Programming and software engineering ; SL 2, 4355.

Programming and Software Engineering ; 4355

Language:

English

Subjects (All):

Computer programming.

Software engineering.

Computer logic.

Logic, Symbolic and mathematical.

Programming Techniques.

Software Engineering.

Logics and Meanings of Programs.

Mathematical Logic and Formal Languages.

Local Subjects:

Programming Techniques.

Software Engineering.

Logics and Meanings of Programs.

Mathematical Logic and Formal Languages.

Physical Description:

1 online resource (XIII, 297 pages).

Edition:

First edition 2006.

Contained In:

Springer eBooks

Place of Publication:

Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2006.

System Details:

text file PDF

Summary:

TheseproceedingsrecordthepaperspresentedattheSeventhInternationalC- ference of B Users (B 2007), held in the city of Besan ̧ con in the east of France. This conference was built on the success of the previous six conferences in this series, B 1996, held at the University of Nantes, France; B 1998, held at the University of Montpellier, France; ZB 2000, held at the University of York, UK; ZB 2002, held at the University of Grenoble, France; ZB 2003, held at the U- versity of Turku, Finland; ZB 2005 held at the University of Surrey, Guildford, UK. B 2007 was held in January at the University of Franche-Comt ́ e,Besan ̧ con, France, hosted by the Computer Science Department (LIFC). LIFC has always placed particular emphasis on the applicability of its research and its relati- ship with industrial partners. In this context, it created in 2003 a company called LEIRIOS Technologies, which produces an automatic test generator tool (LTG) frommodels described in the B speci?cationlanguage. Other members of LIFC work on extensions of the B method for specifying and verifying dynamic properties. All the submitted papers in these proceedings were peer reviewed by at least three reviewers drawn from the B committee, depending on the subject matter of the paper. The authorsof the papersforB 2007werefrom Australia,Canada, Finland, Germany, France, Switzerland, and the UK. The conference featured a rangeof contributions by distinguished invited speakers drawn from both ind- try and academia.

Contents:

Invited Talks

E-Voting and the Need for Rigourous Software Engineering - The Past, Present and Future

Using B Machines for Model-Based Testing of Smartcard Software

The Design of Spacecraft On-Board Software

Regular Papers

Interpreting Invariant Composition in the B Method Using the Spec# Ownership Relation: A Way to Explain and Relax B Restrictions

Chorus Angelorum

Augmenting B with Control Annotations

Justifications for the Event-B Modelling Notation

Automatic Translation from Combined B and CSP Specification to Java Programs

Symmetry Reduction for B by Permutation Flooding

Instantiation of Parameterized Data Structures for Model-Based Testing

Verification of LTL on B Event Systems

Patterns for B: Bridging Formal and Informal Development

Time Constraint Patterns for Event B Development

Modelling and Proof Analysis of Interrupt Driven Scheduling

Refinement of Statemachines Using Event B Semantics

Formal Transformation of Platform Independent Models into Platform Specific Models

Refinement of eb 3 Process Patterns into B Specifications

Security Policy Enforcement Through Refinement Process

Integration of Security Policy into System Modeling

Industrial Papers

Experiences in Using B and UML in Industrial Development

B in Large-Scale Projects: The Canarsie Line CBTC Experience

A Tool for Firewall Administration

The B-Method for the Construction of Microkernel-Based Systems

Hardware Verification and Beyond: Using B at AWE

Tool Papers

A JAG Extension for Verifying LTL Properties on B Event Systems

A Generic Flash-Based Animation Engine for ProB

BE4: The B Extensible Eclipse Editing Environment

BRAMA: A New Graphic Animation Tool for B Models

LEIRIOS Test Generator: Automated Test Generation from B Models

Meca: A Tool for Access Control Models

JML2B: Checking JML Specifications with B Machines

Invited Talk

Plug-and-Play Nondeterminacy.

Other Format:

Printed edition:

ISBN:

978-3-540-68761-0

9783540687610

Access Restriction:

Restricted for use by site license.