# A Blockchain Solution for Remote Sensing Data Management Model
## 4 Experiment
### Data Provenance  
Another important goal of this system is to complete the traceability of data. From the metadata stored in the block, the remote sensing image data on IPFS can be obtained. In this section, we show the results of using the Remix IDE [38] to achieve provenance. Remix is an IDE that allows us to create, compile, and deploy smart contracts. It also provides an environment for executing transactions and interacting with smart contracts. Firstly, we use Remix to create and deploy our smart contract. To interact with this smart contract, we use the Web3 Provider to connect Remix with our blockchain. In Figure 5, we display the produced remote sensing product information, using Remix.  
Smart contracts play a crucial role in facilitating and automating various aspects of remote sensing data sharing and information services within a blockchain framework. Firstly, developers need to define a smart contract that includes attributes, permission rules, and transaction rules related to remote sensing data. Data providers register their data through the smart contract and store descriptive information and relevant attributes within the contract. This may include the data source, time range, resolution, and other details. Data consumers publish their specific requirements for remote sensing data through the smart contract. Once the attributes and rules between data providers and consumers are automatically matched, the contract will execute the data transaction. This process is supervised and recorded. Through the leveraging of smart contracts, remote sensing data sharing and information services can be automated, streamlined, and made more efficient. Smart contracts bring transparency, immutability, and trust to the data sharing process, creating a secure and reliable environment for stakeholders to collaborate and exchange data within a blockchain network.  
Figure 4: The upload time of remote sensing data to IPFS (own elaboration).  
Formal verification methods refer to a special mathematical-based technique used in the field of computer science, especially in software engineering and hardware engineering. These methods are employed to specify, develop, and verify software and hardware systems, in order to enhance their security, reliability, and robustness. In the context of smart contracts, formal methods can be applied to verify the correctness of the contract code, assisting in preventing costly errors and security breaches. Through the explicit definition of the requirements and specifications of smart contracts, and the use of formal methods with descriptive languages, the functionality of the system can be ensured. Formal analysis methods describe functions that can be used to verify programs. Formal methods employ property specifications to define the properties and requirements that the system should satisfy, ensuring the system's compliance with expected behavior. Formal verification tools are used to check if the contract model satisfies the predefined property specifications. These tools can automatically or semi-automatically detect potential errors, conflicts, or inconsistencies. Finally, based on the results of formal verification, necessary fixes and improvements can be made. [39; 40]