第三方支付的基于ＳＰＩＮ的形式化分析
2008-12-31 00:00:00黎升洪馮艷清
計算機時代 2008年12期
摘要：第三方支付業務在電子商務平臺中的廣泛使用，極大促進了電子商務活動的發展。利用模型檢查工具SPIN、建模語言PROMELA，對第三方支付業務進行形式化建模，然后利用時態邏輯公式LTL描述系統待驗證屬性，最后驗證表明，網上交易在第三方支付的支持下可以順利進行。
關鍵詞：SPIN；第三方支付；形式化；模型檢查
摘要：第三方支付業務在電子商務平臺中的廣泛使用，極大促進了電子商務活動的發展。利用模型檢查工具SPIN、建模語言PROMELA，對第三方支付業務進行形式化建模，然后利用時態邏輯公式LTL描述系統待驗證屬性，最后驗證表明，網上交易在第三方支付的支持下可以順利進行。
關鍵詞：SPIN；第三方支付；形式化；模型檢查
