# Formalism-Driven Development: Concepts, Taxonomy, and Practice +
## 2 Preliminaries
### Abstraction Stage
#### 3.1.2 Refinement Stage  
The _Refinement Stage_ accepts a system graph from the last iteration and produces a more detailed system graph while preserving and extending properties. According to Remark 6, a system graph can be interpreted onto a transition system. In FDD, we use both bisimulation and simulation theory [25, 26] to support the refining process. The original purposes of these techniques are generally to optimize the verification process and improve verification efficiency by compacting a model while preserving its properties. However, the _Refinement Stage_ inverses the original purpose to extend a small model into a big one while preserving its properties. A refined system graph (refinement) \(\mathfrak{S}^{\prime}\) of \(\mathfrak{S}\) is a more detailed design model that has either a strong relation \(\sim\) or a weak relation \(\preceq\) to \(\mathfrak{S}\). Relation \(\sim\) is an equivalence relation that identifies \(\mathfrak{S}\) and its refinement with the same branching structure by bisimulation. Relation \(\preceq\) is a preorder. \(\mathfrak{S}^{\prime}\preceq\mathfrak{S}\) holds if the refinement \(\mathfrak{S}^{\prime}\) can be simulated by \(\mathfrak{S}\). **Definition 13** (Bisimulation). : _Let \(\mathfrak{S}_{1}\) and \(\mathfrak{S}_{2}\) be two system graphs. With regard to their transformed transition systems \(\mathfrak{T}_{1}=\langle S_{1},A_{1},\rightarrow_{1},I_{1},P_{1},\mathcal{L}_{ 1}\rangle\) over Var\({}_{1}\) and \(\mathfrak{T}_{2}=\langle S_{2},A_{2},\rightarrow_{2},I_{2},P_{2},\mathcal{L}_{ 2}\rangle\) over Var\({}_{2}\), a bisimulation for \((\mathfrak{T}_{1},\mathfrak{T}_{2})\) is a binary relation \(R\subseteq S_{1}\times S_{2}\) such that_  
* \(\forall s_{i}\in I_{i}(\exists s_{j}\in I_{j}:(s_{i},s_{j})\in R),i,j\in[1,2], i\
eq j\)_;_
* \(\forall(s_{1},s_{2})\in R:\)__
* \(s^{\prime}_{i}\in\text{Succ}(s_{i})\implies\exists s^{\prime}_{j}\in\text{Succ }(s_{j}),i,j\in[1,2],i\
eq j,(s^{\prime}_{i},s^{\prime}_{j})\in R\)_;_  
_where \(\text{Succ}(s)=\{s^{\prime}\in S\mid s\xrightarrow{a}s^{\prime},a\in A\}\)._  
_If there exists a bisimulation \(R\) for \((\mathfrak{T}_{1},\mathfrak{T}_{2})\), then \(\mathfrak{S}_{1}\sim\mathfrak{S}_{2}\iff\mathfrak{T}_{1}\sim\mathfrak{T}_{2}\)._  
**Definition 14** (Simulation). : _Let \(\mathfrak{S}_{1}\) and \(\mathfrak{S}_{2}\) be two system graphs. With regard to their transformed transition systems \(\mathfrak{T}_{1}=\langle S_{1},A_{1},\rightarrow_{1},I_{1},P_{1},\mathcal{L}_{ 1}\rangle\) over Var\({}_{1}\) and \(\mathfrak{T}_{2}=\langle S_{2},A_{2},\rightarrow_{2},I_{2},P_{2},\mathcal{L}_{ 2}\rangle\) over Var\({}_{2}\), a simulation for \((\mathfrak{T}_{1},\mathfrak{T}_{2})\) is a binary relation \(R\subseteq S_{1}\times S_{2}\) such that_  
* \(\forall s_{i}\in I_{i}(\exists s_{j}\in I_{j}:(s_{i},s_{j})\in R),i,j\in[1,2], i\
eq j\)_;_
* \(\forall(s_{1},s_{2})\in R:\)__
* \(s^{\prime}_{1}\in\text{Succ}(s_{1})\implies\exists s^{\prime}_{2}\in\text{Succ }(s_{2}),(s^{\prime}_{1},s^{\prime}_{2})\in R\)_._ _If there exists a simulation_ \(R\) _for_ \((\mathfrak{T}_{1},\mathfrak{T}_{2})\)_, then_ \(\mathfrak{S}_{1}\preceq\mathfrak{S}_{2}\iff\mathfrak{T}_{1}\preceq\mathfrak{ T}_{2}\)_._  
**Example 3** (Refinement in Transaction Client). : _First, we assume that the system graph in Example 1 from the last iteration is the input of the current iteration. According to the gas mechanism of Ethereum, it may consume significant time for a network to reach consensus. Hence, it is helpful to provide accelerating service for the transaction client. Notably, the transaction client needs to cancel the original transaction firstly and resend a new transaction with more gas due to the immutability of the blockchain.