计算机应用与软件
計算機應用與軟件
계산궤응용여연건
COMPUTER APPLICATIONS AND SOFTWARE
2012年
6期
36-38,50
,共4页
史慧玲%马文可%张新常%张玮
史慧玲%馬文可%張新常%張瑋
사혜령%마문가%장신상%장위
模型检测%线性时态逻辑%自动柜员机
模型檢測%線性時態邏輯%自動櫃員機
모형검측%선성시태라집%자동거원궤
由于自动柜员机需要提供可靠的服务,确保其业务逻辑的正确性具有非常重要的意义.然而,传统的测试方法不能对其正确性进行验证.以相关业务逻辑为具体实例,给出一种基于Spin( Simple Promela Interpreter,一种典型的模型检测工具)的自动柜员机的模型检测方法.介绍如何对自动柜员机业务逻辑进行建模、如何对其主要属性进行描述和验证.实验结果表明了所提方法的可行性.
由于自動櫃員機需要提供可靠的服務,確保其業務邏輯的正確性具有非常重要的意義.然而,傳統的測試方法不能對其正確性進行驗證.以相關業務邏輯為具體實例,給齣一種基于Spin( Simple Promela Interpreter,一種典型的模型檢測工具)的自動櫃員機的模型檢測方法.介紹如何對自動櫃員機業務邏輯進行建模、如何對其主要屬性進行描述和驗證.實驗結果錶明瞭所提方法的可行性.
유우자동거원궤수요제공가고적복무,학보기업무라집적정학성구유비상중요적의의.연이,전통적측시방법불능대기정학성진행험증.이상관업무라집위구체실례,급출일충기우Spin( Simple Promela Interpreter,일충전형적모형검측공구)적자동거원궤적모형검측방법.개소여하대자동거원궤업무라집진행건모、여하대기주요속성진행묘술화험증.실험결과표명료소제방법적가행성.
