Formal Techniques for Networked and Distributed Systems – FORTE 2004: 24th IFIP WG 6.1 International Conference, Madrid Spain, September 27-30, 2004. Proceedings

✍ Scribed by Martín Abadi, Ted Wobber (auth.), David de Frutos-Escrig, Manuel Núñez (eds.)

• Publisher: Springer-Verlag Berlin Heidelberg
• Year: 2004
• Tongue: English
• Leaves: 388
• Series: Lecture Notes in Computer Science 3235
• Edition: 1
• Category: Library

✦ Synopsis

This book constitutes the refereed proceedings of the 24th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems, FORTE 2004, held in Madrid, Spain, in September 2004.

The 20 revised full papers presented together with 3 invited papers were carefully reviewed and selected from 54 submissions. Among the topics addressed are state-based specification, distributed Java objects, UML and SDL, algorithm verification, communicating automata, design recovery, formal protocol testing, testing and model checking, distributed real-time systems, formal composition, distributed testing, automata for ACTL, symbolic state space representation, pi-calculus, concurrency, Petri nets, routing protocol verification, and intrusion detection.

✦ Table of Contents

Front Matter....Pages -
A Logical Account of NGSCB....Pages 1-12
Composing Event Constraints in State-Based Specification....Pages 13-32
Formal Description Techniques and Software Engineering: Some Reflections after 2 Decades of Research....Pages 33-42
Parameterized Models for Distributed Java Objects....Pages 43-60
Towards the Harmonisation of UML and SDL....Pages 61-78
Localizing Program Errors for Cimple Debugging....Pages 79-96
Formal Verification of a Practical Lock-Free Queue Algorithm....Pages 97-114
Formal Verification of Web Applications Modeled by Communicating Automata....Pages 115-132
Towards Design Recovery from Observations....Pages 133-149
Network Protocol System Passive Testing for Fault Management: A Backward Checking Approach....Pages 150-166
Connectivity Testing Through Model-Checking....Pages 167-184
Fault Propagation by Equation Solving....Pages 185-198
Automatic Generation of Run-Time Test Oracles for Distributed Real-Time Systems....Pages 199-212
Formal Composition of Distributed Scenarios....Pages 213-228
Conditions for Resolving Observability Problems in Distributed Testing....Pages 229-242
Integrating Formal Verification with Mur φ of Distributed Cache Coherence Protocols in FAME Multiprocessor System Design....Pages 243-258
Witness and Counterexample Automata for ACTL....Pages 259-275
A Symbolic Symbolic State Space Representation....Pages 276-291
Introducing the Iteration in sPBC....Pages 292-308
Petri Net Semantics of the Finite π -Calculus....Pages 309-325
Symbolic Diagnosis of Partially Observable Concurrent Systems....Pages 326-342
Automatized Verification of Ad Hoc Routing Protocols....Pages 343-358
A Temporal Logic Based Framework for Intrusion Detection....Pages 359-376
Back Matter....Pages -

✦ Subjects

Computer Communication Networks; Software Engineering; Logics and Meanings of Programs; Operating Systems