3 Citations (Scopus)

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.

Original languageEnglish
Title of host publicationInternational Conference on Mathematics - Pure, Applied and Computation
Subtitle of host publicationEmpowering Engineering using Mathematics
EditorsDieky Adzkiya
PublisherAmerican Institute of Physics Inc.
ISBN (Electronic)9780735415478
DOIs
Publication statusPublished - 1 Aug 2017
Event2nd International Conference on Mathematics - Pure, Applied and Computation: Empowering Engineering using Mathematics, ICoMPAC 2016 - Surabaya, Indonesia
Duration: 23 Nov 2016 → …

Publication series

NameAIP Conference Proceedings
Volume1867
ISSN (Print)0094-243X
ISSN (Electronic)1551-7616

Conference

Conference2nd International Conference on Mathematics - Pure, Applied and Computation: Empowering Engineering using Mathematics, ICoMPAC 2016
Country/TerritoryIndonesia
CitySurabaya
Period23/11/16 → …

Fingerprint

Dive into the research topics of 'Formal verification of automated teller machine systems using SPIN'. Together they form a unique fingerprint.

Cite this