Hendrawan, Ari Ramadhana (2020) Pemodelan dan Verifikasi Penarikan Tunai Automated Teller Machine (ATM) Menggunakan Timed Automata. Other thesis, Institut Teknologi Sepuluh Nopember.
Preview |
Text
06111640000106-Undergraduate_Thesis.pdf Download (2MB) | Preview |
Abstract
ATM (Automated Teller Machine) merupakan salah satu fasilitas yang diberikan oleh bank kepada nasabahnya. Dengan ATM, nasabah dapat melakukan berbagai transaksi seperti penarikan tunai, transfer, cek saldo rekening, dan sebagainya. Di sisi lain, kemampuan ATM tersebut menimbulkan beberapa tindak kriminal seperti pembobolan ATM dan penipuan terhadap nasabah. Oleh sebab itu, kebenaran sistem ATM perlu dijamin agar keamanannya terjamin. Dengan demikian, pada Tugas Akhir ini, kebenaran dan keamanan dari sistem ATM diuji dengan verifikasi formal. Verifikasi formal adalah teknik untuk memastikan secara matematis bahwa model dari suatu sistem memenuhi suatu spesifikasi. ATM merupakan sistem real time sehingga dipilih model yang sesuai yaitu timed automata. Pada Tugas Akhir ini, pertama dibuat swimlane diagram yang dibuat berdasarkan langkah penarikan tunai ATM. Selanjutnya membuat model timed automata dan mengkonstruksi sembilan spesifikasinya. Setelah itu, timed automata diverifikasi terhadap sembilan spesifikasi tersebut dengan menggunakan UPPAAL. Dari hasil verifikasi tersebut dapat ditarik kesimpulan bahwa kebenaran sistem ATM terjamin.
========================================================================================================================
This study was conducted to verify the system of ATM (Automated Teller Machine) which is a facility provided by bank. Various transactions can be done by using ATM, including cash withdrawal, payment, and transfer. However, in spite of its function, ATM can also be a target of crime such as cash robbery and frauds. Therefore, the correctness of ATM and its security is essential and for that reason, formal verification is needed. Formal verification is a technique to ensure the model of a system to corroborate a certain specification. ATM has a time variable on its system, therefore timed automata can be used as a model of ATM. In this Final Project, swimlane diagram is constructed based on the ATM cash withdrawal steps. Next, we construct a timed automata model and design the nine specifications. Then, timed automata were verified against these nine specifications using UPPAAL. From the verification results, it can be concluded that the security of the ATM system is guaranteed.
| Item Type: | Thesis (Other) |
|---|---|
| Additional Information: | RSMa 511.8 Hen p-1 • Hendrawan, Ari Ramadhana |
| Uncontrolled Keywords: | Automated Teller Machine, verifikasi formal, timed automata, UPPAAL |
| Subjects: | Q Science > QA Mathematics |
| Divisions: | Faculty of Mathematics and Science > Mathematics > 44201-(S1) Undergraduate Thesis |
| Depositing User: | Ari Ramadhana Hendrawan |
| Date Deposited: | 19 Aug 2020 07:04 |
| Last Modified: | 20 Jul 2023 14:18 |
| URI: | http://repository.its.ac.id/id/eprint/79180 |
Actions (login required)
 |
View Item |