A Formal Proof of Correctness of Construct Association from PROMELA to Java
Penulis/Author
Prof. Dr. Suprapto, M.I.Kom. (1); Prof. Drs. Retantyo Wardoyo, M.Sc., Ph.D. (2); Prof. Dr.-Ing. Mhd. Reza M. I. Pulungan, S.Si., M.Sc. (3); Belawati H. Widjaja (4)
Tanggal/Date
2015
Kata Kunci/Keyword
Abstrak/Abstract
The association between the subset of PROMELA’s constructs (or statements) and the subset of Java’s constructs is intended to provide a collection of rules that can be used as a reference in developing a model of code translator from a PROMELA model to a Java program. The idea arises from the fact that, both PROMELA model and Java program are built (or composed) by various elementary elements called constructs. Although this kind of association has already been introduced in some previous researches, they provided no proofs about its correctness.
In this paper we propose a formal proof of association’s correctness by showing the equivalence (or similarity) of the program graphs for every two associated constructs in the association. The correctness of association means that every two associated constructs in association have equivalent semantics. In addition, at the end of this paper we also introduce a translator tool we have developed based on this association’s definition to translate PROMELA model to Java program.
Rumpun Ilmu
Ilmu Komputer
Bahasa Asli/Original Language
English
Level
Internasional
Status
Dokumen Karya
No
Judul
Tipe Dokumen
Aksi
1
ok-SWBP-IJCS-15.pdf
[PAK] Full Dokumen
2
ok-SWBP-IJCS-15-turnitin.pdf
[PAK] Cek Similarity
3
Surat Pernyataan Paper melibatkan mahasiswa_Suprapto_Filled up.pdf
Dokumen Pendukung Karya Ilmiah (Hibah, Publikasi, Penelitian, Pengabdian)
4
BUKTI KORESPONDENSI JURNAL IAENG (A FORMAL PROOF).pdf
