Formal Methods and Hybrid Real-Time Systems : Essays in Honor of Dines Bjørner and Chaochen Zhou on the Occasion of Their 70th Birthdays

This Festschrift volume is published to honour both Dines Bjørner and Zhou Chaochen on the occasion of their 70th birthdays in October and November 2007. 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, from foundational and theoretical topics to algorithms and systems issues and to applications, comprising formal methods, systems modelling, hybrid and real-time systems, specification and verification, as well as interval temporal logic. Dines Bjørner is known for his many contributions to the theory and practice of formal methods for software engineering with special focus on abstraction and modelling, specification of systems and languages, and domains, requirements, and software design. Zhou Chaochen is known for his seminal contributions to the theory and practice of timed and hybrid systems. Front Matter....Pages - Models and Software Model Checking of a Distributed File Replication System....Pages 1-23 From “Formal Methods” to System Modeling....Pages 24-44 A Denotational Semantics for Handel-C....Pages 45-66 Generating Polynomial Invariants with DISCOVERER and QEPCAD....Pages 67-82 Harnessing rCOS for Tool Support —The CoCoME Experience....Pages 83-114 Automating Verification of Cooperation, Control, and Design in Traffic Applications....Pages 115-169 Specifying Various Time Models with Temporal Propositional Variables in Duration Calculus....Pages 170-187 Relating Domain Concepts Intensionally by Ordering Connections....Pages 188-216 Programmable Messaging for Electronic Government - Building a Foundation....Pages 217-236 Balancing Insight and Effort: The Industrial Uptake of Formal Methods....Pages 237-254 Proving Theorems About JML Classes....Pages 255-279 Specification for Testing....Pages 280-299 Semantics and Verification of a Language for Modelling Hardware Architectures....Pages 300-319 A Domain-Oriented, Model-Based Approach for Construction and Verification of Railway Control Systems....Pages 320-348 Compensable Programs....Pages 349-363 Deriving Specifications for Systems That Are Connected to the Physical World....Pages 364-390 Engineering the Development of Embedded Systems....Pages 391-398 Design Verification Patterns....Pages 399-413 On Revival of Algol-Concepts in Modern Programming and Specification Languages....Pages 414-434 Design in CommUnity with Extension Morphisms....Pages 435-466 Symbolic Test Generation Using a Temporal Logic with Constrained Events....Pages 467-471 Expansive-Bisimulation for Context-Free Processes....Pages 472-482 VDM Semantics of Programming Languages: Combinators and Monads....Pages 483-503 Formal Approach to Railway Applications....Pages 504-520 Services as a Paradigm of Computation....Pages 521-538 Back Matter....Pages - Two outstanding computer scientists will soon reach their 70th birthdays: Dines Bjørner was born on October 4, 1937 in Denmark and Zhou Chaochen was born on November 1, in the same year in China. To celebrate their bir- days, we present three LNCS volumes in their honour. - FormalMethodsandHybridReal-TimeSystems. EssaysinHonourofDines BjørnerandZhouChaochenontheOccasionofTheir70thBirthdays. Papers presented at a Symposium held in Macao, China, September 24-25, 2007. LNCS volume 4700. Springer 2007. - DomainModellingandtheDurationCalculus. InternationalTrainingSchool, Shanghai, China, September 10-21,2007. Advanced Lectures. LNCSvolume 4710. Springer 2007. - Theoretical Aspects of Computing - ICTAC 2007. 4th International Col- quium, Macao, China, September 26-28, 2007, Proceedings. LNCS volume 4711. Springer 2007. Dines Bjørner is known for his many contributions to the theory and pr- tice of formal methods for software engineering. He is particularly associated with two formal methods, although his in?uence is far wider. He worked with Cli? Jones and others on theVienna Development Method (VDM), initially at IBM in Vienna. Later, he was involved in producing the Rigorous Approach toIndustrial SoftwareEngineering (RAISE) formal method with tool support 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