使用B语言的形式说明与开发/formal specification and development in B

出版时间：2006-12  出版社：广东教育出版社  作者：Julliand, Jacques; Kouchnarenko, Olga;  页数：292  

内容概要

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.

书籍目录

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 SpacecraR On-Board SoftwareRegular 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 EB3 Process Patterns into B Specifications,  Security Policy Enforcement Through Refinement Process  Integration of Security Policy into System ModelingIndustrial 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 AWETool Papers  A JAG Extension for Verifying ITI Properties on R Event Systems  ……Invited TalkAuthor Index