由于自动柜员机需要提供可靠的服务,确保其业务逻辑的正确性具有非常重要的意义.然而,传统的测试方法不能对其正确性进行验证.以相关业务逻辑为具体实例,给出一种基于Spin( Simple Promela Interpreter,一种典型的模型检测工具)的自动柜员机的模型检测方法.介绍如何对自动柜员机业务逻辑进行建模、如何对其主要属性进行描述和验证.实验结果表明了所提方法的可行性.%It is very important to ensure the correctness of the business logic of automatic teller machine because the system ought to provide reliable services. Traditional test methods fail to ensure its correctness. This paper, taking relative logics as concrete instances, proposes a Spin(a typical model checking tool) based ATM model checking method. The paper also introduces how to model ATM business logic and how to describe and verify its important properties. Experiment results show that the proposed method is feasible.
展开▼
