Analysis and Checking of Internet Banking Based on Safety Transition System

摘要：

The temporal logic of actions is a logic for specifying and reasoning about concurrent systems.One kind of logic brought forward by Leslie Lamport1.And its syntax and complete formal semantics are summarized in about a page.TLA is extremely powerful,both in principle and in practice.In the process of researching Intemet banking system we put forward safety transition condition,safety action and safety transition system based on TLA;then,specify Internet banking system using TLA+ which is based on safety transition system.The specification is checked by TLC,and the results show that the system based on safety transition is more secure.

关键词： TLA Safety transition condition Safety action Safety transition system Intemet banking

作者: Wan Liang Huang Yiwang Li Xiang

作者单位: Institute of Computer Software and Theory,Guizhou University,Guiyang,Guizhou 550025,China

会议类型: 国际会议

会议名称: 2008年国际电子商务、工程及科学领域的分布式计算和应用学术研讨会(2008 International Symposium on Distributed Computing and Applications for Business Engineering and Science)

会议地点: 大连

会议语种:英文

页码: 907-911

在线出版日期: 2008-07-27（万方平台首次上网日期，不代表论文的发表时间）