# Formalism-Driven Development: Concepts, Taxonomy, and Practice +
## 2 Preliminaries
### Communication
: _Let \(\mathfrak{C}=[\mathfrak{T}_{i}\mid\ldots\mid\mathfrak{T}_{i}]\) be a channel system over \((Var,Chan)\) with_  
\[\mathfrak{T}_{i}\triangleq\langle S,A,\hookrightarrow,I,g_{0},P,\mathcal{L} \rangle,i\in[1,n].\]  
_The transition system \(\mathfrak{T}(\mathfrak{C})\) of channel system \(\mathfrak{C}\) is the tuple_  
\[\mathfrak{T}(\mathfrak{C})\triangleq\langle S,A,\rightarrow,I,P,\mathcal{L}\rangle\]  
_where_  
* \(S=(S_{1}\times\cdots\times S_{n})\times[Var]\times[Chan]\)_;_
* \(A=\underset{i=1}{n}A_{i}\uplus\{\tau\}\) _where_ \(\tau\) _is a distinguished symbol to represent all communication actions;_
* \(I=\left\{\langle s_{1},\ldots,s_{n},\mathcal{V},\mathcal{C}_{0}\rangle\mid \forall i\in[1,n]:s_{i}\in I_{i}\wedge\mathcal{V}\models g_{0\wedge i}\right\}\)_;_
* \(P\supseteq\underset{i=1}{n}P_{i}\)_;_
* \(\mathcal{L}:S\mapsto\wp(P)\)_; and_
* \(\rightarrow\) _is defined according to different cases below._  
**Case 1** (Interleaving). : _Given action \(a\in A_{i}\),_  
\[\frac{s_{i}\overset{g\downarrow a}{\longrightarrow}s_{i}^{\prime}\wedge \mathcal{V}=g}{\langle s_{1},\ldots,s_{i},\ldots,s_{n},\mathcal{V},\mathcal{C} \rangle\overset{a}{\rightarrow}\langle s_{1},\ldots,s_{i}^{\prime},\ldots,s_ {n},\mathcal{V}^{\prime},\mathcal{C}\rangle}\]  
_where \(\mathcal{V}^{\prime}=(\underset{j\in[1,n],j\
eq i}{\bigoplus}\mathcal{V}_{j}) \oplus\mathcal{V}_{i}^{\prime}\)_  
**Case 2** (Asynchronous Message Passing). : _Let \(c\in Chan,Cap(c)>0\) be a channel._  
* _For_ \(c\)_\(\tau\)_x:_ \[\frac{s_{i}\overset{g\downarrow c\tau}{\longrightarrow}s_{i}^{\prime}\wedge \mathcal{V}\models g\wedge Len(\mathcal{C}(c))>0\wedge\mathcal{C}(c)=v_{1} \ldots v_{k}}{\langle s_{1},\ldots,s_{i},\ldots,s_{n},\mathcal{V},\mathcal{C} \rangle\overset{\tau}{\rightarrow}\langle s_{1},\ldots,s_{i}^{\prime},\ldots,s _{n},\mathcal{V}^{\prime},\mathcal{C}^{\prime}\rangle}\] _where_ \(\mathcal{V}^{\prime}=\mathcal{V}[x:v_{1}]\) _and_ \(\mathcal{C}^{\prime}=\mathcal{C}[c:v_{2}\ldots v_{k}]\)_._
* _For_ \(c\)_\(\tau\)_x_:_ \[\frac{s_{i}\overset{g\downarrow c\tau}{\longrightarrow}s_{i}^{\prime}\wedge \mathcal{V}\models g\wedge Len(\mathcal{C}(c))<Cap(c)\wedge\mathcal{C}(c)=v_{1 }\ldots v_{k}}{\langle s_{1},\ldots,s_{i},\ldots,s_{n},\mathcal{V},\mathcal{C }\rangle\overset{\tau}{\rightarrow}\langle s_{1},\ldots,s_{i}^{\prime},\ldots,s_{n},\mathcal{V},\mathcal{C}^{\prime}\rangle}\] _where_ \(\mathcal{C}^{\prime}=\mathcal{C}[c:v_{1}v_{2}\ldots v_{k}v]\)_._  
**Case 3** (Synchronous Message Passing). : _Given channel \(c\in Chan,Cap(c)=0\),_  
\[\frac{s_{i}\overset{g_{1}\downarrow c\tau_{\text{N}}}{\longrightarrow}s_{i}^ {\prime}\wedge\mathcal{V}\models g_{1}\wedge s_{j}\overset{g_{2}\downarrow c \tau_{\text{N}}}{\longrightarrow}s_{j}^{\prime}\wedge\mathcal{V}\models g_{2 }\wedge i\
eq j}{\langle s_{1},\ldots,s_{i},\ldots,s_{j},\ldots,s_{n}, \mathcal{V},\mathcal{C}\rangle\overset{\tau}{\rightarrow}\langle s_{1}, \ldots,s_{i}^{\prime},\ldots,s_{j}^{\prime},\ldots,s_{n},\mathcal{V}^{\prime}, \mathcal{C}\rangle}\]  
_where \(\mathcal{V}^{\prime}=\mathcal{V}[x:v]\)._  
The interpretation from a channel system to a transition system can be automated according to the transition system semantics of a channel system, which permits us to model a system on top of a channel system without considering the details of its underlying transition system. It is also flexible to use different models or their combinations according to concrete contexts.