@inproceedings{a9b19ea5772941ef85c9e35c31502011,
title = "Formal verification of automated teller machine systems using SPIN",
abstract = "Formal verification is a technique for ensuring the correctness of systems. This work focuses on verifying a model of the Automated Teller Machine (ATM) system against some specifications. We construct the model as a state transition diagram that is suitable for verification. The specifications are expressed as Linear Temporal Logic (LTL) formulas. We use Simple Promela Interpreter (SPIN) model checker to check whether the model satisfies the formula. This model checker accepts models written in Process Meta Language (PROMELA), and its specifications are specified in LTL formulas.",
author = "Iqbal, {Ikhwan Mohammad} and Dieky Adzkiya and Imam Mukhlash",
note = "Publisher Copyright: {\textcopyright} 2017 Author(s).; 2nd International Conference on Mathematics - Pure, Applied and Computation: Empowering Engineering using Mathematics, ICoMPAC 2016 ; Conference date: 23-11-2016",
year = "2017",
month = aug,
day = "1",
doi = "10.1063/1.4994448",
language = "English",
series = "AIP Conference Proceedings",
publisher = "American Institute of Physics Inc.",
editor = "Dieky Adzkiya",
booktitle = "International Conference on Mathematics - Pure, Applied and Computation",
}