B 2007: Formal Specification and Development in B (eBook, PDF)

7th International Conference of B Users, Besancon, France, January 7-19, 2007, Proceedings
Redaktion: Julliand, Jacques; Kouchnarenko, Olga

• Format: PDF

Produktbeschreibung

This book constitutes the refereed proceedings of the 7th International Conference of B Users, B 2007, held in Besançon, France, January 2007. Coverage in this volume includes 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, and validating requirements through formal models.

---

Dieser Download kann aus rechtlichen Gründen nur mit Rechnungsadresse in A, B, BG, CY, CZ, D, DK, EW, E, FIN, F, GR, HR, H, IRL, I, LT, L, LR, M, NL, PL, P, R, S, SLO, SK ausgeliefert werden.

Produktdetails

• Verlag: Springer Berlin Heidelberg
• Seitenzahl: 297
• Erscheinungstermin: 12. Dezember 2006
• Englisch
• ISBN-13: 9783540687610
• Artikelnr.: 44121807

Autorenporträt

Jacques Julliand, LIFC, France / Olga Kouchnarenko, LIFC, France

Inhaltsangabe

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.