2.1 CSP# and process analysis toolkit

The CSP# is a rich modelling language that contains both high-level modelling operators in the traditional CSP language and programmer-favoured low-level constructs like variables, arrays, if-then-else, while, etc. It offers great flexibility to model systems with complicated structures, like blockchain. A system is modelled as a process in CSP#, where the operators in CSP# are defined as follows (in Figure 1).

The deadlock process is Stop, meaning that the process does absolutely nothing. Process Skip means that the process terminates immediately. Process [b]P is a guarded process—the process behaves as P if b is satisfied. Process ${ e \rightarrow P }$ is event prefixing—the process performs event e (a simple event is a name for representing an observation) and then behaves as P. Process ${e \{program\} \rightarrow P}$ is similar to event prefixing. The difference is that the $\{{program\}}$ attached with event e allows us to write assignments which update global variables. Process ${c?d \rightarrow P(d)}$ is channel input—the process reads a value d from channel c, thus d is known in the subsequent process P. Process ${c!d \rightarrow P}$ is channel output—the process outputs value d in channel c. Process ${P; Q}$ concatenates two processes P and Q sequentially. Process ${P \sqcap Q}$ is internal choice—the process chooses either P or Q to execute. If P performs an event first, then P takes control; otherwise Q takes control. Process ${P \square Q}$ is external choice. Differing from the internal choice, the external choice is resolved by the environment. Process ${if\ b\ then\ P\ else\ Q}$ is straightforward: if b is true, the process behaves as P; otherwise behaves as Q. Both ${P || Q }$ and ${P ||| Q}$ model that processes P and Q run in parallel. The difference is that the former one requires P and Q to synchronize on the shared events, whereas in the latter process P and Q interleave.

PAT is a self-contained framework which supports simulating, reasoning and verifying concurrent systems. It has user-friendly interfaces, a featured model editor and an animated simulator. Most importantly, PAT implements various model checking techniques catering for different properties such as deadlock-freeness, reachability and LTL (Linear Temporal Logic) properties that are useful for our system verification. To achieve good performance, advanced optimization techniques are implemented in PAT, for example partial order reduction, symmetry reduction, process counter abstraction and parallel model checking (PAT, 2019).

2.2 Blockchain and smart contract

Proposed in the digital currency—bitcoin, blockchain technique is initially used as a way to replace the central bank to mint digital coins with the ability to prevent double spending (as long as the majority of participants called miners are honest). Following bitcoin, a large number of decentralized digital currencies have been invented. Essentially, blockchain relies on a peer-to-peer network with distributed nodes. Each node holds a copy of the ledger of the currency transactions, and thus even when some nodes (minority) malfunction, the ledger is still safe, since majority of nodes keep the correct ledger. The blockchain mechanism also uses cryptography to ensure its tamper-resistance, for example using digital signature to ensure that every transaction has its owner, and using hash pointer to ensure no transaction is tampered (for more details, see Narayanan et al., Reference Narayanan, Bonneau, Felten, Miller and Goldfeder2016).

With the popularity of blockchain, it has been discovered that blockchain can be useful in a wide range of applications other than digital currency. To facilitate building applications on top of blockchain, a few platforms have been developed. The most well-known platform is Ethereum, which provides a language Solidity to allow developers to program the agreements between participants on the blockchain. These agreements are called smart contracts. The execution of the smart contracts that are deployed on the blockchain will be enforced, as the execution (presented as state change of the smart contract) is logged and accepted by the majority of the nodes. Thus, whenever a condition/state of the contract is reached, the corresponding actions will be enforced, and no one can modify it (for details, see Chinchilla, Reference Chinchilla2019).

2.3 Ethereum

The Ethereum ecosystem serves as a runtime environment for smart contracts. It provides a language Solidity to write smart contracts. The smart contracts need Gas to be executed. And Gas can only be bought using the cryptocurrency Ether Provided by Ethereum. It mainly involves the following parts (Ethereum, 2019; Modi, Reference Modi2019; Buterin, Reference Buterin2019):

1. • EVM nodes: The EVM runs smart contract bytecode. Each node runs an instance of the EVM. Once written, the contracts have to be deployed on the EVM. Users can interact with the contracts that are on the EVM. The EVM node is a host for the Ethereum network. There can be many EVM nodes serving one network, in that sense the Ethereum network is decentralized.

2. • Mining nodes: The mining nodes (a.k.a. miners) form the basic blockchain. Each block contains data and smart contract code, and holds a copy of the blockchain. The mining nodes are required to verify and add blocks to the chain and in the process get paid in Ether. Every transaction requires Gas to run. Gas is the measure of the amount of Ether that is required to run.

3. • Externally owned account: It represents a user. When a new account is created, a private–public key pair is created. The externally owned account is the public key of the account.

4. • Wallet: It is a software that is associated with user accounts. One user may have more than one account in one wallet. The wallet is an important component as it is the software that tracks the amount of Ether that one user has. Mining nodes also require a wallet to store the Ether earned. Most wallets will show transactions made; these transactions are identified by their hash values.

5. • Smart contracts: Smart contracts are programs that exist on the EVM. They can accept inputs and, based on the inputs, can produce an action whether it is to read a value from the blockchain or to write a value to the blockchain. Smart contracts are the key to interacting with the blockchain.

6. • User interface: It refers to any interface that is interacting with a smart contract on the EVM. User interfaces together with smart contracts are known as DApps or decentralized apps.

The underlying blockchain consensus was initially proof-of-work (PoW) protocols using a memory-bound puzzle. Due to the criticism of PoW, for example energy waste and mining centralization, Ethereum is moving from PoW to proof-of-stake (PoS). Before moving to pure PoS, the two consensus PoW and PoS both exist in Ethereum. In this work, the PoW concept is used to illustrate how the blockchain works. Which consensus is used in EVM will not influence the booking system, which is on a higher abstract level. We highlight that the modelling of blockchain is also general and can be adopted to PoS.

4.1 User

A user, with an address addr, executes function and pays a fund val plus some gas amount gas with price gasPrice. This is modelled as a process User(addr, val, gas, gasPrice, function) (u1 in Figure 4). The reason that the user needs to specify the gas amount and gas price is that the gas price is changing according to the demand and supply; to be clear on how much the user pays the miner for executing the function, the user specifies the current gas price and the amount of gas the user would like to pay.

Figure 4 The user process

To call the function, the user broadcasts the transaction to miners. For simplicity, we assume the user sends the transactions to all miners in order starting from miner 0 (u2 in Figure 4), as this will not affect the results we would like to check. The process of sending a transaction to miner i is modelled as TxBrdcst(i, addr, val, gas, gasPrice, function) (u3 in Figure 4). When the miner index i is correct (i.e. i is smaller than the maximum number of miners—u5 in Figure 4), this process sends a transaction to the i-th miner with the parameters addr, val, gas, gasPrice, function (u6), and then continues to send the transaction to the next miner ${i+1}$ (u7). If the miner index reaches the top M (u8), meaning that the user has sent to every miner, then the process terminates with Skip (u9). The key word atomic (u4) prevents interleaving actions from the other processes and ensures that the sending action is atomic.

4.2 Miner

The miner i has two processes running in parallel: process TxPool(i) which receives transactions and puts them into a pool, and process TxBlock(i) which includes the transactions in the pool into a block and initiates the mining.

4.2.1 Process TxPool

The miner i receives the transactions broadcast by the users in the process TxPool(i) (p1 in Figure 5). On receiving a transaction with parameters, the miner first checks whether the sender, that is the user with address addr, has enough funds and gas (p2); if so, the miner inserts the transaction into his transaction pool (p4), which is modelled by the process TxInsert(i, addr, val, gas, gasPrice, function) defined in Figure 6); otherwise, the miner keeps waiting for another transaction, that is returning to process TxPool(i) (p5 in Figure 5).

Figure 5 The transaction pool process

Figure 6 The transaction insertion process

When inserting a transaction into a pool of miner i (Figure 6), the miner first checks whether the pool is full (t2), that is the current transactions in i (PoolPtr[i] is smaller than the max poolSize). If not, the miner receives the transaction in the pool by updating the address (t6), the value (t7), the gas (t8), the gasPrice (t9) and the function (t10) to the pool of miner i. At the end, we update the pointer of the transaction pool to the next empty position (t11). After updating the transaction pool, the miner sends a signal of newcomer to the channel datach for miner i to activate the block forming (t12). Finally the process goes back to TxPool(i) (t13) to listen to a new transaction. Note that before updating the transaction pool, we double check whether the current empty pool position is really empty by checking whether the gas for the current position is 0 (t3). If the current position is not empty (t14), the process moves to the next position (t15) and tries to insert the transaction to the pool (t16). If the transaction pool is full (t17), the transaction pointer is reset to 0 (t18) and then the transaction is inserted into the transaction pool for the next block (t19). We notice that if there are more than the maximum amount of transactions received in the pool before a block is formed, the pool will be reset to new ones. However, in our experiment, the total transactions are less than the maximum transitions in a pool, so this will not happen.

4.2.2 Process TxBlock

The process TxBlock(i) (Figure 7) includes available transitions into a block. When the number of transactions in the pool is smaller than the pool size (b2) and the channel for receiving transactions is not empty (b3), the process receives a signal that a new transaction has been inserted into the transaction pool ( ${b4-b35}$ ). If the pool is full, the process sets the pointer inPoolPtr(i) to 0 and goes back to the process TxBlock(i) (b36). When the pool is not full yet but there is no further transactions from the channel, as long as there are some transactions, the process starts mining (b34); Otherwise, the process goes back to TxBlock(i) and wait for transactions to be included (b35).

Figure 7 The process of including transactions into a block

On receiving the signal (b4), the miner checks whether the gas for this transaction is 0 (b5), which indicates there is no transaction in the pool.

1. • If there is no transaction in the pool and the block size is bigger than 1 (b6), meaning that all the transactions have been included in the block, the miner starts mining the block by calling Miner(i, 0) (b7). If there is no transaction in the pool and the block size is smaller than 1, meaning that there is no transaction in the block, then the process goes back to TxBlock(i) (b8).

2. • If there are transactions in the pool (b9), the miner checks whether the total gas for the current block reaches the top limit (b10) and checks whether the current transaction in the pool provides enough gas to execute the corresponding function in the transaction (b11). If so, the miner includes the transaction in the block ( ${b12-b27}$ ), by copying the address (b15), value (b16), gas (b17), gas price (b18) and function (b19) into the block. In addition, the miner updates the total gas of the block (b20) and sets the position of the transaction in the pool to be 0 to indicate that the transaction in the pool has been included into the block ( ${b21-b25}$ ). Furthermore, the pointer in the pool will be moved to the next and the size of the block is increased by 1 ( ${b26-b27}$ ). After updating the current transaction in the pool, the process goes back to TxBlock(i) (b28) to include the next transaction into the pool, until all transactions have been included, that is the pointer inPoolPtr[i] is bigger than the poolSize. If the current transaction in the pool fails to provide enough gas, the miner simply ignores the transaction and moves to the next one ( ${b29-b30}$ ). If the total gas has reached the top limit and there are transactions in the block, the miner starts mining (b31). If the total gas reaches the top, but somehow there is no transaction in the block, the process goes back (b33).

The mining process Miner(i, iter) in Figure 8 starts with a checking on whether the block index iter is smaller than the block size of the miner i. If so, the miner locks up the total value and executes the functions in the block (m1). If not, that is the functions have been fully executed, the block will be updated in process BlkUpdate(i, 0) (m2).

Figure 8 The miner process

To lock up the total value, the miner i calculates the amount to lock by adding the fund value and the gas value as the locked total amount ( ${l4-l7}$ in Figure 9). The remaining amount for the user with address addr (l3) is also calculated by deducting the locked amount (l8). Once the amount for a transaction iter is locked (l9), the miner executes the transaction by calling TxExec(i, iter) (l10).

Figure 9 The lock up process

Figure 10 The overall process of transaction execution

To execute a transaction iter (Figure 10), the miner reads the function in the transaction. There are four functions provided in the smart contract: SwitchFunction, ProposeFunction, SettleFunction and FetchFunction, which are defined as constants.

1. • When SwitchFunction is called (e3), the miner checks whether the user who calls the function is the contract owner (e4). If so, the miner executes the transaction and updates the gas with price of UPDATE (e5); Otherwise returns false to indicate that the function is not successfully executed (e6).

2. • When ProposeFucntion is called (e7), the miner checks whether the contract is switched on (e8). If so, the miner updates the gas with price of UPDATE and executes the transaction (e9); Otherwise returns false (e10).

3. • When SettleFunction is called (e11), the miner checks whether the user who calls the function is the contract owner (e12). If so, the miner executes the transaction and update the gas with price of ${UPDATE + TRANSFER}$ (e13); Otherwise returns false (e14). Differing from the previous two functions, this function costs more, including the updating fee and the transferring fee.

4. • When FetchFunction is called (e15), the miner checks whether the user who calls the function is the contract owner (e16). If so, the miner executes the transaction and updates the gas with the price of FETCH (e17); Otherwise returns false (e18).

In any function call, before executing the functions in the transaction, the miner first checks whether the transaction has enough gas (e5, e9, e13, e17). This is modelled in Figure 11 (g2). If not, the execution fails, as modelled in the process ExecFail(i, iter) ( ${g3, g13-g15}$ ). If there is enough gas, the miner updates the gas by deducting the amount (specified in the parameter according to different functions) from the locked wallet and adding them to the miner’s wallet ( ${g5-g10}$ ). Then the miner initiates the execution, modelled by the synchronized event consumed (g11).

Figure 11 The gas update process

Once the event consumed is synced (c1), the miner executes the function ( ${c2-c10}$ ). We model the execution of a function Execution(i, iter) by giving the transaction a unique ID (c3) and storing the transaction owner (c4), contract address (c5), transaction function (c6) and transaction fee in a set of arrays (c9) to indicate that the function of the smart contract in that transaction has been executed (Figure 12). Thus, the process returns true by calling process LockedReturn(i, iter, true) (c11). Then the miner returns the remaining locked gas to the user ( ${r1-r6}$ ). Before the miner executes the next transaction, she checks whether there is any block from another miner (r7). If so, the miner chooses to execute the first block she receives, modelled in process BlkDetect(i, iter, success) ( ${d1-d3}$ ).

Figure 12 The actual execution process

Recall that the miner process starts with a check on whether the block index is smaller than the block size of the miner i (m2 in Figure 8). If not, that is the transaction pool for the miner is full, the miner updates the block ( ${a2-a10}$ ), rewards the miner ( ${a11-a12}$ ) and broadcasts the block (a13), which is modelled in the process BlkUpdate(i, iter) in Figure 13. To broadcast a block, the miner sends the block number and block ID to other miners ( ${s3-s5}$ Figure 14. Note that s2 avoids that a node sends the block to himself/herself). Once this has been done, the miner increases the block ID by 1 (s7) and appends the block to her chain (s8 process BlkAppend(i, i, newBlockNum, blockid)). In the process BlkAppend(i, i, newBlockNum, blockid) defined in Figure 15, the minder appends the latest block ( ${k2-k4}$ ) and updates the state in the blockchain (k5).

Figure 13 The block update process

Figure 14 The block broadcasting process

Figure 15 The block appending process

The process of updating the blockchain actually updates the results of the functions as shown in Figure 16. When the operation is FetchFuction (h4), we add a fetch event to denote it (h5); When the operation is SwitchFunction (h7), the process switches the smart contract from the current state ${on/off}$ to the alternative state ${off/on}$ ( ${h8-h10}$ ); When the operation is ProposeFunction (h12), the process executes a propose event ( ${h13-h19}$ ), where the proposal initiator (h17) and the proposal state (h18) are recorded; When the operation is SettleFunction (h21), the process executes a settle event ( ${h22-h26}$ ), which records the one who settle the deal (h25) and the corresponding transaction state (h26). Once an operation is finished, the process goes back to itself for the operation in the next transaction (h6, h11, h20, h27). Note that the process first checks whether all the transaction has been updated. If so, the process resets the transaction container in process Reset(i, 0) (h28).

Figure 16 The chain updating process

In the reset process, the miner clears each transaction container by setting the values to 0 shown as follows in Figure 17 ( ${f2-f16}$ ). Once all the transactions in a block is cleared, the miner clears the block by setting the gas and size to 0 ( ${f17-f19}$ ) and going back to process TxBlock for the next round.

Figure 17 The reset process

To summarize, the flow of the processes can be abstractly represented as in Figure 18. In the figure, the arrow ${A \rightarrow B}$ indicates that process A calls process B; and the dashed arrow ${A\rightarrow B}$ means that process A sends a message to process B.

Figure 18 An overall relation between the processes

The user initiates a transaction (process User) and broadcasts to miners (process TxBrdcst). The transaction is received by the process TxPool. If there is enough gas, the transaction is added to the pool in process TxInsert. Once the pool is full or there is no further transactions, the process TxInsert triggers the block forming by sending a command to the process TxBlock. The process forms a block and calls the miner (process Miner). The miner locks up the gas (calling process LockUp) for each transaction; until no more transaction left, the miner updates to form a new block (process BlkUpdate).

1. • If the gas is locked, a transaction is passed to the process TxExec to further execute. Depending on different functions in the transaction, the process TxExec deducts different gas (process GasConsume) and executes different functions (process Execution). If anything wrong happens, the process TxExec goes to LockedReturn to release the locked gas. Similarly, if error happens during execution in process Execution, the process LockedReturn is called. In the process GasConsume, if there is no enough gas, ExecFail will be triggered. ExecFail resets the locked wallet. At this point, a new block from other miners may be sent, so the process calls the process BlkDetect. If a new block is received, the process appends the block to the chain BlkAppedn and sends a message to trigger the process BlkBrdcst in which new blocks will be broadcasted.

2. • In the case where the block is updated (process BlkUpdate), the block is broadcasted to others in the process BlkBrdcst, and the block is also appended to the chain in process BlkAppend.

Once the chain is appended, the process ChainUpdate is called by the process BlkAppend to update the actual chain. If it does not succeed, the whole process will be Reset.

4.3 The overall process

In summary, the proposed blockchain-based booking system can be modelled as the User process and the miner process running in parallel. And the miner process is the transaction pool process TxPool and the blockchain process TxBlock running in parallel.

5.1 Properties

We verified five properties that the system needs to satisfy, which are defined as follows:

1. • Deadlockfree: No deadlock situation occurs in the system.

2. • GasRunOut: Each transaction in a block has enough gas to be executed to completion by miners.

3. • SameBlockNumEventually: Each miner reaches the same block number eventually.

4. • ReceiveSettlement: The request (smart contract) owner has settled with some proposer, and thus each miner receives the same transaction.

5. • ProposalReceived: Proposals have been accepted by the request.

Each property is formalized as an assertion in PAT for automatic formal verification as shown in Table 1. Note that the symbol ${\&\&}$ is logical ‘and’. Thus, the formula ${\&\& i:\{0..M\}}$ @ ${{blockNum[i]==1}}$ means ${blockNum[0]==1 \land blockNum[1]==1 \land \ldots \land blockNum[M]==1}$ . Similarly, the formula ${\&\& i: \{0..M\}}$ @ ${settledWith[i] == 1}$ means that ${\forall i\in \{0..M\}: settledWith[i] == 1}$ .

For each property, we match one execution. And the five executions are listed as follows:

1. • ProposerExecution: A user submits proposals to the request (smart contract).

2. • ListnerExecution: A user submits proposals to the request, and the request owner listens to the ‘proposal’ event from the request.

3. • UnavailableExecution: The request owner turns off the request, and no more proposals are allowed to be accepted by the request.

4. • NotOwnerExecution: A user who is not the request owner fetches the proposals from the request.

5. • MultipleUsersExecution: Many users submit their proposals at the same time.

6. • SettlementExecution: The request owner seals a deal.

The formalization of the executions is defined in Table 2. Note that the ‘ProposeExecution’ differs from the ‘MultipleUsersExecution’ in the number of users; the executions ‘ProposeExecution’, ‘UnavialableExecution’, ‘NotOwnerExecution’ and ‘SettlementExecution’ differ in the function parameters (ProposeFunction, SwithchFunction, FetchFunction and SettelFunction respectively). The ‘ListenerExecution’ adds one more process to the ‘ProposeExecution’. The additional process Listener(contractOwner) is shown in Figure 20, which defines a user interface that listens to the state change.

Table 2 Formalization of executions

Figure 20 The process Listener

The assertions that match the property with the executions are defined as follows:

1. • Assertion 1: ${ProposerExecution\ Deadlockfree}$

2. • Assertion 2: ${ProposerExecution |= []! GasRunOut}$

3. • Assertion 3: ${ProposerExecution\ reaches\ SameBlockNumEventually}$

4. • Assertion 4: ${ListenerExecution |= ProposalReceived \rightarrow listenerReceiving}$

5. • Assertion 5: ${UnavailableExecution |= []! ProposalReceived}$

6. • Assertion 6: ${NotOwnerExecution |= []! Fetch}$

7. • Assertion 7: ${MultipleUsersExecution\ reaches\ SameBlockNumEventually}$

8. • Assertion 8: ${SettlementExecution\ reaches\ ReceiveSettlement}$

The Assertion 1 states that the execution ProposerExecution is deadlock free. The Assertion 2 ensures that each transaction has enough gas to be executed. The symbol ‘ ${|=}$ ’ reads as ‘satisfies’, which states that the execution satisfies the claimed LTL property on the right-hand side. The symbol ‘[]’ reads as ‘globally’ meaning that every state in the system execution shall satisfy the subsequent LTL formula. The Assertion 3 states that in the execution ProposerExecution, each miner reaches the same block. The Assertion 4 ensures that if the proposal is received by the smart contract, then the listener must have received the proposal. The Assertion 5 says that if the smart contract is turned off, then the proposal will not be received. The Assertion 6 states that when a user, who is not the smart contract owner, fetches the proposal, she will never succeed. The Assertion 7 ensures that when there are multiple users, the execution can still reach the same block eventually. The Assertion 8 means that when the smart contract owner seals a deal, the deal must have been settled.

5.2 Verification settings

For the simplicity of verification, we assume the following settings: there are five hoteliers or travellers and two miners; and the length of blockchain is five with the maximally 20 transactions in a block. The maximum gas limit for a block is set to be a large number ${20\,000}$ , which is the gas limit for a transaction times the maximum number of transaction in a block. We set the reward for successfully appending the valid block to be a large number as well, so that there is enough Ether and Gas to perform the functions. We assume the gas consumption of each functions (FETCH, TRANSFER and UPDATE) is an integer. We define asynchronized channels with buffer size of 5 to model the network delays. In addition, we set smart contract address and the smart contract’s owner address as integers as well. Furthermore, we set the gas consumption limit, miner’s selection of gas price per transaction, the pool size to receive transactions for each miner and pool size for received proposal, and the data size as shown in Figure 21.

Figure 21 The experiment settings

5.3 Verification results

Our experiment shows that the outcome of the assertions from PAT with respect to different configurations of C users and M miners. We can see from Table 3 that the properties are all satisfied when there are five users and two miners. Note that in the table, we also show the checked states, state transactions and the time used for verification using PAT. Generally speaking, model checking in PAT verifies all the possible reaching states (defined by the state variables) and detects whether a bad state that some of the assertions are violated. States are connected by transitions, which defines the possible execution traces of the system behaviour. However, when C and M are set larger, the state space is too large to be verified. The states and transactions increase exponentially as shown in Tables 4 and 5. The increasing numbers of miners lead to more state variables and thus increase the states exponentially. Similarly, since the miners work in parallel with interleaving actions, the number of possible actions (i.e. the transactions) grows steeply; especially as the model includes peer-to-peer broadcasting, the increasing numbers of miners lead to exponential growth of the broadcasting messages.

Table 3 The assertion results with ${C = 5}$ and ${M = 2}$

Table 4 The assertion results with ${C = 5}$ and ${M = 10}$

Table 5 The assertion results with ${C = 5}$ and ${M = 50}$