Verifikasi Formal Desain Sistem Transaksi ATM (Automated Teller Machine) Menggunakan Spin (Simple Promela Interpreter)

Iqbal, Ikhwan Mohammad (2016) Verifikasi Formal Desain Sistem Transaksi ATM (Automated Teller Machine) Menggunakan Spin (Simple Promela Interpreter). Undergraduate thesis, Institut Teknologi Sepuluh Nopember.

[img] Text
1212100086-Undergradute Thesis.pdf - Published Version

Download (1MB)

Abstract

Verifikasi formal adalah teknik penting untuk memastikan kebenaran sistem yang diselidiki. Namun, tools pada model pemeriksaan harus memperhatikan perkembangan ruang state dimana hal ini akan mengabaikan teknik praktis dalam teknik penerapannya. Pemodelan dan deskripsi dari Automated Teller Machine (ATM) merupakan pemodelan kasus desain yang khusus dalam sistem yang real time dan safety critical. Sebagai sebuah sistem kontrol yang real time, sistem ATM merupakan sistem dengan tingkat kompleksitas yang tinggi. SPIN (Simple Promela Interpreter) adalah sistem verifikasi generik yang mendukung desain dan proses sistem verifikasi yang asynchronous. Model Pemeriksaan ini, mampu menerima spesifikasi desain yang ditulis dalam bahasa verifikasi PROMELA (Process Meta Language), dan hal tersebut mampu menerima klaim kebenaran atau claim correctness yang ditentukan dalam sintaks dalam LTL (Linear Temporal Logic) sederhana. Dalam penelitian ini akan dilakukan verifikasi terhadap model sistem ATM dengan SPIN model checker

Item Type: Thesis (Undergraduate)
Uncontrolled Keywords: :Verifikasi Formal, SPIN, PROMELA, ATM
Subjects: T Technology > TJ Mechanical engineering and machinery > TJ230 Machine design
Divisions: Faculty of Mathematics and Science > Mathematics > (S1) Undergraduate Theses
Depositing User: ansi aflacha
Date Deposited: 05 Apr 2019 07:16
Last Modified: 05 Apr 2019 07:16
URI: http://repository.its.ac.id/id/eprint/62706

Actions (login required)

View Item View Item