product iamge

Formal Techniques for Networked and Distributed Systems - FORTE 2005: 25th IFIP WG 6.1 International Conference, Taipei, Taiwan, October 2-5, 2005. Proceedings

This document was uploaded by one of our users. The uploader already confirmed that they had the permission to publish it. If you are author/publisher or own the copyright of this documents, please report to us by using this DMCA report form.

Download
Search on Amazon

Simply click on the Download Book button.

Yes, Book downloads on Ebookily are 100% Free.

Sometimes the book is free on Amazon As well, so go ahead and hit "Search on Amazon"

This book constitutes the refereed proceedings of the 25th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems, FORTE 2005, held in Taipei, Taiwan, in October 2005.

The 33 revised full papers and 6 short papers presented together with 3 keynote speeches were carefully reviewed and selected from 88 submissions. The papers cover all current aspects of formal methods for distributed systems and communication protocols such as formal description techniques (MSC, UML, Use cases, . . .), semantic foundations, model-checking, SAT-based techniques, process algebrae, abstractions, protocol testing, protocol verification, network synthesis, security system analysis, network robustness, embedded systems, communication protocols, and several promising new techniques.

Author(s): Ittai Balaban, Amir Pnueli, Lenore D. Zuck (auth.), Farn Wang (eds.)
Series: Lecture Notes in Computer Science 3731 : Programming and Software Engineering
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2005

Language: English
Pages: 558
Tags: Computer Communication Networks; Software Engineering; Logics and Meanings of Programs; Operating Systems

Front Matter....Pages -
Ranking Abstraction as Companion to Predicate Abstraction....Pages 1-12
Developing High Quality Software with Formal Methods: What Else Is Needed?....Pages 13-19
A Testing Architecture for Designing High-Reliable MANET Protocols....Pages 20-23
A Composition Operator for Systems with Active and Passive Actions....Pages 24-37
A Formal Semantics of UML StateCharts by Means of Timed Petri Nets....Pages 38-52
A Hierarchy of Implementable MSC Languages....Pages 53-67
Combining Static Analysis and Model Checking for Systems Employing Commutative Functions....Pages 68-82
Fast Generic Model-Checking for Data-Based Systems....Pages 83-97
Logic and Model Checking for Hidden Markov Models....Pages 98-112
Proving ∀ μ -Calculus Properties with SAT-Based Model Checking....Pages 113-127
Ad Hoc Routing Protocol Verification Through Broadcast Abstraction....Pages 128-142
Discovering Chatter and Incompleteness in the Datagram Congestion Control Protocol....Pages 143-158
Thread Allocation Protocols for Distributed Real-Time and Embedded Systems....Pages 159-173
A Petri Net View of Mobility....Pages 174-188
Modular Verification of Petri Nets Properties: A Structure-Based Approach....Pages 189-203
An Improved Conformance Testing Method....Pages 204-218
Resolving Observability Problems in Distributed Test Architectures....Pages 219-232
Automatic Generation of Conflict-Free IPsec Policies....Pages 233-246
A Framework Based Approach for Formal Modeling and Analysis of Multi-level Attacks in Computer Networks....Pages 247-260
Model Checking for Timed Statecharts....Pages 261-274
Abstraction-Guided Model Checking Using Symbolic IDA* and Heuristic Synthesis....Pages 275-289
Modeling and Verification of Safety-Critical Systems Using Safecharts....Pages 290-304
Structure Preserving Data Abstractions for Statecharts....Pages 305-319
Amortised Bisimulations....Pages 320-334
Proof Methodologies for Behavioural Equivalence in Dpi ....Pages 335-350
Deriving Non-determinism from Conjunction and Disjunction....Pages 351-365
Abstract Operational Semantics for Use Case Maps....Pages 366-380
ArchiTRIO: A UML-Compatible Language for Architectural Description and Its Formal Semantics....Pages 381-395
Submodule Construction for Extended State Machine Models....Pages 396-410
Towards Synchronizing Linear Collaborative Objects with Operational Transformation....Pages 411-427
Designing Efficient Fail-Safe Multitolerant Systems....Pages 428-442
Hierarchical Decision Diagrams to Exploit Model Structure....Pages 443-457
Computing Subgraph Probability of Random Geometric Graphs: Quantitative Analyses of Wireless Ad Hoc Networks....Pages 458-472
Formalising Web Services....Pages 473-488
From Automata Networks to HMSCs: A Reverse Model Engineering Perspective....Pages 489-502
Properties as Processes: Their Specification and Verification....Pages 503-517
Epoch Distance of the Random Waypoint Model in Mobile Ad Hoc Networks....Pages 518-524
Automatic Partitioner for Behavior Level Distributed Logic Simulation....Pages 525-528
Expressive Completeness of an Event-Pattern Reactive Programming Language....Pages 529-532
Formalizing Interoperability Testing: Quiescence Management and Test Generation....Pages 533-537
Formal Description of Mobile IPv6 Protocol....Pages 538-541
Incremental Modeling Under Large-Scale Distributed Interaction....Pages 542-546
The Inductive Approach to Strand Space....Pages 547-552
Compositional Modelling and Verification of IPv6 Mobility....Pages 553-556
Back Matter....Pages -