Skip to content

Latest commit

 

History

History
6 lines (4 loc) · 755 Bytes

README.md

File metadata and controls

6 lines (4 loc) · 755 Bytes

formal-verification-atm-spin

Formal verification of automated teller machine systems using SPIN

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.

Full Article : https://aip.scitation.org/doi/pdf/10.1063/1.4994448