摘要
第三方支付业务在电子商务平台中的广泛使用,极大促进了电子商务活动的发展。利用模型检查工具SPIN、建模语言PROMELA,对第三方支付业务进行形式化建模,然后利用时态逻辑公式LTL描述系统待验证属性,最后验证表明,网上交易在第三方支付的支持下可以顺利进行。
出处
《计算机时代》
2008年第12期23-25,共3页
Computer Era
参考文献5
-
1Clarke E M, Grumberg O, Peled D A. Model Checking[M]. London,England: MIT Press,1999.
-
2Baier C, Katoen J. Principles of Model Checking[M].London, England:The MIT Press,2008.
-
3Ben-ari M. Principles of the Spin Model Checker[M]. London: Springer-Verlag,2008.
-
4Holzmann,J G. Spin Model Checker:Primer and Reference Manual[M].Addison-Wesley Professional,2003.
-
5黎升洪,缪淮扣,张新林.线性时态逻辑中的特性模式[J].计算机应用,2006,26(8):1912-1915. 被引量：9
二级参考文献9
-
1CLARKE EM,SCHLINGLOFF BH.Model Checking[A].Handbook of Automated Reasoning[C].Band Ⅱ,S.Elsevier,2001.1637 -1790.
-
2BERARD B,BIDOIT M,FINKEL A.Systems and Software Verification:Model-Checking Techniques and Tools[M].Berlin:Springer,1999.
-
3KRIPKE SA.Semantical considerations on modal logic[J].Acta Philosophica Fennica,1963,16:83-94.
-
4PNUELI A.The Temporal Semantics of Concurrent Programs[A].Proceedings of the International Sympoisum on Semantics of Concurrent Computation,Lecture Notes In Computer Science[C].SpringerVerlag,1979,Vol 70.
-
5BEN-ARI M,PNUELI A,MANNA Z.The Temporal Logic of Branching Time[J].Acta Informatica,1983,20(3):207-226.
-
6EMERSON EA,HALPERN JY."Sometimes" and "Not Never" revisited:on branching versus linear time temporal logic[J].Journal of the ACM,1986,33(1):151-178.
-
7HOLZMANN GJ.Spin Model Checker:The Primer and Reference Manual[M].New York:Addison Wesley,2003.608.
-
8HOLZMANN GJ.Design and validation of computer protocols[M].London:PRENTICE-HALL,1991.22 -78.
-
9HOLZMANN GJ.The Model Checker SPIN[J].IEEE transactions on software engineering,1997,23(5).
共引文献8
-
1黎升洪,冯艳清.SPIN语义引擎执行方式研究[J].计算机与现代化,2009(11):112-115. 被引量：1
-
2周慧.计算树逻辑特性模式研究[J].计算机工程,2009,35(23):68-70. 被引量：3
-
3张丹,伦立军.基于LTL的交通灯系统形式化描述方法[J].哈尔滨师范大学自然科学学报,2009,25(6):89-92. 被引量：1
-
4李春林,任勇伟,孙正平,肖娟.住宅小区大型地下车库智能灯光导航与用电节能系统[J].智能建筑电气技术,2014,8(6):104-107. 被引量：3
-
5孙二杰,石震,李伟,肖娟,王敬.大型公共地下停车场智能管理系统[J].现代建筑电气,2015,6(2):50-53. 被引量：2
-
6舒新峰,张炎龙,孙林泽.基于Spin的地铁门控制系统建模与验证[J].西安邮电大学学报,2015,20(5):57-61. 被引量：1
-
7冯艳清,熊爱金,周慧.基于形式化分析的信号处理模块设计[J].电脑编程技巧与维护,2022(2):170-172.
-
8温文海,黄培东,王磊,汤建明,李兵,梁弘文.大型停车场智能管理系统[J].科技经济导刊,2016(1):31-32.
同被引文献18
-
1肖美华,薛锦云.基于SPIN/Promela的并发系统验证[J].计算机科学,2004,31(8):201-203. 被引量：20
-
2薛锐,冯登国.安全协议的形式化分析技术与方法[J].计算机学报,2006,29(1):1-20. 被引量：60
-
3黎升洪,缪淮扣,张新林.线性时态逻辑中的特性模式[J].计算机应用,2006,26(8):1912-1915. 被引量：9
-
4Lu Shiyong, Smolka S A. Model checking the secure electronic transaction (SET) protocol[C]// Proceedings of the 7th International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems. 1999:358-365.
-
5Holzmann G J. The SPIN Model Checker: Primer and Reference Manual[M].Addison-Wesley, 2003.
-
6Bella G, Massacci F, Paulson L. Verifying the SET registration protocols[J].IEEE Journal on Selected Areas in Communications, 2003,21(1):77-87.
-
7Ruiz M C, Cazorla D, Cuartero F, et al. Analysis of the SET E-commerce protocol using a true concurrency process algebra[C]// Proceedings of the 2006 ACM Symposium on Applied Computing. 2006:879-886.
-
8张若岩,刘晓霞,张宏.SET协议形式化模型的建立和安全性分析[J].计算机应用与软件,2009,26(5):81-84. 被引量：1
-
9黎升洪,冯艳清.SPIN语义引擎执行方式研究[J].计算机与现代化,2009(11):112-115. 被引量：1
-
10周慧.计算树逻辑特性模式研究[J].计算机工程,2009,35(23):68-70. 被引量：3
-
1陈大伟,董荣胜,郭云川,古天龙.IKEv2协议的SPIN模型检测[J].计算机工程,2006,32(5):164-166. 被引量：9
-
2刘正新.浅谈SPIN模型检测的发展及工作原理[J].消费电子,2013(8):64-64. 被引量：1
-
3杨柳.B/S系统数据完整的检查与约束[J].湘潭师范学院学报（自然科学版）,2007,29(4):24-26.
-
4徐兴旺.探析央行第三方支付限制举措[J].消费电子,2014(7):95-95.
-
5王旭磊,王宝海,孙春薇.银行与第三方支付平台的竞合关系分析[J].华南金融电脑,2007,15(8):53-55. 被引量：9
-
6张雪超.第三方支付革新的转折点[J].互联网天地,2010(5):52-55.
-
7陈文伟,钟鸣.示例学习的信息理论以及逻辑公式的生成[J].国防科技参考,1993,14(2):61-67.
-
8夏友平.两招搞定自助接入第三方支付按钮[J].电子商务世界,2005(9):78-79.
-
9Windows7兼容性检查工具变身成特洛伊木马[J].软件和信息服务,2010(6):10-10.
-
10桂小庆,张俊,张晓民,于鹏飞.时态主题模型方法及应用研究综述[J].计算机科学,2017,44(2):46-55. 被引量：10
