ZB 2000: Formal Specification and Development in Z and B: First International Conference of B and Z Users York, UK, August 29 - September 2, 2000 Proceedings (Lecture Notes in Computer Science (1878))

This Book Constitutes The Refereed Proceedings Of The First International Conference Of B And Z Users, Zb 2000, Held In York, Uk In August/september 2000. The 25 Revised Full Papers Presented Together With Four Invited Contributions Were Carefully Reviewed And Selected For Inclusion In The Book. The Book Documents The Recent Advances For The Z Formal Specification Notion And For The B Method; The Full Scope, Ranging From Foundational And Theoretical Issues To Advanced Applications, Tools, And Case Studies, Is Covered. Meeting The Challenge Of Object-oriented Programming -- A Formal Mapping Between Uml Models And Object-z Specifications -- A Generic Process To Refine A B Specification Into A Relational Database Implementation -- Recursive Schema Definitions In Object-z -- On Mutually Recursive Free Types In Z -- Reasoning Inductively About Z Specifications Via Unification -- Reconciling Axiomatic And Model-based Specifications Using The B Method -- Compositional Structuring In The B-method: A Logical Viewpoint Of The Static Context -- Automatic Construction Of Validated B Components From Structured Developments -- Playing With Abstraction And Refinement For Managing Features Interactions -- A Formal Architecture For The 3apl Agent Programming Language -- How To Drive A B Machine -- Deriving Software Specifications From Event Based Models -- Reformulate Dynamic Properties During B Refinement And Forget Variants And Loop Invariants -- Type-constrained Generics For Z -- Typechecking Z -- Guards, Preconditions, And Refinement In Z -- Retrenchment, Refinement, And Simulation -- Performing Algorithmic Refinement Before Data Refinement In B -- Program Development And Specification Refinement In The Schema Calculus -- Are Smart Cards The Ideal Domain For Applying Formal Methods -- Formal Methods For Industrial Products -- An Execution Architecture For Gsl -- A Computation Model For Z Based On Concurrent Constraint Resolution -- Analysis Of Compiled Code: A Prototype Formal Model -- Zzzzzzzzzzzzzzzzzzzzzzzzzz -- Segregation With Communication -- Closure Induction In A Z-like Language -- Fuzzy Concepts And Formal Methods: A Fuzzy Logic Toolkit For Z. Edited By Gerhard Goos, Juris Hartmanis, Jan Leeuwen. ZB 2000: Formal Specification and Development in Z and B Preface Programme and Organizing Committees Table of Contents Meeting the Challenge of Object-Oriented Programming A Formal Mapping between UML Models and Object-Z Specifications Introduction UML UML Class Diagrams A Formal Definition of UML Class Constructs Object-Z A Metamodel of Object-Z A Formal Description for the Object-Z Metamodel The Semantics of Object-Z The semantics of attributes The Semantics of Types The Semantics of Classes The Semantics of Object-Z Specifications A Formal Mapping between UML Class Constructs and Object-Z Constructs UML Classes UML Associations UML Association Classes UML Generalizations Mapping A UML Class Diagram to an Object-Z Specification Mapping the UML Class Diagram to its Semantic Models Related Work Conclusion References A Generic Process to Refine a B Specification into a Relational Database Implementation Introduction Overview of the B Refinement Process and the Relational Model Overview of the B Re Overview of the Relational Model Description of our Approach From UML Class Diagrams to B Speci cations Refinement of B Specifications into Relational Database Implementations Related Work Refinement Rules Transition to the First Normal Form From an Object-Based Model to a Value-based Model Transformation of Associations Extension of Partial Functions From a Functional Representation to a Set Representation Mapping into SQL Tables Description of the Mapping Discussion Proof of the Re Conclusions and Future Works References Recursive Schema Definitions in Object-Z Introduction Recursion in Object-Z Fixed Point Definitions Initial State Schemas Operation Schemas Interpreting Recursive Definitions Initial State Schemas Operation Schemas Tree Example Revisited Initial State Schema Insert Operation Conclusion References On Mutually Recursive Free Types in Z Introduction Traditional Free Types Example Free Types General Form of a Free Type Constraints Abbreviated by a Free Type Finiteness Consistency of Constraints Formulation as Inference Rules Use of Inference Rules in an Example Proof Single Disjointness Constraint Mutually Recursive Free Types Example General Form Constraints Constraints for the Example Consistency An Inductive Proof Involving the Example A Second Example of Mutual Recursion Conclusions References Reasoning Inductively about Z Specifications via Unification Motivation Z and the {sf CADi${@mathbb Z}$} Proof System Unification in {sf CADi${@mathbb Z}$} Application to Inductive Reasoning Free Types The Basic Strategy Using Syntactic Orderings Selection Strategies Conclusions References Reconciling Axiomatic and Model-Based Specifications Using the B Method Introduction Specification: Mathematical Model vs. Axiomatic Example: A Stack The Stack Axioms An Axiomatic Specification of a Stack A Model-Based Specification of a Stack Reconciling the Axiomatic and Model-Based Specifications Reconciliation through Implementation Instantiating the Abstract Constants The Reconciliation An Example with State The StackVAR Machine The StackVARSeq Machine The StackVAR Implementation A Framework Reasoning about Operations Summary References Compositional Structuring in the B-Method: A Logical Viewpoint of the Static Context Introduction Background: The Structuring Primitives of B Incremental Specification: The {sc includes} and {sc extends} Primitives Sharing Specification Text: The {sc uses} Primitive Reference-Only Sharing: The SEES Clause Layered Implementation: The {sc imports} Primitive Internal Consistency of Abstract Machine Specifications Logical Background Incremental Specification Extending Specifications Sharing Components Layered Implementation ({sc imports}) Conclusion References Automatic Construction of Validated B Components from Structured Developments Introduction Component, Composition and Refinement in B B-Components B Composition The proposed Tool Extraction Algorithms Component Extraction from a Direct Refinement Component Extraction through a Chain of Refinements Component Extraction from a Structured Refinement Conclusion Specification Structure Stating New Properties Calculus of Component Relations Perspectives References Playing with Abstraction and Refinement for Managing Features Interactions Introduction Feature Interaction Problem Abstract Models for Services The Refinement-As-Composition Principle Modelling CF Call Forwarding Modelling TCS Terminating Call Screening Modelling OCS Originating Call Screening Analysis of OCS and TCS Combining CF, TCS, OCS Concluding Remarks and Future Works References A Formal Architecture for the 3APL Agent Programming Language Introduction The 3APL Programming Language 3APL Types Beliefs Actions Goals, Contexts, and Front Contexts Practical Reasoning Rules 3APL Agents Agents and Mental State Initial Agent State 3APL Agent Operation Applying Practical Reasoning Rules Goal Execution Conclusions References Substitutions Application of Substitutions Composition of Substitutions Unification How to Drive a B Machine Introduction Overview of CSP The Language Semantics Specification A Simple Coupling between B and CSP Loops Developing a Control Executive Consistency of a CSP Control Executive and a B Abstract System Reviewing Divergence Freedom Conditions for Deadlock Freedom Determining Guards Using $PAIRS$ Verification of Deadlock Freedom Consistency A Coupling for Terminating Loops Extended Syntax Acceptable Deadlock Modified Condition for Deadlock Freedom Verifying Deadlock Freedom Consistency for Terminating Loops Allowing Channels in Loops Further Extended Control Syntax Preserving Consistency with New Syntax Example with Divergence and Deadlock Freedom Discussion References Deriving Software Specifications from Event Based Models Introduction Description of the Proposed Method Specifying Sequential Programs Specifying Concurrent and Distributed Systems Deriving Program Specifications from System Specifications Using the B Method and Generalized Substitutions The Flight Warning System (FWS) System Description Formal Specification of the FWS System FWS. Environment Specification: Component Specifications: Implementing the Derived Modules Conclusion References Reformulate Dynamic Properties during B Refinement and Forget Variants and Loop Invariants Introduction Some Dynamic Property Refinements Operational Description Temporal Property Expression About Refinement Reformulated Dynamic Property Verification Refinement and Dynamic Properties Weak Sufficient Conditions Strong Sufficient Conditions Tools Related and Future Works References Proofs Type-Constrained Generics for Z Introduction Implicit Instantiation - Schema Negation Type Compatibility - Schema Conjunction Syntactic Overloading - Schema Logical Operations Schema Axiomatic Definitions The scope of Generic Schemas Projection Further Schema Operations - Natural Composition Heterogeneous State Transitions Removing Decorations - Schema Precondition Schema Override Turning an Operation Schema into a Relation Schema Composition Type-Correctness and Associativity of Schema Composition Schema Piping Rules of Refinement Homogeneous State Transitions - $Delta $ and $Xi $ Homogeneous Operation Schemas - Recognising the State Schema Iteration Implementation Conclusions References Typechecking Z Introduction Types Requirements on the Typechecker Schemas Browsing Draft Standard Z Type-Constrained Generics Specification of the Typechecker Notations Type Inference Rules Type Inference System Implicit Instantiations Schemas Browsing Draft Standard Z Undecoration Expressions Type-Constrained Generics Diagnosing Type Errors Conclusions References Guards, Preconditions, and Refinement in Z Introduction Guards and Preconditions in Z Example Classical Precondition and Guarded Interpretation Refinement Combining Guards and Preconditions A Syntax for Using Generalised Guards Operations with Guards and Preconditions Regions of Before States Three Valued Interpretation Semantical Description of the Regions Meaning of Refinement Operation Refinement Rules for Operation Refinement Example Generalisation of Traditional Refinement Rules Related and Further Work Strulo's Work The $(R,A)$-Calculus Hehner and Hoare's Predicative Approach to Programming Refinement Rules for Required Non-determinism Conclusion and Future Work References Retrenchment, Refinement, and Simulation Introduction Some Inadequacies of Refinement Retrenchment Stepwise Simulation Modulated Refinement and Simulation Simple Simulable Retrenchment The Mobile Radio Example Revisited Conclusions References Performing Algorithmic Refinement before Data Refinement in B Introduction Algorithmic Refinement before Data Refinement System of Interest Case Study 1 - Development of Make_Ballot Make_Ballot - Algorithmic Refinement followed by Data Refinement Make_Ballot - Data Refinement followed by Algorithmic Refinement Case Study 2 - Development of Pre_Process C++ STL Multisets Pre_Process - Algorithmic Refinement followed by Data Refinement Pre_Process - Data Refinement before Algorithmic Refinement Dealing with Procedural Refinement in the B-Toolkit Conclusions References Program Development and Specification Refinement in the Schema Calculus Introduction A First Example The Specification The Development An Interpretation of Operation Schemas Preconditions and Postconditions Operation Schema Calculus Refinement Inequations Types and Programs An Example Using Promotion Specification Refinement Further Work and Conclusions References Are Smart Cards the Ideal Domain for Applying Formal Methods? Introduction Needs of Security and Formalism The Small and Secure System The Certification Process The Complexity is Increasing Reducing the Cost of the Test The Constraints Development Overhead Industrial Constraints Cultural Resistance Need of a Methodology Conclusions References Formal Methods for Industrial Products Introduction Overview of the Application Special Features Security Models and Proofs Segregation with Communication Modelling Consequences Segregation and Multi-promotion Modelling the Functionality Determinism Imposed Determinism Determinism and Refinement Determinism and Traces Functional and Non-functional Properties Two Security Models Differently Segregated Resulting Specification Structure Abstract Security Policy Model, SP Virtual Machine Model, VM Concrete Hardware Model, HW Resulting Proof Structure Proof Tree Proof Sizes HW has SP Segregation Property HW has SP functional properties Results Design of the Virtual Machine Identification of Communication Channels Proof Detected an Error Lessons Learned Model Structure Versus Proof Structure Presentation Providing Further Justification Elegant Mathematical Results may not Help Summary References Conjectures with fuzz Non-generic Conjectures Generic Conjectures An Execution Architecture for GSL Introduction Reversible Computation Virtual Machine Architecture, Outline ``Executing'' Non-deterministic Choice The Command Random Choice and Morgan's pGSL Abstract Command Language ACLA Details Indirect Threaded Code Multiple Code Fields Reversing Branch Instructions The ACLA Multi-tasker Evaluating the Feasibility of an Event Conclusions References A Computation Model for Z Based on Concurrent Constraint Resolution Introduction The MZ Calculus: Syntax and Informal Semantics Mapping Z to MZ Abstraction and Application Predicates Schema Calculus Types and Genericity Semantics Computation Model Domains Reduction Resolution Implementation What Can be Computed? The Positive Answer The Negative Answer (And What Can be Enhanced) Conclusion and Related Work References Analysis of Compiled Code: A Prototype Formal Model Introduction Background Program Analysis Formal Model Expressing Higher-Order Properties in Z Specification of Program Analyses Structure of the Paper Processor Model Register and Memory Model Processor State Instruction Set Instruction Execution CPU Execution Cycle Behavioural Model Discussion Basic Blocks Abstraction Introduction Representing Basic Blocks Instantaneous Basic Block Decompositions Correct Basic Block Decompositions Discussion Concluding Remarks Limitations of the Processor Model Recent Work Future Research References Zzzzzzzzzzzzzzzzzzzzzzzzzz Segregation with Communication Introduction Motivating the Problem Trace Definition of Segregation A Segregated System Using Segregation Multiple Models Multi-promotion Unwinding Theorem Multiple Models Traces from the Computational Model The Computational Model Including Initialisation and Finalisation Input--Output Traces Event Traces Mapping from State-and-Operations to Traces Multi-promotion A Reminder of Single Promotion Introducing Multi-promotion Defined Communication Channels Unwinding Theorem Strength of Segregation Property not Preserved by Refinement Conclusions References Closure Induction in a Z-Like Language Motivation A Typed Language and Its Semantics The Syntax of Expressions The Semantics of Expressions Inductive Reasoning Closure Induction Definedness Rules Conclusion Proof of the Soundness Theorem for Closure Induction References Fuzzy Concepts and Formal Methods: A Fuzzy Logic Toolkit for Z Introduction Fuzzy Sets Motivation A Possible Fuzzy Set Representation in Z The Toolkit Summary Some Basic Definitions Some Set Measures Some Set Operators Fuzziness, Set Equality and Set Inclusion Set Modifiers and Fuzzy Numbers Fuzzy Relations Range and Domain for a Fuzzy Relation Range and Domain Restrictions (and Anti-restriction) for Fuzzy Relations The {em max-min } Relational Composition Operator for Fuzzy Relations A {em Fuzzy Relational Image} for fuzzy Relations Fuzzy Functions Alternative Notation and Definitions Conclusion References Author Index