Choreography

1. Specification & Model

1.1. Expression

1.1.1. Data

1.1.2. Loop (infinite)

1.1.3. Choice Internal vs. External

1.2. Model

1.2.1. Interconnection

1.2.2. Interaction

1.3. Local Specification (Role)

1.3.1. Projection

1.3.2. Composition

1.3.3. Asynchronization

1.3.4. True Concurrency

1.4. Symbolic Execution

1.4.1. Early vs. Late Semantics

1.4.1.1. Late semanttics

1.4.2. Symbolic Execution Tree

2. Equivalence

2.1. Bisimulation

2.1.1. Strong

2.1.2. Branching

2.1.3. Weak

2.2. Trace equivalence

2.2.1. Inclusion (SAC'12)

2.2.2. Equivalence

3. Problem

3.1. Realizability

3.1.1. Definition

3.1.2. Solution

3.2. Conformance

3.2.1. Solutions

3.2.1.1. Verification (at model level)

3.2.1.2. Testing

3.2.2. Definition

3.3. Controlability

3.4. Compatibility

4. Approachs

4.1. Bottom-up

4.2. Top-down