关于原子交换智能合约的规约与验证
计算机科学中的逻辑
2018-11-16 v1 分布式、并行与集群计算
摘要
区块链系统与智能合约提供了在无可信中介（目前支撑众多商业交易）参与下安全实现多方交易的方式。然而，它们通过将信任转移至计算机系统来实现这一点，从而引发了代码是否可信的问题。由错误代码导致高价值损失的实际经验已表明，智能合约的形式化验证可能是有益的。本文研究了简单形式多方交易——原子交换——的规约与验证。我们认为，能够表达多智能体设定中参与者策略性质的逻辑在此概念上是有用的，尽管最终对于我们具体的示例，表达力较弱的时序逻辑设定已足以验证具体实现。这通过若干使用模型检测器验证链上与跨链设定下原子交换智能合约的示例加以说明。
引用
@article{arxiv.1811.06099,
title = {On the specification and verification of atomic swap smart contracts},
author = {Ron van der Meyden},
journal= {arXiv preprint arXiv:1811.06099},
year = {2018}
}