A formal proof of correctness of construct association from PROMELA to Java

Suprapto, Retantyo Wardoyo, Belawati H. Widjaja, Reza Pulungan

Research output: Contribution to journalArticlepeer-review

3 Citations (Scopus)


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.

Original languageEnglish
Pages (from-to)313-331
Number of pages19
JournalIAENG International Journal of Computer Science
Issue number4
Publication statusPublished - 2015


  • Constructs association
  • Correctness
  • Equivalence
  • Java
  • Preserving
  • Program graph
  • Semantics
  • Similarity


Dive into the research topics of 'A formal proof of correctness of construct association from PROMELA to Java'. Together they form a unique fingerprint.

Cite this