This book presents the refereed proceedings of the 14th International Symposium on Formal Methods, FM 2006, held in Hamilton, Canada in August 2006.
The 36 revised full papers presented together with 2 invited contributions and extended abstracts of 7 invited industrial presentations were carefully reviewed and selected from 145 submissions. The papers are organized in topical sections on interactive verification, formal modelling of systems, real time, industrial experience, specification and refinement, programming languages, algebra, education, formal modelling of systems, formal aspects of java, model checking, and abstracts of invited talks from the industry day.
Author(s): Thomas A. Henzinger, Joseph Sifakis (auth.), Jayadev Misra, Tobias Nipkow, Emil Sekerinski (eds.)
Series: Lecture Notes in Computer Science 4085 : Programming and Software Engineering
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2006
Language: English
Pages: 620
Tags: Software Engineering; Logics and Meanings of Programs; Programming Languages, Compilers, Interpreters; Programming Techniques; Mathematical Logic and Formal Languages; Management of Computing and Information Systems
Front Matter....Pages -
The Embedded Systems Design Challenge....Pages 1-15
The Mondex Challenge: Machine Checked Proofs for an Electronic Purse....Pages 16-31
Interactive Verification of Medical Guidelines....Pages 32-47
Certifying Airport Security Regulations Using the Focal Environment....Pages 48-63
Proving Safety Properties of an Aircraft Landing Protocol Using I/O Automata and the PVS Theorem Prover: A Case Study....Pages 64-80
Validating the Microsoft Hypervisor....Pages 81-81
Interface Input/Output Automata....Pages 82-97
Properties of Behavioural Model Merging....Pages 98-114
Automatic Translation from Circus to Java....Pages 115-130
Quantitative Refinement and Model Checking for the Analysis of Probabilistic Systems....Pages 131-146
Modeling and Validating Distributed Embedded Real-Time Systems with VDM++....Pages 147-162
Towards Modularized Verification of Distributed Time-Triggered Systems....Pages 163-178
A Story About Formal Methods Adoption by a Railway Signaling Manufacturer....Pages 179-189
Partially Introducing Formal Methods into Object-Oriented Development: Case Studies Using a Metrics-Driven Approach....Pages 190-204
Compositional Class Refinement in Object-Z....Pages 205-220
A Proposal for Records in Event-B....Pages 221-235
Pointfree Factorization of Operation Refinement....Pages 236-251
A Formal Template Language Enabling Metaproof....Pages 252-267
Dynamic Frames: Support for Framing, Dependencies and Sharing Without Restrictions....Pages 268-283
Type-Safe Two-Level Data Transformation....Pages 284-299
Feature Algebra....Pages 300-315
Using Domain-Independent Problems for Introducing Formal Methods....Pages 316-331
Compositional Binding in Network Domains....Pages 332-347
Formal Modeling of Communication Protocols by Graph Transformation....Pages 348-363
Feature Specification and Static Analysis for Interaction Resolution....Pages 364-379
A Fully General Operational Semantics for UML 2.0 Sequence Diagrams with Potential and Mandatory Choice....Pages 380-395
Towards Automatic Exception Safety Verification....Pages 396-411
Enforcer – Efficient Failure Injection....Pages 412-427
Automated Boundary Test Generation from JML Specifications....Pages 428-443
Formal Reasoning About Non-atomic Java Card Methods in Dynamic Logic....Pages 444-459
Formal Verification of a C Compiler Front-End....Pages 460-475
A Memory Model Sensitive Checker for C#....Pages 476-491
Changing Programs Correctly: Refactoring with Specifications....Pages 492-507
Mechanical Verification of Recursive Procedures Manipulating Pointers Using Separation Logic....Pages 508-523
Model-Based Variable and Transition Orderings for Efficient Symbolic Model Checking....Pages 524-540
Exact and Approximate Strategies for Symmetry Reduction in Model Checking....Pages 541-556
Monitoring Distributed Controllers: When an Efficient LTL Algorithm on Sequences Is Needed to Model-Check Traces....Pages 557-572
PSL Model Checking and Run-Time Verification Via Testers....Pages 573-586
Formal Methods for Security: Lightweight Plug-In or New Engineering Discipline....Pages 587-591
Formal Methods in the Security Business: Exotic Flowers Thriving in an Expanding Niche....Pages 592-597
Connector-Based Software Development: Deriving Secure Protocols....Pages 598-599
Model-Based Security Engineering for Real....Pages 600-606
Cost Effective Software Engineering for Security....Pages 607-611
Formal Methods and Cryptography....Pages 612-616
Verified Software Grand Challenge....Pages 617-617
Back Matter....Pages -
