This book presents the refereed proceedings of the 15th International Symposium on Formal Methods, FM 2008, held in Turku, Finland in May 2008.
The 23 revised full papers presented together with 4 invited contributions and extended abstracts of 5 invited industrial presentations were carefully reviewed and selected from 106 submissions. The papers are organized in topical sections on programming language analysis, verification, real-time and concurrency, grand chellenge problems, fm practice, runtime monitoring and analysis, communication, constraint analysis, and design.
Author(s): Shmuel Katz (auth.), Jorge Cuellar, Tom Maibaum, Kaisa Sere (eds.)
Series: Lecture Notes in Computer Science 5014 : Programming and Software Engineering
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2008
Language: English
Pages: 436
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 -
Aspects and Formal Methods....Pages 1-11
Getting Formal Verification into Design Flow....Pages 12-32
Lessons in the Weird and Unexpected: Some Experiences from Checking Large Real Systems....Pages 33-33
Simulation, Orchestration and Logical Clocks....Pages 34-34
CoVaC: Compiler Validation by Program Analysis of the Cross-Product....Pages 35-51
Lazy Behavioral Subtyping....Pages 52-67
Checking Well-Formedness of Pure-Method Specifications....Pages 68-83
Verifying Dynamic Pointer-Manipulating Threads....Pages 84-99
Proofs and Refutations for Probabilistic Refinement....Pages 100-115
Assume-Guarantee Verification for Interface Automata....Pages 116-131
Automated Verification of Dense-Time MTL Specifications Via Discrete-Time Approximation....Pages 132-147
A Model Checking Language for Concurrent Value-Passing Systems....Pages 148-164
Verification of Mondex Electronic Purses with KIV: From a Security Protocol to Verified Code....Pages 165-180
Incremental Development of a Distributed Real-Time Model of a Cardiac Pacing System Using VDM....Pages 181-197
Industrial Use of Formal Methods for a High-Level Security Evaluation....Pages 198-213
Secret Ninja Formal Methods....Pages 214-228
Specification and Checking of Software Contracts for Conditional Information Flow....Pages 229-245
JML Runtime Assertion Checking: Improved Error Reporting and Efficiency Using Strong Validity....Pages 246-261
Provably Correct Runtime Monitoring....Pages 262-277
A Schedulerless Semantics of TLM Models Written in SystemC Via Translation into LOTOS....Pages 278-293
A Rigorous Approach to Networking: TCP, from Implementation to Protocol to Service....Pages 294-309
Constraint Prioritization for Efficient Analysis of Declarative Models....Pages 310-325
Finding Minimal Unsatisfiable Cores of Declarative Specifications....Pages 326-341
Precise Interval Analysis vs. Parity Games....Pages 342-357
Introducing Objects through Refinement....Pages 358-373
Masking Faults While Providing Bounded-Time Phased Recovery....Pages 374-389
Towards Consistent Specifications of Product Families....Pages 390-405
Formal Methods for Trustworthy Skies: Building Confidence in the Security of Aircraft Assets Distribution....Pages 406-410
An Industrial Case: Pitfalls and Benefits of Applying Formal Methods to the Development of a Network-Centric RTOS....Pages 411-418
Software Engineering with Formal Methods: Experiences with the Development of a Storm Surge Barrier Control System....Pages 419-424
Application of a Formal Specification Language in the Development of the “Mobile FeliCa” IC Chip Firmware for Embedding in Mobile Phone....Pages 425-429
Safe and Reliable Metro Platform Screen Doors Control/Command Systems....Pages 430-434
Back Matter....Pages -
