# Formalism-Driven Development: Concepts, Taxonomy, and Practice +
## 2 Preliminaries
### Communication  
To model distributed systems, a communication model is indispensable. In this paper, we model the communication by channels. A channel is a buffer based on a queue where messages are stored and held to be processed later. Given channel \(c\), we define a set of functions to access the properties of \(c\). \(c\) has a finite capacity \(\text{Cap}(c)\in\mathbb{N}\) and a domain \(\text{Dom}(c)\). The current number of messages in \(c\) is fetched by _Len(c)_. We can manipulate contents of \(c\) by a set of operations. \(\text{Enq}(c,m)\) puts message \(m\) at the rear of the buffer, whereas \(\text{Deq}(c)\) pops an element from the front of the buffer. We introduce two actions for sending and receiving messages based on the operations of \(c\). * \(c!m\): send the message \(m\) along channel \(c\), i.e., \(\text{Enq}(c,m)\);
* \(c?x\): receive a message via channel \(c\) and variable \(x\) has value of the message, i.e., \(x:\text{Deq}(c)\). With two message-passing actions, we define the set of communication actions \(\text{Com}\) as: \(\text{Com}=\left\{c!m,c?x\mid c\in\text{C}\text{L}\text{a}\text{m},m\in\text{ Dom}(c),x\in\text{Var}\text{ with }\text{Dom}(x)\supseteq\text{Dom}(c)\right\}\), where \(\text{C}\text{a}\text{m}\) is a set of channels with typical element \(c\) and \(\text{Var}\) is a set of variables as in Definition 2. **Definition 7** (Channel System). : _A transition system with conditional transitions \(\mathfrak{T}\) over \((\text{Var},\text{C}\text{L}\text{a}\text{m})\) is a tuple_  
\[\mathfrak{T}\triangleq\langle S,A,\hookrightarrow,I,g_{0},P,\mathcal{L}\rangle\]  
_according to Definitions 2 and 3 with the only difference that \(\hookrightarrow\subseteq S\times\|\text{Var}\|\times(A\cup\text{Com})\times S\)._  
_A channel system \(\mathfrak{C}\) over \((\text{Var},\text{C}\text{L}\text{a}\text{m}),\text{Var}=\bigcup\limits_{i=1 }^{n}\text{Var}_{i}\) with \(\bigcap\limits_{i=1}^{n}\text{Var}_{i}=\emptyset\), consisting of transition systems \(\mathfrak{T}_{i}\) over \((\text{Var}_{i},\text{C}\text{L}\text{a}\text{m}),i\in[1,n]\) is defined as_  
\[\mathfrak{C}\triangleq[\mathfrak{T}_{1}\mid\dots\mid\mathfrak{T}_{n}].\]  
**Remark 4** (State Structure of a Channel System). : _Let \(\mathfrak{C}=[\mathfrak{T}_{1}\mid\dots\mid\mathfrak{T}_{n}]\) be a channel system over \((\text{Var},\text{C}\text{L}\text{a}\text{m})\). The global states \(S\) of \(\mathfrak{C}\) are tuples of the form \(\langle s_{1},\dots,s_{n},\mathcal{V},\mathcal{C}\rangle\), where_  
* \(s_{i}\in S_{i}\) _is the current state (variable evaluation) of subsystem_ \(\mathfrak{T}_{i}\)_, i.e.,_ \(s_{i}=\mathcal{V}_{i}\in[\text{Var}_{i}]\)_;_
* \(\mathcal{V}=\bigoplus\limits_{i=1}^{n}\mathcal{V}_{i}\in[\text{Var}]\) _is the current variable evaluation (state) of_ \(\mathfrak{C}\)_, i.e.,_ \(\mathcal{V}=s\in S\)_; and_
* \(\mathcal{C}\in[\text{C}\text{L}\text{a}\text{m}]\) _is the current channel evaluation._
* \(\mathcal{C}\) _is a mapping from channel_ \(c\in\text{C}\text{L}\text{a}\text{m}\) _onto a sequence_ \(\mathcal{C}(c)\in\text{Dom}(c)^{*}\) _such that_ \(\text{Len}(\mathcal{C}(c))\leqslant\text{Cap}(c)\)_, e.g.,_ \(\mathcal{C}(c)=[v_{1}v_{2}\dots v_{k}]\) _with_ \(\text{Cap}(c)\geqslant k\)_. If_ \(\text{Cap}(c)=0\)_,_ \(c\) _is a synchronous channel. Otherwise,_ \(c\) _is an asynchronous channel._  
Notably, a channel system can have a nested structure; i.e., a subsystem can also be a channel system or parallel system. If a channel system only contains one transition system with conditional transitions, it is merely a transition system with conditional transitions and channel extension. Therefore, a channel system is capable of describing the complex structures and behaviors of a distributed system. Furthermore, given a channel system, there exists an equivalent transition system  
**Definition 8** (Transition System Semantics of a Channel System).