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