Formal Techniques for Networked and Distributed Systems - Forte 2002: 22nd Ifip Wg 6.1 International Conference, Houston, Texas, Usa, November 11-14, 2002 : Proceedings

by Peled, Doron A.; Peled, Doron A.; Vardi, Moshe Y.

• ISBN13: 9783540001416
• ISBN10: 3540001417
• Format: Paperback
• Copyright: 2002-12-01
• Publisher: Springer Verlag

Summary

This book constitutes the refereed proceedings of the 22nd IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems, FORTE 2002, held in Houston, Texas, USA in November 2002.The 22 revised full papers, 2 tool papers, and 2 posters presented were carefully reviewed and selected from 61 submissions. All current aspects of formal method for distributed systems and communication protocols are addressed, in particular formal specification, testing, and verification of such systems.

Table of Contents

Encoding PAMR into (Timed) EFSMs	p. 1
Submodule Construction for Specifications with Input Assumptions and Output Guarantees	p. 17
Congruent Weak Conformance, a Partial Order among Processes	p. 34
Symmetric Symbolic Safety-Analysis of Concurrent Software with Pointer Data Structures	p. 50
A Nested Depth First Search Algorithm for Model Checking with Symmetry Reduction	p. 65
Protocol Techniques for Testing Radiotherapy Accelerators	p. 81
System Test Synthesis from UML Models of Distributed Software	p. 97
Formal Test Purposes and the Validity of Test Cases	p. 114
Use of Logic to Describe Enhanced Communications Services	p. 130
A Formal Venture into Reliable Multicast Territory	p. 146
Modelling SIP Services Using CRESS	p. 162
Verifying Reliable Data Transmission over UMTS Radio Interface with High Level Petri Nets	p. 178
Verifying Randomized Byzantine Agreement	p. 194
Automatic SAT-Compilation of Protocol Insecurity Problems via Reduction to Planning	p. 210
Visual Specifications for Modular Reasoning about Asynchronous Systems	p. 226
Bounded Model Checking for Timed Systems	p. 243
C Wolf - A Toolset for Extracting Models from C Programs	p. 260
NTIF: A General Symbolic Model for Communicating Sequential Processes with Data	p. 276
Building Tools for LOTOS Symbolic Semantics in Maude	p. 292
From States to Transitions: Improving Translation of LTL Fourmulae to Buchi Automata	p. 308
A Compositional Sweep-Line State Space Exploration Method	p. 327
On Combining the Persistent Sets Method with the Covering Steps Graph Method	p. 344
Innovative Verification Techniques Used in the Implementation of a Third-Generation 1.1GHz 64b Microprocessor	p. 360
Mechanical Translation of I/O Automation Specifications into First-Order Logic	p. 364
Verification of Event-Based Synchronization of SpecC Description Using Difference Decision Diagrams	p. 369
A Distributed Partial Order Reduction Algorithm	p. 370
Author Index	p. 371
Table of Contents provided by Blackwell. All Rights Reserved.