Iqbal, Ikhwan Mohammad (2016) Verifikasi Formal Desain Sistem Transaksi ATM (Automated Teller Machine) Menggunakan Spin (Simple Promela Interpreter). Undergraduate thesis, Institut Teknologi Sepuluh Nopember.
Preview |
Text
1212100086-Undergradute Thesis.pdf - Published Version Download (1MB) | Preview |
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 > 44201-(S1) Undergraduate Thesis |
| 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 |