Formal Techniques for Networked and Distributed Systems – FORTE 2008: 28th IFIP WG 6.1 International Conference Tokyo, Japan, June 10-13, 2008, Proceedings

✍ Scribed by Kenji Suzuki (editor), Teruo Higashino (editor), Keiichi Yasumoto (editor), Khaled El-Fakih (editor)

• Publisher: Springer
• Year: 2008
• Tongue: English
• Leaves: 351
• Series: Lecture Notes in Computer Science; 5048
• Category: Library

✦ Synopsis

This volume contains the proceedings of FORTE 2008, 28th IFIP WG6.1 - ternational Conference on Formal Techniques for Networked and Distributed Systems. FORTE 2008 was held at the Campus Innovation Center in Tokyo, Japan during June 10–13, 2008. FORTE denotes a series of international wo- ing conferences on formal description techniques applied to computer networks and distributed systems. The conference series started in 1981 under the name PSTV. In 1988 a second series under the name FORTE was set up. Both - ries were united to FORTE/PSTV in 1996. In 2001 the conference changed the name to its current form. Recent conferences of this long series were held in Berlin (2003), Madrid(2004), Taipei(2005), Paris(2006), and Tallinn(2007). As in the previous year, FORTE 2008 was collocated with TESTCOM/ FATES 2008: the 20th IFIP International Conference on Testing of Com- nicating Systems (TESTCOM) and the 8th International Workshop on Formal Approaches to Testing of Software (FATES). The co-location of FORTE and TESTCOM/FATES fostered the collaboration between their communities. The commonspiritofboth conferenceswasunderpinnedby jointopening andclosing sessions, invited talks, as well as joint social events.

✦ Table of Contents

Title Page
Preface
Organization
Table of Contents
Model Generation for Horn Logic with Stratified Negation
Introduction
Background and Running Example
Classical Horn Logic
Closed World Assumption
Negation-as-Failure
Definitions
Basic Concepts
Substitutions and Unifiers
Horn Logic with CWA and NAF
The Model Generation Problem
Utilizing Backwards Chaining
Simplification of Backwards Chaining
Restratification
Generating Schedules: Part 1
Eliminating the Closed World
Generating Schedules: Part 2
A Better Algorithm Using SMT
Conclusion and Future Work
Counterexample Guided Spotlight Abstraction Refinement
Introduction
Preliminaries
Dynamic Systems
Spotlight Abstraction of Dynamic Systems
Specification Logic for Dynamic Systems
Spotlight Abstraction Refinement
Evaluation
Conclusion
An Experimental Evaluation of Probabilistic Simulation
Introduction
Preliminaries
Optimization Options
Case Studies
Regular Case Studies
Randomly Generated Models
Conclusions
An SMT Approach to Bounded Reachability Analysis of Model Programs
Introduction
Model Programs
Background Theory
Variables and Values
Actions
Update Rules
Model Program Definition
Composition of Model Programs
Bounded Reachability of Model Programs
Step Formula Creation
Reachability
Array Model Programs and Quantifier Elimination
Implementation Using Z3
Experiments
Related and Future Work
Parameterized Tree Systems
Introduction
Preliminaries
Parameterized Tree Systems
Operational Semantics
Approximation
Scheme
Algorithm
Case Studies
The Tree- rbitA er Protocol
The IEEE 1394 Tree Identification Protocol
Experiments
Conclusions and Future Work
References
Adapting Petri Nets Reductions to Promela Specifications
Introduction
Petri Nets Transitions Agglomerations
Brief Petri Nets Definitions and Notations
Petri Nets Agglomerations
Simplifying Promela Model Analysis
The Promela Language
Syntactical Promela Agglomerations
Experimentations
Related Works on Syntactical Model Reductions
Conclusion
Agglomerated Petri Net Definition
Verification of a Hierarchical Generic Mutual Exclusion Algorithm
Introduction
Related Work
Our Composition Algorithm - An Informal Approach
Coordinator Algorithm
Coordinator Automaton
Our Composition Algorithm - A Formal Model
A Basic Mutual Exclusion Aware Application Modelization
Our Composition Algorithm Petri Net
Fundamental Properties
Formal Expression of Properties
Simplified Models for Mutual Exclusion Algorithms
Model Checking
Conclusion
Distributed Semantics and Implementation for Systems with Interaction and Priority
Introduction
BIP -- Basic Semantic Models
Global State Semantics
Partial State Semantics
Comparing Global and Partial State Semantics
Partial State Semantics with Oracles
Basic Definitions and Properties
Oracles
Correctness with Respect to Global State Semantics
Distributed Semantics
Implementation
Experimental Results
Conclusion
Checking Correctness of Transactional Behaviors
Introduction
Background: The Signal Calculus
Reaction Rules
LTS Semantics
The Car Repair Scenario
The Sensoria Scenario
Modeling the Car Repair Scenario
Checking Sub-transaction Isolation
Future Work
Specifying and Verifying Web Transactions
Introduction
Compensable Transaction
The Transactional Model
Behavioral Dependencies
A Case Study
Verification
Acceptable Termination States
Verifying Temporal Constraints
Related Work
Conclusion
Modelling and Analysing the Contract Net Protocol - Extension Using Coloured Petri Nets
Introduction
Contract Net Protocol - Extension
CPN Model of the Contract Net Protocol - Extension
Assumptions
Declarations
Model Structure
Model of the Auctioneers
Model of the Bidders
State Space Analysis Results
Absence of Deadlocks and Consistency in Beliefs
Absence of Livelocks and Proper Termination
Absence of Dead Code
Channel Bound
Conclusions and Future Work
Program Repair Suggestions from Graphical State-Transition Specifications
Introduction
Related Work
State Graphs
Repairs and Their Cost Estimation
Upper-Bounds for Minimum Repair Cost
Upper-Bounds from the Graph Theory
A Logic-Based Algorithm for the MCS
Techniques for Repair Suggestions with a Cost Concept
Identifying the Common Structure Between Am and As
Identifying of the Difference Between Am and As
Constructing Repair Based on the Common Structure and the Difference
Suggestions for Repairing Programs
Implementation and Experiment
Conclusion and Future Directions
Verifying Erlang Telecommunication Systems with the Process Algebra $μ$CRL
Introduction
Telecommunication System
System Infrastructure
Client Behaviour Modelling
Erlang Implementation
Functional Server Implementation
Client Implementation
Translating Our Case Study into CRL
Pre-processing
Translating the Server Component
Translating the Client Component
System Translation
Verifying the Telecommunication System with CRL
Property Verification
State Space Investigation
Conclusions and Future Work
NQSL - Formal Language and Tool Support for Network Quality-of-Service Requirements
Introduction
Related Work
Formalization of Quality-of-Service
Formalization of Network QoS Requirements
Formal QoS Mappings
The Network Quality-of-Service Specification Language
Tool Support for NQSL
Graphical NQSL Editor
NSQL Analyzer
NQSL-to-SDL Compiler
Conclusions and Future Work
Timed Mobile Ambients for Network Protocols
Introduction
Mobile Ambients with Time Constraints
Semantics
Transmission Control Protocol
Timed Mobile Ambients Behaviour
Location Bisimulation
Timed Location Bisimulation
Properties Related to the Passage of Time
Conclusion
A Specification Framework for Earth-Friendly Logistics
Introduction
Background
Example Scenario
Requirements
Basic Approach
Remarks
Specification Language for Milk-Run Truck Routes
Order Relation for Route Selection
Implementation
Route Selection Algorithm
Route Specification in RFID Tags
Early Experience
Related Work
Future Work
Conclusion
A Hierarchy of Equivalences for Probabilistic Processes
Introduction
An Overwiew of PPA
Syntax and Operational Semantics of PPA
Testing Semantics
The Reactive Model
Alternative Characterization for R
The must Reactive Equivalence
The may Reactive Equivalence
The Generative Model
The must Generative Equivalence
The Limited Generative Model
Conclusion
Multiset Bisimulations as a Common Framework for Ordinary and Probabilistic Bisimulations
Introduction
Basic Definitions
Natural Transformations and Bisimulations
$\equiv^\alpha$-simulations Through Quotients of Bisimulations
Natural Transformations and Simulations
Combining Non-determinism and Probabilistic Choices
Conclusion
Detecting Communication Protocol Security Flaws by Formal Fuzz Testing and Machine Learning
Motivation
Formal Protocol Synthesis
FSM Learning Algorithm
Partial FSM Minimization Algorithm
Fuzz Testing Strategy
Experiments and Evaluation
Conclusion
References
Using SPIN to Detect Vulnerabilities in the AACS Drive-Host Authentication Protocol
Introduction
A Formal Model for Security Protocols
Protocol Verification Using Spin
Formalization of the Protocol
Formalization of the Intruder
Formalization of the Authenticity Property
Formalization of the Authenticity Property
The Experimental Result
Formalization of the Collusion Attack
Introduction of the Collusion Attack
Formalization of the Collusion Attack
The Experimental Result
The Modified Scheme
Relevant Analysis
Conclusion
Protocol Modeling with Model Program Composition
Introduction
Model Programs
Model Program Composition
Trace Intersection
Trace Restriction
Sample Protocol
Credit Negotiation
Cancellation
Composition
Implementation and Experiences
Related Work
Conclusion
Author Index