1. Towards Choreography Conformance using Symbolic Execution
1.1. Introduction
1.1.1. Choreography?
1.1.2. Choreography models
1.1.2.1. Interconnection
1.1.2.2. Interaction
1.1.3. Relation Choreography - Implementation
1.1.3.1. Top-Down
1.1.3.2. Bottom-Up
1.1.3.2.1. Conformance Problem
1.1.4. Conformance Relation
1.1.4.1. Data Flow
1.1.4.2. Control Flow
1.2. Motivation Example
1.2.1. New node
1.3. Formalization
1.3.1. A Calculus Language
1.3.1.1. STS
1.3.1.2. A Process Algebra Language
1.3.2. Choreography Specification
1.3.3. Implementation Specification
1.3.3.1. Peer
1.3.3.2. System of Peers
1.4. Choreography Conformance
1.4.1. Uniform Choreography and Peer System
1.4.2. Branching Bisimulation Relation
1.4.3. Choreography Conformance
1.5. Prototype Implementation
1.6. Related Work
1.6.1. A table summarized Choreography specifications
1.6.1.1. Büchi automata
1.6.1.2. Petri Net
1.6.1.3. Process Algebra
1.6.2. Process Algebra
1.6.2.1. Data
1.6.2.2. Local View
1.6.2.3. Symbolic
1.6.3. Equivalence Relations
1.6.3.1. Bisimulation
1.6.3.1.1. Weak
1.6.3.1.2. Branching
1.6.3.2. Trace Equivalence
1.6.3.2.1. Inclusion
1.6.3.2.2. Equivalence