[1] 贺海武, 延安, 陈泽华. 基于区块链的智能合约技术与应用综述[J]. 计算机研究与发展, 2018, 55(11):2452-2466. He H W, Yan A, Chen Z H. Survey of smart contract technology and application based on blockchain[J]. Journal of Computer Research and Development, 2018, 55(11):2452-2466. (in Chinese) [2] Szabo N. Smart contracts in essays on smart contracts, commercial controls and security[EB/OL]. 1994[2020-09-25]. http://www.fon.hum.uva.nl/rob/Courses/InformationInSpeech/CDROM/Literature/LOTwinterschool2006/szabo.best.vwh.net/smart.contracts.html. [3] Buterin V. A next-generation smart contract and decentralized application platform[EB/OL]. 2014[2020-09-26]. https://www.zybuluo.com/Gebitang/note/1039458. [4] 邱欣欣, 马兆丰, 徐明昆. 以太坊智能合约安全漏洞分析及对策[J]. 信息安全与通信保密, 2019(2):44-53. Qiu X X, Ma Z F, Xu M K. Ethereum smart contract security vulnerability scenario analysis[J]. Information Security and Communications Privacy, 2019(2):44-53. (in Chinese). [5] 赵延红, 原宝华, 梁军. 区块链技术在医疗领域中的应用探讨[J]. 中国医学教育技术, 2018, 32(1):1-7. Zhao Y H, Yuan B H, Liang J. Application of blockchain technology in medical field[J]. China Medical Education Technology, 2018, 32(1):1-7. (in Chinese) [6] 何源源. 数字版权保护中的区块链智能合约法律规制研究[D]. 开封:河南大学, 2019:1-35. [7] DuPont Q. Experiments in algorithmic governance:a history and ethnography of "The DAO", a failed decentralized autonomous organization[M]. Bitcoin and Beyond, 2017:157-177. [8] Bai X, Cheng Z, Duan Z, et al. Formal modeling and verification of smart contracts[C]//Proceedings of 20187th International Conference on Software and Computer Applications, 2018:322-326. [9] Alt L, Reitwießner C. SMT-based verification of solidity smart contracts[C]//International Symposium on Leveraging Applications of Formal Methods. Cham:Springer, 2018:376-388. [10] 王璞巍, 杨航天, 孟佶, 等. 面向合同的智能合约的形式化定义及参考实现[J]. 软件学报, 2019, 30(9):2608-2619. Wang P W, Yang H T, Meng J, et al. Formal definition for classical smart contracts and reference implementation[J]. Journal of Software, 2019, 30(9):2608-2619. (in Chinese). [11] Solidity-the official documentation of Solidity 0.7.0 documentation[EB/OL]. 2019[2020-9-25]. https://solidity.readthedocs.io/en/v0.7.1/. [12] Bengtsson J, Larsen K, Larsson F, et al. UPPAAL-a tool suite for automatic verification of real-time systems[C]//International Hybrid Systems Workshop. Berlin, Heidelberg:Springer, 1995:232-243. [13] 郭华, 庄雷, 张习勇. UPPAAL——一种适合自动验证实时系统的工具[J]. 微计算机信息, 2006(5X):52-54. Guo H, Zhuang L, Zhang X Y. UPPAAL-a tool suit for automatic verification of real-time systems[J]. Control & Automation, 2006(5X):52-54. (in Chinese). [14] 欧阳丽炜, 王帅, 袁勇, 等. 智能合约:架构及进展[J]. 自动化学报, 2019, 45(3):445-457. Ouyang L W, Wang S, Yuan Y, et al. Smart contracts:architecture and research progresses[J]. Acta Automatica Sinica, 2019, 45(3):445-457. (in Chinese). [15] Liu J, Liu Z. A survey on security verification of blockchain smart contracts[J]. IEEE Access, 2019, 7:77894-77904. [16] 倪远东, 张超, 殷婷婷. 智能合约安全漏洞研究综述[J]. 信息安全学报, 2020, 5(3):78-99. Ni Y D, Zhang C, Yin T T. A survey of smart contract vulnerability research[J]. Journal of Cyber Security, 2020, 5(3):78-99. (in Chinese). [17] Dannen C. Introducing Ethereum and Solidity[M]. Berkeley:Apress, 2017:69-88. [18] Luu L, Chu D H, Olickel H, et al. Making smart contracts smarter[C]//Proceedings of 2016 ACM SIGSAC Conference on Computer and Communications Security, 2016:254-269. [19] 陈伟, 薛云志, 赵琛, 等. 一种基于时间自动机的实时系统测试方法[J]. 软件学报, 2007, 18(1):62-73. Chen W, Xue Y Z, Zhao C, et al. A method for testing real-time system based on timed automata[J]. Journal of Software, 2007, 18(1):62-73. (in Chinese) [20] 李力行, 金芝, 李戈. 基于时间自动机的物联网服务建模和验证[J]. 计算机学报, 2011, 34(8):1365-1377. Li L X, Jin Z, Li G. Modeling and verifying services of Internet of things based on timed automata[J]. Chinese Journal of Computers, 2011, 34(8):1365-1377. (in Chinese). [21] Bengtsson J, Yi W. Timed automata:semantics, algorithms and tools[C]//Advanced Course on Petri Nets. Berlin, Heidelberg:Springer, 2003:87-124. [22] Zhu X Y, Yan R, Gu Y L, et al. Static optimal scheduling for synchronous data flow graphs with model checking[C]//International Symposium on Formal Methods. Cham:Springer, 2015:551-569. [23] Pnueli A. The temporal logic of programs[C]//The 18th Annual Symposium on Foundations of Computer Science, IEEE, 1977:46-57. [24] Novy D. Python-solidity-parser[EB/OL]. 2019[2020-07-15]. https://github.com/ConsenSys/python-solidity-parser. [25] Zuo H B. The example of auction[EB/OL]. 2019[2020-08-03]. https://soliditycn.readthedocs.io/zh/develop/solidity-by-example.html. [26] Stewart-Frantz K. FlightSurety-DApp[EB/OL]. 2019[2020-09-12]. https://github.com/jeroat-github/FlightSurety-DApp/tree/master/contracts. |