Variable-State-Trigger: A Formal Model of Smart Contracts Based on Conditional Response and Finite State Automata and Its Application

Abstract

As one of the technical elements supporting the blockchain to realize decentralized autonomous organizations, smart contracts are crucial for understanding the inherent properties of blockchain systems through formal research. Most existing formal models of smart contracts focus primarily on static properties, lacking the depiction of dynamic processes such as conditional responses and internal state migration during contract execution, which complicates effective supervision. In this paper, a novel formal model of smart contracts, based on finite state automata, named Variable-State-Trigger (VST), is proposed, which presents state migration and conditional response mechanisms during smart contract execution. The VST model is verified to portray both the static and dynamic properties of smart contracts, providing new avenues for effective supervision during contract execution. Moreover, the VST model is used to illustrate the life cycle of a UAV mission smart contract, demonstrating its feasibility. With the growing integration of blockchain and emerging technologies, smart contracts have found applications in various fields, including drone swarm coordination. In this context, smart contracts enable secure, decentralized management and automation of interactions between autonomous drones, ensuring compliance with predefined conditions and enhancing the reliability of complex drone operations. The VST model can be extended to such applications, offering dynamic supervision and enhancing the coordination efficiency in decentralized autonomous drone systems.

1. Introduction

With the introduction of Bitcoin [1] in 2008, blockchain came into the limelight as a distributed, asymmetric encrypted peer-to-peer network. Bitcoin transactions rely on Bitcoin scripts to take place on a decentralized peer-to-peer network. Bitcoin scripts are a stack-based, non-Turing-complete scripting language that defines the basic rules of Bitcoin transactions and is the prototype of a blockchain smart contract. Since then, a number of decentralized cryptocurrencies, typified by Bitcoin, have enabled the use of blockchain in finance. In 2015, Ethereum [2] was launched, which is the first blockchain platform supporting Turing-complete language programming. Ethereum users can write smart contracts in languages such as Solidity to automate the transaction process. Subsequently, platforms such as Hyperledger [3] and EOS [4] were released, and their common feature is that they rely on smart contracts to automate interactions between nodes on a decentralized/weakly centralized peer-to-peer network. Thanks to Turing-complete language programming, such interactions are capable of handling computations of almost arbitrary complexity.

With the introduction of smart contracts, blockchain is no longer limited to the financial sector but is also used in the Internet of Industry [5], logistics [6], healthcare [7], legal [8], vulnerability detection [9], privacy protection [10], and other fields [11], showing great application value. One emerging application area is the coordination of drone swarms. Drone swarms, consisting of multiple autonomous drones working together, require secure and reliable decentralized coordination to efficiently carry out tasks such as surveillance, search and rescue, or delivery services. Smart contracts can be leveraged in this context to automate and manage the interactions between individual drones, ensuring that certain conditions, such as task allocation, communication protocols, and resource sharing, are executed without central authority. By applying blockchain-based smart contracts, the operations of drone swarms become tamper-proof and can execute autonomously based on predefined rules, improving operational transparency, security, and fault tolerance in dynamic and potentially adversarial environments.

In order to better realize the application of blockchain technology in combination with traditional industries, more and more researchers [12,13,14] have focused their work on smart contracts themselves in recent years.

A smart contract is defined as a computer program running in a distributed system whose rules are pre-set and whose states are conditionally correlated to facilitate the exchange of information, value, and asset ownership among distributed nodes, and that can encapsulate, verify, and execute complex behaviors [15]. Zheng [16] assumes that the smart contract life cycle is divided into four stages: creation, deployment, execution, and completion. A life-cycle approach to understanding smart contracts can assist in gaining a more thorough understanding of how they work. At present, the main research directions around smart contracts in academia are smart contract security issues [17,18,19], smart contract applications [20,21], mechanism design [22,23], and formalization [24].

Among these, formalization includes formal specification and formal verification, two important research elements. Formal research on smart contracts is a mathematical description of what a smart contract is and what it does, which can solve a series of problems such as functional verification, privacy, security, scalability, bug bounties, the Oracle problem, blockchain consensus, etc. [25]. Existing research on the formalization of smart contracts has focused on formal verification, i.e., formal tools/frameworks to help troubleshoot vulnerabilities in smart contracts and reduce the risk of malicious attacks. However, few studies have analyzed the state migration of smart contracts from a microscopic perspective, resulting in a lack of detail on the internal execution logic of smart contracts, which makes it difficult to effectively supervise the process of contract execution as a black box.

At the same time, most of the existing formal models of smart contracts are based on specific application areas, with insufficient abstraction and a lack of generality to provide theoretical support for general research on smart contracts. Therefore, this paper analyzes the internal execution logic of smart contracts based on finite state automata and a conditional response mechanism and proposes a general formal model of smart contracts, the Variable-State-Trigger (VST) model, which is shown in Figure 1. More importantly, this paper introduces the application of the VST model in the field of lightweight communication for drones, and will focus on introducing an intelligent contract for drone communication, created based on the VST model in the sixth part. This work is pioneering in the field of drone communication and formalization of smart contracts. The contributions of this paper are as follows.

Contributions:

• This paper innovatively combines theorem proving and finite state automata to describe smart contracts. In general, finite state automata can clearly express the state migration process of smart contracts. Microscopically, the conditional trigger mechanism of smart contracts can be explained by means of theorem proof.
• This paper represents the smart contract conditional response mechanism based on the graph structure, so as to modularize the smart contract so that it can be used for smart contract supervision, vulnerability detection, etc.
• This paper expounds on the formal role of the proposed VST model in the practical application field of drone communication, which is innovative.

This paper is structured as follows: Section 2 lists the existing research on the formalization of smart contracts; Section 3 defines smart contracts formally and gives the basic definition of the VST model; Section 4 analyzes the micro-conditional response mechanism; Section 5 uses a rigorous mathematical proof method to verify the true property of the VST model; and Section 6 takes a UAV mission contract written in natural language as an example and analyzes the VST model’s ability to interpret real contracts and verify its feasibility.

2. Related Work

Currently, research on blockchain technology and smart contracts encompasses a variety of approaches to enhance security, functionality, and scalability. AlSobeh’s work, “OSM: leveraging model checking for observing dynamic behaviors in aspect-oriented applications”, employs model checking techniques to scrutinize the dynamic behaviors within aspect-oriented applications, providing insights into their complex interactions [26]. Xu et al. contribute to the field with “Adding generic role- and process-based behaviors to smart contracts using dynamic condition response graphs”, where they introduce a method to enrich smart contracts with role- and process-based behaviors, enhancing their adaptability and responsiveness to changing conditions [27].

In the domain of blockchain system verification, AlSobeh and Magableh present “BlockASP: a framework for AOP-based model checking blockchain system”, which utilizes aspect-oriented programming to facilitate model checking and ensure the integrity of blockchain systems [28]. Lekidis and Katsaros integrate data-driven security with model checking and self-adaptation in “Integrating data-driven security, model checking, and self-adaptation for IoT systems using BIP components”, showcasing the potential of these techniques in enhancing IoT system resilience [29].

Dinh et al. offer a comprehensive view of blockchain systems in “Untangling blockchain: a data processing view of blockchain systems”, dissecting the technology’s data processing mechanisms and their implications [30]. Zheng et al. address data sharing challenges in “Scalable and privacy-preserving data sharing based on blockchain”, proposing solutions that maintain privacy while facilitating data sharing at scale [31].

Zhang et al. introduce a reputation-based mechanism in “A reputation-based mechanism for transaction processing in blockchain systems”, aiming to optimize transaction processing through trust evaluation among nodes [32]. Wu et al. present “VQL: efficient and verifiable cloud query services for blockchain systems”, a system that ensures the efficiency and verifiability of cloud queries, crucial for maintaining data integrity in blockchain applications [33].

Finally, Gao et al. delve into the security vulnerabilities of the Bitcoin system with “Power adjusting and bribery racing: novel mining attacks in the Bitcoin system”, highlighting innovative attack vectors and their implications for cryptocurrency mining security [34].

In summary, these studies represent a diverse array of approaches to advancing blockchain technology and smart contract applications, focusing on aspects such as security enhancement, functional expansion, privacy preservation, and system scalability, demonstrating the multifaceted nature of research in this domain.

3. VST Model Overview

In this section, we introduce a conditional response mechanism based on finite state automata to describe the dynamic process of state migration of smart contracts from a microscopic perspective. The Variable-State-Trigger (VST) model is a formal specification of the smart contract and describes three core properties of the smart contract: Variable, State, and Trigger. The parameters involved in the VST model are shown in

Table 1. Parameter symbol list.

Symbols	Implication
C	Smart Contract
V	Environment
S	Smart Contract State Set
T	Conditional Response Mechanism
v	Environment Variables
s	Instantaneous State
$T_x$	Conditional Response Module
t	Triggers
e	Conditional Response Path

.

The environment, V, in which the smart contract, C, is located can be quantified as a $\left|I\right|$-dimensional vector, and each component, $v_i$, is called an environment variable. The smart contract, C, is subjected to changes in the environment variables and undergoes state migration in a finite state space, S, which contains $\left|J\right|$ instantaneous states. $I,J$ are sets of indicators for the environment, V, and state set, S, respectively. The conditional response mechanism, T, consists of $\left|X\right|$ modules $T_x$, $T_x$ is a directed acyclic graph consisting of vertices, t, and edges, e, and X is the set of indicators of T.

Definition 1.

Smart Contract, C

A smart contract $C:=(V,S,T)$ is a triple consisting of:

• A vector $V=(v_1,v_2,\dots ,v_i,\dots ,v_{\left|I\right|})$;
• A set $S=\left\{s_j\right|s_j=f\left(V_j\right),j\in J\}$;
• A set $T=\{T_1,T_2,\dots ,T_x,\dots ,T_{\left|X\right|}\}$, $T_x=({\tau }_x,E_x),{\tau }_x=\left\{t_j\right|t_j=(s_j,V_j),s_j\in S\},E_x=\left\{e_{mn}\right|e_{mn}=<t_m,t_n>,t_m,t_n\in \tau \}$.

In Definition 1, the environment variable, $v_i$, is a component of the multidimensional vector V. The state $s_j$ is a function on V, using $V_j$ to denote a particular environment that induces the state $s_j$. The trigger, $t_j$, is represented by the binary $(s_j,V_j)$, in the sense that the variable environment is $V_j$, and the instantaneous state of the smart contract, C, is represented as $s_j$. The conditional response path, $e_{m,n}$, is a directed edge from vertex $t_m$ to vertex $t_n$ in the directed acyclic graph $T_x$, in the sense that the trigger condition $t_n$ occurs only if the trigger condition $t_m$ has already occurred.

Definition 2.

The environment of a smart contract, C, can be quantified as a multidimensional vector $V=(v_1,v_2,\dots ,v_i,\dots ,v_{\left|I\right|})$, where each component, $v_i$, is called an environmental variable.

To explain more concretely the environment of the smart contract, C, the multidimensional vector $V=(v_1,v_2,\dots ,v_i,\dots ,v_{\left|I\right|})$ can be represented by a data table, as shown in

Table 2. The environment in which smart contracts operate.

Environment Variables	Data Storage	Meta-Attributes
$v_0$	$attribut{e}_0$:value	key variable/dummy variable
$v_1$	$attribut{e}_1$:value	key variable/dummy variable
$v_2$	$attribut{e}_2$:value	key variable/dummy variable
…	…	…
…	…	…
$v_{\left|I\right|}$	$attribut{e}_{\left|I\right|}$:value	key variable/dummy variable

. For each component, $v_i$, in addition to symbols and key-value pairs, it also has meta-attributes: key variable/dummy variable.

Definition 3.

States

The value range of the function $s_j=f\left(V_j\right)$ is $\{s_0,s_{cpl},s_{brk},s_{fin},s_{fai}\}$.

The state set, S, consists of |j| instantaneous states, $s^{*}$; “states” contain two forms: stable states and intermediate states. The stable states include the initial state, $s_0$, the completion state, $s_{fin}$, and the failure state, $s_{fai}$; The intermediate states include the success state, $s_{cpl}$, and the default state, $s_{brk}$. The value of any instantaneous state, $s^{*}$, is equal to some steady state or intermediate state, but the environment, $V^{*}$, that induces different instantaneous states varies.

There are intra-state migration and inter-state migration in the VST model, as shown in Figure 2.

Definition 4.

Inter-state migration

If $s^{*}=f\left(V^{*}\right)\to s^{**}=f\left(V^{**}\right)$ satisfies $V^{*}\ne V^{**},s^{*}\ne s^{**}$, this migration process → is called inter-state migration.

The reason for the above two different forms of state migration is that there are several key variables and key points in the multidimensional vector $V=(v_1,v_2,\dots ,v_k)$, there are several key variables and corresponding key points, and inter-state migration is caused when and only when the value of the key variables changes to the key point; otherwise, only intra-state migration is caused. In other words, the intra-state migration is related to all variables in the multidimensional vector V, while the inter-state migration is only related to the key variables in the multidimensional vector V.

Definition 5.

Key variables

If a change in the value of one or more components of a vector causes inter-state migration, then these components are called key variables, i.e., if $s^{*}=f\left(V^{*}\right)\to s^{**}=f\left(V^{**}\right)$ satisfies $V^{*}=(v_1,v_2,\dots ,v_m,\dots ,v_k),V^{**}=(v_1,v_2,\dots ,v_m^{*},\dots ,v_k),v_m\ne v_m^{*},s^{*}\ne s^{**}$, then $v_m$ is called a key variable.

Definition 6.

Dummy variables

If any change in the value of one or more components of a vector does not cause inter-state migration, then these components are called dummy variables, i.e., if $s^{*}=f\left(V^{*}\right)\to s^{**}=f\left(V^{**}\right)$ satisfies $V^{*}=(v_1,v_2,\dots ,v_m,\dots ,v_k),V^{**}=(v_1,v_2,\dots ,v_m^{*},\dots ,v_k),v_m\ne v_m^{*},s^{*}=s^{**}$, then $v_m$ is called a dummy variable.

It is worth noting that the range of key variables and dummy elements changes dynamically with the state migration of the smart contract. That is, at state $s^{*}$, it is assumed that $v_m$ is the key variable that affects the migration of the current state to the next state, but when the state migrates to $s^{**}$, $v_m$ no longer affects the future state migration, i.e., the dummy element.

Definition 7.

key points and key set

If a change in the value of a key variable reaches a certain point and causes inter-state migration, then this point is called a key point, and the set of these key points is called a key set, i.e., when $s=f\left(V\right)$ satisfies $V=(v_1,v_2,\dots ,v_m,\dots ,v_k)$, $v_m$ is a key variable in V, if $\exists p\in \mathbb{R}$ satisfies $\underset{v_m\to p^{-}}{lim}f\left(V\right)\ne \underset{v_m\to p^{+}}{lim}f\left(V\right)$, then p is called a key point, and the set of values like p is called a key set.

Definition 8.

Legal interval

An interval is called a legal interval if the value of a key variable varying arbitrarily within that interval does not cause the state to migrate from $s_{cpl}$ to $s_{brk}$.

Definition 9.

Illegal interval

An interval is called an illegal interval if the value of a key variable changing within that interval causes the state to migrate to $s_{brk}$.

i.e., when $s^{*}=f\left(V^{*}\right)\to s^{**}=f\left(V^{**}\right)$ satisfies $s^{*}=s_{cpl},V^{*}=(v_1,v_2,\dots ,v_m,\dots ,v_k),V^{**}=(v_1,v_2,\dots ,v_m^{*},\dots ,v_k)$, $v_m$ is a key variable in $V^{*}$, $v_m^{*}=a$, if an interval A satisfies $\forall a\in A$, $f\left(V^{**}\right)=s^{*}=s_{cpl}$, then A is called a legal interval, and its complement set $\tilde{A}$ is called an illegal interval.

Stable state. When the execution of the smart contract is completed, the contract migrates to the stable state, i.e., inter-state migration such as $s_{cpl}\to s_{fin},s_{brk}\to s_{fai}$ occurs. At this point, the environment, V, no longer changes. When the environment, V, of the smart contract, C, no longer changes, C migrates from the intermediate state to the stable state: if the instantaneous state $s^{*}=s_{cpl}$ and the stable state $s=s_{fin}$, the contract, C, executes successfully; if the instantaneous state $s^{*}=s_{brk}$ and the stable state $s=s_{fai}$, the execution of the contract, C, fails. The migration of a smart contract, C, from an intermediate state to a stable state still follows the conditions of inter-state migration. This process has a special key variable, $v_{stale}$, whose role is to listen to whether the environment, V, stops changing, and if the environment, V, stops changing then $v_{stale}$ reaches the key point and causes the inter-state migration, which also marks the contract, C, reaching the stable state.

Definition 10.

Conditional response mechanism

The conditional response mechanism, T, of the smart contract, C, consists of several conditional response modules, $T_x$, and each module, $T_x$, is a directed acyclic graph, including the vertex set, τ, and the edge set, E, where the vertex set contains the following vertex types.

• $t_0=(s_0,V_0)$;
• $t_{cpl}=(s_{cpl},V_{cpl})$;
• $t_{brk}=(s_{brk},V_{brk})$;
• $t_{fin}=(s_{fin},V_{fin})$;
• $t_{fai}=(s_{fai},V_{fai})$.

In Definition 10, the vertices $t_0,t_{fin},t_{fai}$ denote the trigger conditions for the stable states $s_0,s_{fin},s_{fai}$, respectively, and the vertices $t_{cpl},t_{brk}$ denote the trigger conditions for the intermediate states $s_{cpl},s_{brk}$, respectively.

4. Microscopic Conditional Response

In order to describe the conditional response mechanism of a smart contract from a microscopic perspective, $t=(s,V)$ is introduced as a trigger into the VST model. Several triggers, t, and conditional response paths, e, form a directed acyclic graph, $T_x$, and several directed acyclic graphs, $T_x$, form the conditional response mechanism of a smart contract, C. Unlike the state migration graphs of finite state automata, there is no loop in the directed acyclic graphs, which can clearly show the start–end, and are more advantageous in describing complex logic structures than the state migration graphs with loops. Statically, T, as a collection of directed acyclic graphs, can clearly and intuitively show the conditional response structure of the contract, C, i.e., the encoding logic; dynamically, the trigger, t, can record the environment, V, when the smart contract, C, reaches the specified state, s, and the dynamic path returns to the user, t, during the contract execution, providing an idea for effective supervision of smart contracts. In this section, we introduce the micro-conditional response mechanism from a syntax-logical structure-modularity writing idea.

4.1. Grammar

Definition 10 introduces five types of triggers t: $t_0,t_{cpl},t_{brk},t_{fin},t_{fai}$. Since the conditional response mechanism of a smart contract works mostly in the intermediate state, the contract can be executed properly when and only when $t=t_{cpl}$, so the form $t_i$ (i denotes a letter or a non-zero number) is used below to refer to $t_{cpl}$, $t_0,t_{brk}{t}_{fin},t_{fai}$ without special specification, and $t_{fai}$ is marked separately.

The meaning of the trigger $t_0$ is to listen to the address of the smart contract, C, to see if it receives a call request from the user, and if the user issues a call to C, then $t_0$ is triggered and the contract, C, starts execution. The meaning of the trigger $t_i$ is that the smart contract, C, is executed normally and all key variables in the environment, V, are in the legal interval. As shown in Figure 3, when $t_i$ is triggered $s_i=s_{cpl}$, if $t_i$ is triggered then $t_j=(s_{cpl},V_j)$ cannot be triggered, and no arbitrary $t_k=(s_{cpl},V_k)$ is triggered, meaning that one or some key variables in the environment, V, change into an illegal interval, and $t_{brk}$ is triggered, signifying that the smart contract, C, is temporarily suspended. It is worth noting that each $t_i$ can point to $t_{brk}$,while the $t_{brk}$ which $t_i$ points to is not consistent with the $t_{brk}$ which $t_j$ points to. Although $s_i=s_{cpl}=f\left(V_i\right)=f(v_1,v_2,\dots ,v_i,\dots ,v_{\left|I\right|})$ is equivalent to $s_j=s_{cpl}=f\left(V_i\right)=f(v_1,v_2,\dots ,v_j,\dots ,v_{\left|I\right|})$, the key variables of $V_i$ are partly different from $V_j$,which means that the trigger of state migration $s_i\to s_i^{brk}$ is distinct from $s_j\to s_j^{brk}$ (according to Definition 5).

$t_{fin}$ marks the successful execution of a smart contract, C. A smart contract may have multiple clauses, which may be relatively independent of each other or may affect each other. $t_{fin}$ means that, after all the required clauses have been invoked, the environment, V, no longer changes, and the instantaneous state of the smart contract is $s_{cpl}$, and then the contract will migrate to the stable state, $s_{fin}$.

The meaning of $t_{fai}$ is that the execution of the smart contract, C, ends in failure. After $t_{brk}$ is triggered, if the environment, V, does not change any more, then C will migrate from the hung state, $s_{brk}$, to the failed state, $s_{fai}$.

4.2. Logical Structure

Smart contracts are mainly presented in the form of program code, and there are three main logical structures in programming: sequential structure, selection structure, and cyclic structure. Naturally, directed acyclic graphs can describe sequential and selective structures, but not cyclic structures directly. However, the microscopic conditional response mechanism of the VST model can overcome this problem, and the directed acyclic graph, $T_x$, can explain the loop structure in smart contracts well.

As shown in Figure 4, when $t_i,t_j,t_k$ form a loop structure, there are.

• $t_i\to t_j,t_j\to t_k,t_k\to t_i$;
• $t_i=(s_i,V_i=(\dots ,V_i^m,\dots ))$;
• $t_j=(s_j,V_j=(\dots ,V_j^m,\dots ))$;
• $t_k=(s_k,V_k=(\dots ,V_k^m,\dots ))$.

It is well known that dead loops are meaningless in computer programming, so any loop structure must have a counter, $v_c$, to control the number of loops in order to prevent the contract program from falling into a dead loop. Suppose $v_i^m,v_j^m,v_k^m$ are the key variables of $V_i,V_j,V_k$, respectively, then the loop progression between the trigger conditions $t_i,t_j,t_k$ can be replaced by a trigger condition $t_{ijk}=(s_{cpl},V_{ijk})$ instead, where $v_i^m,v_j^m,v_k^m,v_c$ are the key variables of the multidimensional vector $V_{ijk}$. In other words, microscopically $t_i\to t_j,t_j\to t_k,t_k\to t_i$ corresponding to $s_i\to s_j,s_j\to s_k,s_k\to t_i$, the migration process between the three instantaneous states can actually be interpreted as an intra-state migration of $s_{ijk}=s_{cpl}$, which fuses the three instantaneous states.

4.3. Modularization

Definition 11.

Dimension

The set $\widehat{V_t}$ of all event parameters of a trigger, t, is called the dimension of t.

Definition 12.

Each DAG $T_x\in T$ in a smart contract consisting of consecutive triggers is called a module.

There may be multiple clauses in a smart contract, and the modularity is designed to discuss the possible relationships between the clauses of a smart contract. In a smart contract, the following two relationships between different modules may exist.

• Mutually independent:
  Module $T_x$ completion does not cause module $T_y$ execution, and module $T_y$ completion does not cause module $T_x$ execution.
• Strictly progressive:
  Module $T_x$ completion causes module $T_y$ execution, and module $T_y$ completion does not cause module $T_x$ execution.

For convenience, the relationship between module $T_x$ and module $T_y$ can be formalized as $\neg T_{x}R{T}_y$ if they meet the mutually independent clause. $R\subseteq T\times T$ represents the relationship between modules. The relationship between module $T_x$ and module $T_y$ can be formalized as $T_{x}R{T}_y$ if they meet the strictly progressive clause.

Definition 13.

Let the initial vertices of the modules $T_x$ and $T_y$ be $t_x^0$ and $t_y^0$, respectively, and their termination vertices be $t_x^e$ and $t_y^e$, respectively. If the module $T_x$ and the module $T_y$ satisfy:

$$\left\{\begin{array}{c}\hfill \widehat{V_x^e}\cap \widehat{V_y^0}\ne \widehat{V_x^e}\\ \hfill \widehat{V_y^e}\cap \widehat{V_x^0}\ne \widehat{V_y^e}\end{array}\right.$$

(1)

Then the module $T_x$ and the module $T_y$ are said to be mutually independent $\neg T_{x}R{T}_y$.

If the module $T_x$ and the module $T_y$ satisfy:

$$\left\{\begin{array}{c}\hfill \widehat{V_x^e}\cap \widehat{V_y^0}=\widehat{V_x^e}\\ \hfill \widehat{V_x^e}\ne \widehat{V_y^0}\\ \hfill \widehat{V_y^e}\cap \widehat{V_x^0}\ne \widehat{V_y^e}\end{array}\right.$$

(2)

Then the module $T_x$ and the module $T_y$ are said to be strictly progressive $T_{x}R{T}_y$.

As shown in Figure 5 and Figure 6, let the module $T_x$ start with a green sphere and end with a blue sphere, and the module $T_y$ start with an orange sphere and end with a yellow sphere. Only the event parameters of each vertex are written in parentheses, and the parameters marked in red are the key variables of that vertex. As shown in the Figure 5, $\{a,b,c\}\cap \{a,b,d\}\ne \{a,b,c\}$, while $\{a,b,d\}\cap \{a,b,c\}\ne \{a,b,d\}$, so the module $T_x$ and the module $T_y$ are independent of each other; as shown in Figure 6, $\{a,b,c\}\cap \{a,b,c,d\}=\{a,b,c\}$, $\{a,b,c\}\ne \{a,b,c,d\}$, while $\{a,b,c,d\}\cap \{a,b,c\}\ne \{a,b,c,d\}$, thus module $T_x$ and module $T_y$ are strictly recursive.

The strictly recursive relationship between modules provides feasibility for the implementation of the complementary terms. If $T_1,T_2$ satisfy $t_1^e=t_{brk},\widehat{v_1^e}\cap \widehat{v_2^0}=\widehat{v_1^e},\widehat{v_1^e}\ne \widehat{v_2^0},\widehat{v_1^e}\cap \widehat{v_2^0}\ne \widehat{v_2^e}$, then $T_2$ is said to be a supplementary clause to $T_1$, that is, if the relevant clause in $T_1$ is violated, the relevant clause in $T_2$ can be invoked to make the intelligent. The contract can be executed smoothly by calling $T_2$ to migrate its instantaneous state to $s_{cpl}$.

In the module, there is a special existence called the supervision module. The responsibility of the supervision module is to monitor the environment, V, and the state, S, of the smart contract. Assuming there is a key variable time. Once the state of the smart contract is $s_{brk}$, the smart contract does not migrate to $s_{cpl}$ within time, the state of the smart contract migrates to $s_{fai}$, and the smart contract fails to run. The supervision module can effectively solve the problem that the loss causes by malicious contracts or the vulnerabilities in the contract itself cannot be terminated.

5. Theoretical Analysis

In the previous section, finite state automata are used to illustrate the state transition process of smart contracts from a macro perspective, and the conditional response mechanism is introduced to analyze the reasons for smart contract state transition from a micro perspective. Nevertheless, given the reality property of the VST model, the feasibility of the model needs to be demonstrated. Below we will introduce the theorem of the VST model and give the proof process. In this section, three theorems will be presented. The importance of Theorems 1 and 2 is to explain what is the condition for the state migration of the smart contract. The importance of Theorem 3 lies in proving the completeness of the conditional corresponding mechanism theory.

Theorem 1.

A necessary and sufficient condition for the inter-state migration $s_{cpl}\to s_{brk}$ is that the value of at least one key variable changes to an illegal interval.

Proof. 

• Sufficiency
• Let the current state be:

  $$s^{*}=f\left((v_1,v_2,\dots ,v_m,\dots ,v_k)\right)=s_{cpl}$$

  (3)

Assuming there exists a previous state:

$$\begin{array}{c}\hfill s^{*-}=f\left((v_1,v_2,\dots ,v_{m-},\dots ,v_k)\right)=s_{cpl}\end{array}$$

(4)

there exists an intra-state migration $s^{*-}\to s^{*}$. According to Definition 8, there exists a key variable $v_{m-}=a^{-},v_m=a$ satisfies $a^{-},a\in A$, and A is a legal interval. Let set p be a key point and $a<p$. According to Definitions 7–9, the two ends of a key point are the legal interval and the illegal interval.

When $v_{m*}=b,b\in \tilde{A},b\ge p$, there exists:

$$\begin{array}{c}\hfill f\left((v_1,v_2,\dots ,v_m,\dots ,v_k)\right)\ne f\left((v_1,v_2,\dots ,v_{m*},\dots ,v_k)\right))\end{array}$$

(5)

the current state $s^{*}=f\left((v_1,v_2,\dots ,v_m,\dots ,v_k)\right)=s_{cpl}$, and there exists a new state $s^{**}=f\left((v_1,v_2,\dots ,v_{m*},\dots ,v_k)\right)=s_{brk},s^{*}\ne s^{**}$. According to Definition 4, there exists an inter-state migration $s_{cpl}\to s_{brk}$.

• Necessity

There exists an inter-state migration $s_{cpl}\to s_{brk}$, according to Definition 4, there exists key variables.

Assuming no key variables change to a value within an illegal interval, and, according to Definition 6, there exists an intra-state migration $s_{cpl}\to s_{cpl}$.

$s_{cpl}\to s_{cpl}$ contradicts $s_{cpl}\to s_{brk}$,

$\exists v_m=a,a\in \tilde{A}$, $\tilde{A}$ is the illegal interval of a key variable $v_m$. □

Theorem 2.

The inter-state migration $s_{brk}\to s_{cpl}$ happens if and only if the values of all key variables change to values within the legal interval.

Proof. 

• Sufficiency

Let us set the current state:

$$s^{*}=f\left((v_1,v_2,\dots ,v_m,\dots ,v_k)\right)=s_{brk}$$

(6)

According to Definition 9, $\exists v_m=a,a\in \tilde{A}$, $\tilde{A}$ is the illegal interval of a key variable $v_m$.

Let set p be a key point and $b\ge p$, when $v_{m*}=b,b\in A,b>p$, there exists:

$$f\left((v_1,v_2,\dots ,v_m,\dots ,v_k)\right)\ne f\left((v_1,v_2,\dots ,v_{m*},\dots ,v_k)\right))$$

(7)

the current state $s^{*}=f\left((v_1,v_2,\dots ,v_m,\dots ,v_k)\right)=s_{brk}$, and there exists a new state $s^{**}=f\left((v_1,v_2,\dots ,v_{m*},\dots ,v_k)\right)=s_{cpl} \mathit{or} s_{fai}{s}^{*}\ne s^{**}$. If the status is $s_{fai}$, it means that the call to the compensation module failed. Smart contract execution failed. $v_{m*}$ is a key variable of controlling the inter-state migration $s_{brk}\to s_{fai}$. The other key variables become dummy variables.

If the status is $s_{cpl}$, $v_{m*}$ is a key variable of controlling the inter-state migration $s_{brk}\to s_{cpl}$. The key variable that controls the inter-state migration $s_{brk}\to s_{fai}$ becomes a dummy variable.

According to Definition 4, there exists an inter-state migration $s_{brk}\to s_{cpl}$.

• Necessity

There exists an inter-state migration $s_{brk}\to s_{cpl}$, and, according to Definition 5, there exists key variables.

Assuming $\exists v_m=a,a\in \tilde{A}$, $\tilde{A}$ is the illegal interval of a key variable $v_m$, according to Definition 9, there exists an intra-state migration $s_{brk}\to s_{brk}$.

$s_{brk}\to s_{brk}$ contradicts $s_{brk}\to s_{cpl}$,

And no key variables change to a value within an illegal interval, i.e., the values of all key variables change to within the legal interval.

To sum up, the original proposition holds. □

Theorem 3.

There are only two relations between module $T_x$ and module $T_y$ that are mutually independent and strictly recursive.

Proof. 

Let the initial vertices of module $T_x$ and module $T_y$ be $t_x^0$ and $t_y^0$, respectively, and their end vertices be $t_x^e$ and $t_y^e$. We may wish to list all the combinations to prove them one by one.

Firstly, let the current combination of their relationships be:

$$\left\{\begin{array}{c}\hfill \widehat{V_x^e}\cap \widehat{V_y^0}=\widehat{V_x^e}\\ \hfill \widehat{V_y^e}\cap \widehat{V_x^0}=\widehat{V_y^e}\end{array}\right.$$

(8)

The termination node of the current module $T_x$ has the same dimension as the initial vertex of module $T_y$, and the termination node of module $T_y$ and the initial vertex of module $T_x$ describe the same trigger event. So, the two modules form a huge cyclic graph. For module $T_x$, it is a one-way path from the initial vertex to the terminal vertex, but since the terminal vertex of module $T_x$ is the initial vertex of module $T_y$, they will continue to loop, which does not match the actual meaning and does not exist.

Secondly, let the current combination of their relationships be:

$$\left\{\begin{array}{c}\hfill \widehat{V_x^e}\cap \widehat{V_y^0}=\widehat{V_x^e}\\ \hfill \widehat{V_x^e}=\widehat{V_y^0}\\ \hfill \widehat{V_y^e}\cap \widehat{V_x^0}\ne \widehat{V_y^e}\end{array}\right.$$

(9)

Since the termination node of module $T_x$ and the initial node of module $T_y$ have the same dimension, they describe the same event. Therefore, module $T_x$ and module $T_y$ are actually the same module, and there is no relationship between modules.

Finally, let the current combination of their relationships be:

$$\left\{\begin{array}{c}\hfill \widehat{V_x^e}\cap \widehat{V_y^0}\ne \widehat{V_x^e}\\ \hfill \widehat{V_y^e}=\widehat{V_x^0}\\ \hfill \widehat{V_y^e}\cap \widehat{V_x^0}=\widehat{V_y^e}\end{array}\right.$$

(10)

According to the Definition 13, module $T_y$ and module $T_x$ are strictly progressive.

To sum up, the original proposition holds. □

6. Application

In the context of the widespread application of distributed network technology, lightweight blockchain shows unique advantages in improving network security and credibility. Figure 7 shows the operational framework of a lightweight blockchain-based distributed unmanned aerial vehicle (UAV) self-organizing network. This framework uses the consensus mechanism of blockchain and smart contracts to achieve the statistics and update of global credibility by real-time monitoring the behavior of UAV nodes. UAV nodes form a self-organizing network by connecting with each other. In this network, the credibility of nodes is dynamically evaluated by their data-forwarding behavior. After the evaluation result is verified by the consensus mechanism, it is automatically executed through the smart contract, and the global trust view is finally updated. This process fully reflects the ability of blockchain technology to improve transparency and trust in distributed systems. On this basis, the smart contract, as one of the core components of the system, further simplifies the complex processes in network operation. Smart contracts can automatically implement pre-set rules and protocols, such as the incentive mechanism for resource sharing between UAVs or the automatic isolation of faulty nodes. In this section, the VST model is used to describe the life cycle of a smart contract in four phases: creation, deployment, execution, and completion, and the following will illustrate how smart contracts play a practical role in UAV networks through specific application scenarios.

6.1. Creation

The creation phase of a smart contract is the process by which a software engineer transforms a traditional contract into a smart contract code that can be recognized and executed by a computer through a programming language. Generally, creating a smart contract involves defining variables, describing state, and setting conditional response rules. In the VST model, this process can be described as the instantiation of a multidimensional vector V, $V\to S$ corresponding rules, and a directed acyclic graph set T. In conjunction with a common UAV mission contract, we need to perform natural language processing on the contract, extracting its entities, relations and logical structures, and recording and saving the attributes involved in the contract.

Declaration. The first step to create a smart contract is to extract the variables needed for the smart contract from the natural language contract, and declare the key-value pairs. In the UAV mission contract shown in Figure 8, the variables to be declared are shown in

Table 3. Declaration of V.

Variables	Key-Value Pairs
$v_0$	Whether the contract is called: T/F
$v_1$	Party A (Principal)
$v_2$	Party B (Executor)
$v_3$	Task location: [specific location or area]
$v_4$	Task time: [specific date and time]
$v_5$	Communication bandwidth fee: XX$
$v_6$	Task collaboration start time XX$
$v_7$	Additional data package value-added service fee: XX$
$v_8$	Whether received a communication reply: T/F
$v_9$	Whether the next stage of tasks continue to be executed: T/F
$v_{10}$	Whether the drone parameter reset: T/F
$v_{11}$	Drone maintenance cost: XX$
$v_{12}$	Drone Health Status: T/F
$v_{13}$	Whether to terminate task: T/F
$v_{14}$	Liquidated damages: XX$
$v_{15}$	Whether there is any dispute during the task period: T/F
$v_{16}$	Whether the task can be redone: T/F
$v_{17}$	Whether the smart contract state is $s_{cpl}$ when the listener module is called: T/F

. After declaring the variables, it is necessary to define the state-variable mapping relationship, i.e., to define the instantaneous state that can cause the trigger condition, as shown in

Table 4. Declaration of S.

Instantaneous States	Key Variables
$s_0$	$\left(v_0\right)$
$s_1$	$(v_1,v_2,v_3,v_4)$
$s_2$	$(v_1,v_2,v_5,v_6)$
$s_3$	$(v_2,v_4,v_7)$
$s_4$	$(v_1,v_2,v_4,v_8)$
$s_5$	$(v_1,v_2,v_4,v_8,v_9)$
$s_6$	$(v_1,v_2,v_4,v_8,v_9,v_{10},v_{11})$
$s_7$	$(v_1,v_2,v_4,v_{12})$
$s_8$	$(v_1,v_2,v_4,v_{12},v_{13})$
$s_9$	$(v_1,v_2,v_4,v_{12},v_{13},v_{14})$
$s_{10}$	$(v_1,v_2,v_3,v_4,v_5,v_6,v_7,v_8,v_9,v_{10},$$v_{11},v_{12},v_{13},v_{14},v_{15})$
$s_{11}$	$(v_1,v_2,v_3,v_4,v_5,v_6,v_7,v_8,v_9,v_{10},$$v_{11},v_{12},v_{13},v_{14},v_{15},v_{16})$
$s_{12}$	$(v_1,v_2,v_4,v_{17})$
$s_{brk}$	$(v_1,v_2,v_3,v_4,v_5,v_6,v_7,v_8,v_9,v_{10},$$v_{11},v_{12},v_{13},v_{14},v_{15},v_{16},v_{17})$
$s_{fai}$	$(v_1,v_2,v_3,v_4,v_5,v_6,v_7,v_8,v_9,v_{10},$$v_{11},v_{12},v_{13},v_{14},v_{15},v_{16},v_{17})$
$s_{fin}$	$(v_1,v_2,v_3,v_4,v_5,v_6,v_7,v_8,v_9,v_{10},$$v_{11},v_{12},v_{13},v_{14},v_{15},v_{16},v_{17})$

. After the first two steps are completed, the trigger conditions of the smart contract can be declared and a directed acyclic graphical set representing the structure of the trigger conditions of a smart contract can be drawn. The trigger condition declaration of an example UAV mission contract is shown in

Table 5. Declaration of T.

Triggers	States and Variables	Meanings
$t_0$	$(s_0^{*},\left(v_0^{*}\right))$	Contracts are called.
$t_1$	$(s_1^{*},(v_1^{*},v_2^{*},v_3^{*},v_4^{*}))$	Party A will provides the drone to Party B to carry out the task for X months.
$t_2$	$(s_2^{*},(v_1^{*},v_2^{*},v_5^{*},v_6^{*}))$	Party B needs to pay Party A a monthly drone communication bandwidth fee $.
$t_3$	$(s_3^{*},(v_2^{*},v_4^{*},v_7^{*}))$	Party B has to pay for additional data package value-added service fees during the task period.
$t_4$	$(s_4^{*},(v_1^{*},v_2^{*},v_4^{*},v_8^{*}))$	Party B modifies or retrofits the parameters of Party A’s unmanned aerial vehicle during the task period.
$t_5$	$(s_5^{*},(v_1^{*},v_2^{*},v_4^{*},v_8^{*},v_9^{*}))$	Party A is agreeable to Party B’s parameter modifications and modifications during the task period.
$t_6$	$(s_6^{*},(v_1^{*},v_2^{*},v_4^{*},v_8^{*},v_9^{*},$$v_{10}^{*}$, $v_{11}^{*}\left)\right)$	Party B did not compensate Party A for the damage to the drone equipment, nor replied to the default settings of the drone.
$t_7$	$(s_7^{*},(v_1^{*},v_2^{*},v_4^{*},v_{12}^{*}))$	Termination of the task between Party A and Party B during the task period.
$t_8$	$(s_8^{*},(v_1^{*},v_2^{*},v_4^{*},v_{12}^{*},v_{13}^{*}))$	Party A and Party B signed a task termination plan.
$t_9$	$(s_9^{*},(v_1^{*},v_2^{*},v_4^{*},v_{12}^{*},v_{13}^{*},$$v_{14}^{*}\left)\right)$	A party forcibly terminating a contract is required to pay X amount of liquidated damages.
$t_{10}$	$(s_{10}^{*},(v_1^{*},v_2^{*},v_3^{*},v_4^{*},v_5^{*},$$v_6^{*},v_7^{*},v_8^{*},v_9^{*},v_{10}^{*},v_{11}^{*},$$v_{12}^{*},v_{13}^{*},v_{14}^{*},v_{15}^{*}\left)\right)$	During the task period, Party A and Party B have conflicts they need to negotiate.
$t_{11}$	$(s_{11}^{*},(v_1^{*},v_2^{*},v_3^{*},v_4^{*},v_5^{*},$$v_6^{*},v_7^{*},v_8^{*},v_9^{*},v_{10}^{*},v_{11}^{*},$$v_{12}^{*},v_{13}^{*},v_{14}^{*},v_{15}^{*},v_{16}^{*}\left)\right)$	During the task period, Party A and Party B negotiated and resolved the conflict.
$t_{12}$	$(s_{12}^{*},(v_1^{*},v_2^{*},v_4^{*},v_{17}^{*}))$	When the task calls the listener module, the task state is $s_{cpl}$.
$t_{brk}$	$(s_{brk},(v_1^{*},v_2^{*},v_3^{*},v_4^{*},v_5^{*},$$v_6^{*},v_7^{*},v_8^{*},v_9^{*},v_{10}^{*},v_{11}^{*},$$v_{12}^{*},v_{13}^{*},v_{14}^{*},v_{15}^{*},v_{16}^{*},$$v_{17}^{*}\left)\right)$	Task status is in default, pending.
$t_{fai}$	$(s_{brk},(v_1^{*},v_2^{*},v_3^{*},v_4^{*},v_5^{*},$$v_6^{*},v_7^{*},v_8^{*},v_9^{*},v_{10}^{*},v_{11}^{*},$$v_{12}^{*},$ $v_{12}^{*}$, $v_{13}^{*}$, $v_{14}^{*}$, $v_{15}^{*}$, $v_{16}^{*}$, $v_{17}^{*}$))	Task status is stable failure status.
$t_{fin}$	$(s_{cpl},(v_1^{*},v_2^{*},v_3^{*},v_4^{*},v_5^{*},$$v_6^{*},v_7^{*},v_8^{*},v_9^{*},v_{10}^{*},v_{11}^{*},$$v_{12}^{*},v_{13}^{*},v_{14}^{*},v_{15}^{*},v_{16}^{*}$,$v_{17}^{*}\left)\right)$	Task is finished.

, and its directed acyclic graph set is shown in Figure 9. Thus, the process of creating a smart contract from a traditional contract under the VST model is formally completed.

6.2. Deployment

After a smart contract is created, it is packaged and deployed on the chain by a consensus node (miner). The existing technology first stores the contract code directly to the contract address, then the contract address is asymmetrically encrypted, packaged into blocks, and deployed to the main chain. The deconstructed VST model can store the multidimensional vector set, V, state set, S, and graph set, T (split into module $T_x$, point set ${\tau }_x$, and edge set $E_x$) independently.

6.3. Execution

In the execution phase of a smart contract, the contract invoker initiates a transaction to the contract address, and the consensus node (miner) runs the smart contract to be executed in the local sandbox environment. The local sandbox accesses the state of the world through the prophecy machine, and returns the result to the contract invoker after execution, as shown in Figure 10.

In the VST model, since the environment, V, state set, S, and graph set, T, of the smart contract are stored independently in advance, the clause steps of the smart contract can be monitored during the execution process. When a clause is called, the module and vertex corresponding to the clause are returned to the caller in real time, and the instantaneous state of the contract and the corresponding variable key-value pairs are listened to. After the execution of the contract is completed, the result of the computation, the corresponding state and the variable key-value pairs to achieve the result are returned to the caller, as shown in Figure 11. Thus, the execution phase of a smart contract under the VST model has been transformed from a black-box process to a white-box process.

This transformation means that the execution of smart contracts is no longer an opaque black box, but has become a transparent white box, where every step of the execution can be monitored and verified. This enhancement in transparency is crucial for the security and reliability of smart contracts, as it allows developers and users to monitor the execution status of the contract in real time, and to identify and correct potential issues promptly.

Compared with traditional deployment of smart contracts, the VST model offers greater transparency and monitorability, which is one of its main contributions and a key feature that distinguishes it from conventional smart contract deployment. In this way, the VST model enhances the auditability and verifiability of smart contracts, providing new safeguards for the secure execution of smart contracts.

In this example UAV mission contract, if Party B modifies Party A’s drone without Party A’s consent during the task period, Party B must compensate Party A for the damage to the equipment as required. As shown in Figure 8, under the VST model, the above clauses correspond to Module4 and Module5, which are strictly recursive, and Module5 is a supplement to Module4. When Party B renovates Party A’s house without Party A’s consent, the trigger condition is $t_4\to t_{brk}$, followed by $t_{brk}\to t_6$. At this point, a supplement to the example UAV mission contract is executed.

6.4. Completion

A contract is completed when the smart contract no longer executes any of its terms. In the VST model, the “completion phase” of a contract refers to a stable state that reflects not only the success of the execution of the contract, but also the instantaneous state in which the contract has reached a stable state. In the VST model, there are two steady states, $s_{fin}$ and $s_{fai}$, for smart contracts. Each contract has a separate listening module, $T_{end}$, which contains three vertices, $t_{end},t_{fin},t_{fai}$, as shown in Figure 12.

When the smart contract is no longer executing any clause, $t_{end}$ is triggered, and the termination state of the last executed module is checked: if the state is $s_{cpl}$, $t_{fin}$ is triggered, i.e., the contract reaches a stable completion state, $s_{fin}$; if the state is $s_{brk}$, $t_{fai}$ is triggered, i.e., the contract reaches a stable default state, $s_{fai}$.

6.5. Conditional Response Path

In the VST model, after the execution of a smart contract, a conditional response path is returned to the user, which is the set of all triggers triggered during the execution of the contract. Unlike the pre-declared T-chart at the time of contract creation, the condition response path returned after contract execution records the environment and state under which the completion/failure condition was reached. Thus, for both developers and users, each contract call makes experimental sense: suppose that under contract version $C_{v_1}$, user a completes the contract with $t_{fin}=(s_{fin},V_1)$, and user b completes the contract with $t_{fin}=(s_{fin},V_2)$; under contract version $C_{v_2}$, user a completes the contract with $t_{fin}=(s_{fin},V_3)$, while user b completes the contract with $t_{fin}=(s_{fin},V_4)$. Suppose some key variables in $V_1$ have better values than $V_2$, and some key variables in $V_4$ have better values than $V_3$. Then, for user a, it seems that the contract version $C_{v_1}$ better satisfies his interests, while, for user b, the opposite is true; for the developer, it becomes a mechanism design problem to adjust the predefined parameters at each step, balance the preferences of user a and user b, and improve the smart contract so that it can satisfy the interests of most users.

Specifically in the UAV mission contract example in this section, if the contract is executed and the conditional response path is $t_4=(a,b,2021.06.01-2022.05.31,T), t_5=(a,b,2021.06.01-2022.05.31,T,F), t_6=(a,b,2021.06.01-2022.05.31,T,F,T,1000)$, this means that b made alterations to the house while renting a’s property, but a did not agree to the alterations and ordered b to return the house to its original condition and pay 1000. If the owner, a, does not want to modify the drone in the next task period, he/she can improve the contract template, for example, setting the compensation to 10,000 in advance, which increases the user’s modification cost and reduces the possibility of users modifying the drone. Such a change in the contract is to some extent more favorable to the interests of the first party.

7. Conclusions

This paper creatively proposes a formal model of a blockchain smart contract—VST model, focusing on the definition and interpretation of state migration and the trigger condition response mechanism of smart contracts under the VST model. In terms of model validation, this paper verifies the feasibility of the VST model by instantiating a real UAV mission contract into a programmable smart contract form.

Unlike the traditional formal model, the VST model defines the conditional response mechanism of the smart contract, and analyzes the execution logic of the smart contract from a microscopic perspective, which is more capable of explaining the possible supplementary clauses and hierarchical clauses in the traditional contract, and facilitates the implementation of the construction from the smart contract. The VST model supports the deployment of the smart contract environment, state, and trigger conditions to the blockchain, which facilitates the supervision of the contract state and condition response paths during contract execution and helps developers improve smart contracts.

Moving forward, we plan to integrate the system model from Wu’s work [33] to enhance our framework’s data handling capabilities.Addressing the potential vulnerabilities raised, we will analyze the novel attacks from Gao’s work [34] to strengthen our model against such threats. Our future research will focus on ensuring the VST model’s robustness against blockchain attacks, thus safeguarding the system’s integrity.