采用SPIN的自动柜员机业务逻辑模型检测方法

• 作者: 史慧玲 张新常 张玮 马文可
• 来源期刊: 计算机应用与软件
• 学科: 工学
• 关键词: 模型检测 线性时态逻辑 自动柜员机
• 年，卷（期）: 2012,（6）
• 所属期刊栏目: 基金项目论文
• 页码范围: 36-38,50
• 分类号: TP311.5
• 字数: 3067字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-386X.2012.06.011

摘要

由于自动柜员机需要提供可靠的服务,确保其业务逻辑的正确性具有非常重要的意义.然而,传统的测试方法不能对其正确性进行验证.以相关业务逻辑为具体实例,给出一种基于Spin( Simple Promela Interpreter,一种典型的模型检测工具)的自动柜员机的模型检测方法.介绍如何对自动柜员机业务逻辑进行建模、如何对其主要属性进行描述和验证.实验结果表明了所提方法的可行性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	张新常	山东省计算中心山东省计算机网络重点实验室	2	20	2.0	2.0
2	马文可	山东省计算中心山东省计算机网络重点实验室	2	11	2.0	2.0
3	史慧玲	山东省计算中心山东省计算机网络重点实验室	2	5	2.0	2.0
4	张玮	山东省计算中心山东省计算机网络重点实验室	2	5	2.0	2.0