Pembangkit Model Otomatis dari Bahasa Standar IEC 61131-3 menjadi Model Otomata Berjangka Waktu

RYAN TIRTA SAPUTRA, Dr.-Ing. Awang N. I. Wardana, S.T., M.T., M.Sc. ; Dr.-Ing. Sihana

2018 | Skripsi | S1 TEKNIK FISIKA

Pada proses pengendalian di industri, Programmable Logic Controller (PLC) telah diaplikasikan pada berbagai bidang termasuk pada sistem untuk keselamatan sehingga program PLC yang dibentuk juga ikut berkembang menjadi semakin kompleks. Tahap verifikasi menjadi solusi untuk memastikan agar program PLC yang dibentuk sesuai dengan spesifikasi kendali yang diharapkan. Namun verifikasi manual secara menyeluruh tetap sulit untuk dilakukan, sehingga dibutuhkan suatu sistem yang dapat memverifikasi program PLC terhadap spesifikasi kendali secara otomatis. Dengan demikian, penelitian ini bertujuan untuk membentuk sistem verifikasi otomatis dengan pendekatan model checking. Model checking merupakan teknik verifikasi yang mampu menjamin pemeriksaan secara menyeluruh dan dapat dilakukan secara otomatis menggunakan perangkat lunak model checker. UPPAAL adalah model checker yang dapat digunakan untuk verifikasi suatu sistem real time karena mendukung pewaktuan melalui model formal Timed Automata. Pembentukan model timed automata dari program PLC dengan bahasa standar IEC 61131-3 secara otomatis merupakan fokus dari penelitian ini. Pembangkitan model secara otomatis dilakukan dengan sebuah program yang memanfaatkan metode regular expression. Program tersebut akan mengambil informasi karakteristik PLC dari dokumen program PLC untuk kemudian dibentuk sebagai model timed automata pada dokumen baru. Hasil evaluasi terhadap pembangkit model otomatis menunjukkan bahwa model yang dihasilkan telah menggambarkan karakteristik PLC. Kemampuan model yang dibentuk bergantung pada ukuran program PLC yang diverifikasi, seperti jumlah variabel, jumlah standard function block (SFB) yang digunakan, serta struktur dari program PLC. Hasil studi kasus menunjukkan model dapat digunakan untuk memverifikasi program PLC dengan 5 input dan 1 timer dalam waktu 210 detik.

In industrial control processes, Programmable Logic Controller (PLC) have been applied to various fields including safety systems so PLC programs that are formed also grow to become more complex. The verification stage becomes the solution to ensure that the PLC program is formed according to the expected control specifications. However, manual verification as a whole is still difficult to do, so it takes a system that can verify the PLC program towards the control specification automatically. Thus, this research aims to establish an automatic verification system with a model checking approach. Model checking is a verification technique that can guarantee a thorough check and can be done automatically using the model checker software. UPPAAL is a model checker that can be used to verify a real time system as it supports timing through a formal model of Timed Automata. The formation of timed automata model from PLC program with IEC 61131-3 standard language automatically is the focus of this research. Model generation is automatically performed with a program that utilizes regular expression methods. The program will retrieve the PLC characteristic information from the PLC program document to be formed as a timed automata model on the new document. The evaluation results of the automatic model generator show that the resulting model has depicted the real PLC characteristics. The capabilities of the model formed depend on the size of the verified PLC program, such as the number of variables, the number of standard function block (SFB) used, and the structure of the PLC program. The case study results show the model can be used to verify the PLC program with 5 inputs and 1 timer within 210 seconds.

Kata Kunci : PLC, IEC 61131-3, Timed Automata, Model Checking