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 AbstrakArtikel 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
Copyrights © 2015