The paper mentions that onece the smart contract is deployed, it can't be modified. What if the smart contract need to be modified due to the changes of laws or regulations? Do you provide solutions for this circumstances?
Hello, Thank you for your questions.
The basic principle is that once a smart contract is deployed, it cannot be modified (because it is blockchain-based).
Therefore, it is important to ensure that there are no errors and contradictions through formal specifications prior to deployment.
As said in the question, if a smart contract needs to be modified due to a change in law or regulation,
Basically, when implementing a smart contract, there is a way to implement it so that it can be upgraded.
The contract address should not change, the information from the existing contract should not disappear, and there should be multiple contracts.
The version must be the same even during the upgrade.
There is also a way to reconnect the chain by cutting the blockchain itself with a hard fork and a soft fork.
Currently, modeling does not provide a solution for this situation.
It seems like a good way to verify by formal modeling a smart contract that can cope with this situation in future research.
Thanks for the question.