ABSTRAKSI: Automated Teller Machine (ATM) merupakan alat transaksi keuangan yang sudah umum dipergunakan oleh instansi keuangan untuk melayani pelanggan. Fungsi ATM sangat kritis, sehingga butuh metode pemodelan sistem yang akurat yaitu metode formal.
Metode formal dapat menghasilkan spesifikasi yang tidak ambigu, konsisten, dan lengkap, karena menggunakan deskripsi matematis dalam setiap penjabaran kebutuhan sistem. Salah satu metode spesifikasi secara formal adalah B-Method, yang dirancang untuk membangun spesifikasi sistem dan telah banyak digunakan untuk membangun dan mengembangkan sistem yang bersifat kritis. B-Method menggunakan B sebagai bahasa spesifikasi. B-Method memiliki banyak tool yang dapat menunjang pembangunan spesifikasi serta pembuktian dalam B-Method.
Tugas akhir ini mengkhususkan diri pada analisis keamanan transaksi yang terjadi pada mesin ATM dan Bank sebagai pusat data dari ATM. Dasar untuk membuat spesifikasi diperoleh dari simulasi sistem ATM yang kemudian dimodifikasi sesuai dengan hasil pengamatan langsung pada mesin ATM di dunia nyata. Hasil penelitian menunjukkan bahwa sistem ATM yang memenuhi persyaratan keamanan dapat dimodelkan secara formal dengan B-Method.
Kata Kunci : B-Method, B, metode formal, ATM, spesifikasiABSTRACT: Automated Teller Machine (ATM) is a tool of financial transactions that have been commonly used by financial institutions to serve the customer. ATM has critical function, so the it need an accurate system modeling method such as formal methods.
Formal methods can produce unambiguous specifications, consistent, and complete, because it uses a mathematical description of each system needs. One of the formal specification method is the B-Method, which is designed to build the system specifications and has been widely used to build and develop a system that is critical. B-Method using B as a specification language. B-Method has many tools that can support the development of the specification, verification in the B-Method.
This final task specializes in security analysis of transactions at the ATM machines and Banks as the data center from an ATM. Basis for the specification obtained from the simulation of ATM systems which is then modified in accordance with the results of direct observations on the ATM machines in the real world. Result of the research in this final project shows that ATM system that can satisfy the safety requirement can be formal modelled with B-Method.
Keyword: B-Method, B, formal method, ATM, specification