VERIFIKASI DESAIN PEMODELAN LIFT MENGGUNAKAN PROMELA

Agus Heri, Theodorus Eric

Abstract


This article discusses the lift system modeling using Promela language and use the software SPIN to verify the design. The process begins with the specification (formally), implementation, and validation. Spin indicates that the design is correct and has been proven to be verified. One reason the use of Spin is its ability to perform the verification process. Keywords: Modeling, System, Elevator, Promela, Spin  

Abstrak

Artikel ini membahas pemodelan sistem lift dengan menggunakan bahasa Promela dan menggunakan perangkat lunak SPIN untuk memverifikasi desainnya. Prosesnya dimulai dengan spesifikasi (secara formal), implementasi, dan validasi. Spin menunjukkan bahwa desain telah benar dan telah dibuktikan dengan diverifikasi. Salah satu alasan penggunaan Spin adalah kemampuannya untuk melakukan proses verifikasi.

 

Kata Kunci: Pemodelan, Sistem, Lift, Promela, Spin


Full Text:

PDF

References


Bell Lab. Basic Spin Manual. http://cm.bellabs.com/cm/cs/what/spin/Man/Basic Spin Manual.html.[1997]

Hoare, C, A, R,. (1978) Communicating Sequential Processes. The Queen`s University Belfast, Northern Ireland.

Rahardjo, B,. (1999) Penggunaan Formal Methods Dalam Disain Perangkat Keras. PPAU-ME I. [Januari 1999].


Refbacks

  • There are currently no refbacks.


Copyright (c) 2007 JURNAL COMPUTECH & BISNIS