Formal Methods and Hybrid Real-Time Systems: Essays in Honour of Dines Bjorner and Zhou Chaochen on the Occasion of Their 70th Birthdays (Lecture Notes in Computer Science, 4700)

This Festschrift volume is published to honour both Dines Bjørner and Zhou Chaochen on the occasion of their 70th birthdays. The volume includes 25 refereed papers by leading researchers, current and former colleagues, who congregated at a celebratory symposium held in Macao, China, in the course of the International Colloquium on Theoretical Aspects of Computing, ICTAC 2007. The papers cover a broad spectrum of subjects. Title Page Foreword Preface Organization Table of Contents Models and Software Model Checking of a Distributed File Replication System Introduction File Replication A State-Based File Replication System Components Operations The Real Deal with Join Prototyping DFS-R with OCaml Modeling DFS-R with AsmL Protocol Description Test Case Generation Reconciling Trees Zing A Zing Encoding A Mountain Too High for Zing? The Zing Experience Distributed Garbage Collection Implementation Checking Vocabulary A Custom Memory Layer Thread Layering Virtualization Partial Order Reduction Experiments Conclusions From “Formal Methods” to System Modeling Introduction Nature of Software Development Models, Their Structures and Views Description Techniques, Their Structures and Views Formal Methods and Models in Software Engineering Models for Structure and Behavior in Software Engineering System Model: A Meta Model Theory of Software Criteria for a Theory of Modeling A System Meta Model A System Development Meta Model, Development Relations: Refinement Observation and Degrees of Abstraction Software Development as Modeling Tasks Scientific Foundations of Modeling in Software Development The Role of Description Techniques Practice Today: Diagrams Limitations of Diagrams From Logic to Modeling Languages and Back to Logic Formal Description Techniques Summary and Outlook References A Denotational Semantics for Handel-C Introduction The Language Syntax Behaviour Restrictions Previous and Related Work Overview of $prialt$ Semantics Semantic Framework Abstraction of Action, States and Predicates Typed Assertion Traces Trace Operators Merging Traces in Parallel Framework Summary Execution State Environments Static State Dynamic State Actions for Handel-C Fixpoints Handel-C Denotational Semantics Extending the Language Examples Conclusions and Future Work Generating Polynomial Invariants with DISCOVERER and QEPCAD Introduction Preliminaries: Theories on Semi-algebraic Systems Basic Notions Theories on Real Solution Classification A Computer Algebra Tool: DISCOVERER Semi-algebraic Transition Systems and Invariants Polynomial Invariants Generation Complexity Analysis Generating Invariants vs. Discovering Ranking Functions Conclusions and Future Work Harnessing rCOS for Tool Support —The CoCoME Experience Introduction The Basic Ideas Behind rCOS rCOS Formulation of Software Concepts Coordination Object-Orientation in rCOS Integrating rCOS Support into Model-Driven Development Process POST---The Common Modelling Example Development of POST with rCOS Enhance Industrial Tool Support: MasterCraft Concepts in MasterCraft Developing Software with Support of MasterCraft and rCOS Conclusion Automating Verification of Cooperation, Control, and Design in Traffic Applications Introduction Extending ETCS Level 3 for Rail-Road Crossings Mechanical Transmission Outer Losses Brake ETCS Control Part A Verification Methodology for Cooperating Traffic Agents Verification of the Cooperation Layer A Design Pattern for Collision Avoidance Case Study: Movement Authority Automatic Discovery of the Criticality Functions Parameterized Verification of the Cooperation Layer Parameterized Hybrid Systems Technical Approach: Differential Logic Analysis of Parameters in ETCS Protocol Phases Proving Stability of Local Control and Design Models The Drive Train Subsystem Synthesizing Lyapunov Functions Stability of the Drive Train with Continuous-Time Controller Stability of the Discretized Drive Train Stability of the Sampled-Data Drive Train Proving Safety of Local Control and Design Models Model Checking Hybrid Systems with Large Discrete State Spaces Continuous-Time Models and Verification Results Iterative Abstraction Refinement for Step-Discrete Linear Hybrid Systems Discrete-Time Modes and Verification Results Conclusion and Future Work Specifying Various Time Models with Temporal Propositional Variables in Duration Calculus Introduction Summary of Duration Calculus Syntax of Duration Calculus Semantics of Duration Calculus Specifying Substructure of Time with Temporal Propositional Letters Discrete Duration Calculus Models Specifying Sampling, Periodic Task Systems and Projection to Discrete Time Sampling Periodic Task System Hybrid States and Projection to Discrete Time Modelling Communication Protocols with Digitizing in DC Biphase Mark Protocols Verification of BMP Conclusion Relating Domain Concepts Intensionally by Ordering Connections Introduction Domain Engineering Intensional Modelling: A Proposed Method Galois Connections and Abstract Interpretation The Order of Information Flow Steps Budgets Intrinsics Formalization Operations, Resources, and Object Aspects Intrinsics Formalization Project Plans Intrinsics Formalization Mediating Ties Intrinsics Formalization The Characteristics Connection Identifying Abstract Properties Galois Predicate The Information Flow Connection Relating the Two Connections Conclusion Programmable Messaging for Electronic Government - Building a Foundation Introduction Electronic Government Example - Electronic License Service Programmable Messaging - Foundations State State Changes Messages Members Channels Messaging Example Revisited - Electronic License Service Programmable Messaging - Software Related Work Conclusions Balancing Insight and Effort: The Industrial Uptake of Formal Methods Introduction Background: VDM A Tools Viewpoint Static Analysis Features Dynamic Analysis of Formal Models Verification of Formal Models Connection to the Development Environment Past and Future for Formal Methods Tools An Educational Viewpoint Aims Content Delivery Concluding Remarks Proving Theorems About JML Classes On Linking Z and JML JML Specifications JML Type System Abstraction Mechanisms Equational Theory Nullability and Instance Cloning JML Invariants Formalising Java $HashMaps$ in Z Java $HashMap$ Design in Z Map Operations Operation Preconditions Theorems and Automation Rules Conclusions Verifying the JML Type System Strengthening JML Annotations JML to Z Z to JML Finally Specification for Testing Introduction Related Work and Outline Case Study Overview Model: $Webbo$ Linking Model to Implementation Testing Language Action Words Oracle Link Issues for Testing Problems with Test Automation Laws Laws in $Webbo$ Reality Check Testing Consistency Invariants Confidence Conditions Confidence Conditions in $Webbo$ Partial Operators Are Equalities Assignments? Guide to Implementers Boundaries Intermediate States Sequential Components Principle Conclusion and Further Work Semantics and Verification of a Language for Modelling Hardware Architectures Introduction Gezel Specifications Extracting FSMD from Programs Constructing Hardware from an FSMD The Module Concept Top-Level Modules Basic Modules Abstract Syntax of Datapaths Semantics of Datapaths Abstract Syntax for Controllers Semantics of Basic Modules Composition of Modules Abstract Syntax for Composition of Modules Semantics for Composition of Modules Representing Modules in Uppaal Main Idea of the Uppaal Representation Construction for Basic Modules --- a Sketch Construction for Composition of Modules --- A Sketch Examples: Verification of Gezel Specification First gcd-Algorithm Second gcd-Algorithm Verification of gcd-Specifications Verification of SDES Specification Results and Analysis of Verification Conclusion Gezel Specification of a gcd-Algorithm A Domain-Oriented, Model-Based Approach for Construction and Verification of Railway Control Systems Introduction Method and Toolchain -- Overview A Case Study Domain-Specific Description Generated SystemC Models From Static Domain Model to Domain-Specific Language RSL Static Domain Model Domain-Specific Language Generating Applications from Domain-Specific Descriptions Safety Requirements and Their Verification Object Code Verification Motivation Approach Common Semantic Foundations: I/O-Safe Transitions Systems IOTS Transformation Rules IOTS Semantics of the Source and Target Languages Abstraction Mappings Implementation of a Code Verifier Example Conclusion Compensable Programs Introduction Preliminaries Design Matrix Compensable Programs Primitive Commands Programming Combinators Scope Compensation Algebraic Properties Composition Exception Handler Compensation Conclusion Deriving Specifications for Systems That Are Connected to the Physical World Introduction Outline of Our Method A Micro Example Technical Tools Fault Tolerance The Sluice Gate Example The Scope of the Problem Formalising the Problem Requirement Initial Combined System Specification The Shape of the Specification of the Control System Assumptions About the Problem World Avoiding Breakage Derived Specification of the Control Machine Taking Stock Addressing Component Failures Faults in the Sluice Gate System Making the System More Robust New Equipment/Requirements Looking for “Drift” Looking at the External Equipment Transient Errors Combining Specifications Normal and Radical Design Conclusions Related Research How General Is Our Approach? Further Developments References Engineering the Development of Embedded Systems Inter Alia Embedded Real-Time Systems Abstractions and Reality Requirements Requirements, Program Specification and Design Progress: Termination Implementation Priorities A New Generation Testing Conclusions Design Verification Patterns Introduction Background Verification of Design Patters Related Work Patterns Singleton Pattern Observer Pattern Summary Conclusion On Revival of Algol-Concepts in Modern Programming and Specification Languages Introduction Formal Procedures Versus Classes and Objects Introduction to the Problem On Reasons Why Proper Understanding of Formal Algol60-Procedures and Their Static Scope Semantics Has Been so Intricate On Another Misunderstanding of Static Binding Towards Dynamic Binding Structural Simulation of Algol60-Programs with Nested and Formal Procedures by Object Oriented Java-Programs On Denesting of Algol60-Procedures and Java-Classes Algol60 and Turbo ASM Corresponding Notions and Phrases Dynamic Semantics Verification Conclusion Design in CommUnity with Extension Morphisms Introduction Motivation and Background Introducing CommUnity The Morphisms Between Designs CommUnity and Extension Morophisms Combining Regulative Superpositions with Extension Morphisms An Example Vending Machine System The Design of the Customer The Design of the Vending Machine The Extended Vending Machine System Conclusions References Symbolic Test Generation Using a Temporal Logic with Constrained Events Introduction A Temporal Logic with Constrained Events Symbolic Test Generation Case Study Conclusion Expansive-Bisimulation for Context-Free Processes Motivation BPA Processes and Operational Semantics Expansive-Bisimulation Conclusion VDM Semantics of Programming Languages: Combinators and Monads Introduction Denotational Semantics The Oxford Style Abstract Syntax Domains and Operations Denotations The VDM Style Abstract Syntax Domains and Operations Denotations The Monadic Style Domains and Operations Denotations Published VDM Semantic Descriptions Conclusion Formal Approach to Railway Applications Introduction Issues of Scheduling and Allocation Introduction Rail Net Development Timetable Generation Scheduling and Rescheduling Other Resource Planning Maintenance Planning Optimum Train Length Station Track Assignment Delay Train Management Hub Location Problem Automatic Train Control Train Dispatch Shunting and Marshalling Passenger and Freighter Information Line Capacity Issues of Train Monitoring and Control Introduction Line Direction Agreement Device Station Interlocking Signalling Level Railway Crossing Interlocking Safety and Reliability Automatic Train Control European Rail Traffic Management System (ERTMS) Discussion Services as a Paradigm of Computation The Demand for a New Paradigm of Computation Shortcomings of the Classical Paradigm Proposals to Adjust the Classical Paradigm Aspects of the New Paradigm Service-Oriented Computing and Service-Oriented Architectures The New Paradigm in Practical Applications Service-Oriented Computing Web Services Service-Oriented Architectures An Algebraic View on Services Composition of Services and ``Reasonable'' Services The Strategies of a Service Simulation and Equivalence Brokering of Services Service Nets The Motivation for Open Workflow Nets The Formal Framework of Open Workflow Nets Composition of Open Workflow Nets Partners and Fellows Open Workflow Nets with Ports Hierarchical Open Workflow Nets Analysis Techniques for Open Workflow Nets Conclusion General Notions and Notations Open Workflow Nets Author Index Cliff B. Jones, Zhiming Liu, Jim Woodcock (eds.). Papers Presented At A Symposium Held In Macao, China, Sept. 24-25, 2007 During The Course Of The International Colloquium On Theoretical Aspects Of Computing. Includes Bibliographical References And Index. Also Issued Online