[vc_empty_space][vc_empty_space]
Developing translation rules of Java-JML source code to Event-B
Hadiputra F.I.a, Asnar Y.D.W.a, Hendradjaya B.a
a School of Electrical Engineering and Informatics, Institut Teknologi Bandung, Bandung, Indonesia
[vc_row][vc_column][vc_row_inner][vc_column_inner][vc_separator css=”.vc_custom_1624529070653{padding-top: 30px !important;padding-bottom: 30px !important;}”][/vc_column_inner][/vc_row_inner][vc_row_inner layout=”boxed”][vc_column_inner width=”3/4″ css=”.vc_custom_1624695412187{border-right-width: 1px !important;border-right-color: #dddddd !important;border-right-style: solid !important;border-radius: 1px !important;}”][vc_empty_space][megatron_heading title=”Abstract” size=”size-sm” text_align=”text-left”][vc_column_text]© 2014 IEEE.This paper proposes translation rules of Java-JML source code to Event-B. Java Modeling Language (JML), a specification language for Java, provides an ease to make a code-level specification regarding to its similarity with Java syntax. However, the verification tools which support JML still have a lot of limitations. On the other hand, in formal method, Event-B has been frequently used to specify software and hardware systems. Also, its verification tools are widely available and supplements one another. These facts give the opportunity to combine the ease provided by JML and the maturity of Event-B in formal method. In this case, translating Java-JML source code to Event-B could be the way. Thus, systematic translation rules are needed. Through this work, the rules are successfully formulated. Besides, the soundness of the rules are also guaranteed according to its correct-by-construction approach. Then, the rules are also evaluated yielding that unique properties which are required by the Event-B model-assertion, convergence, and enabledness-are properly checked. By using these rules, limitation of verification tools for JML can be supplemented.[/vc_column_text][vc_empty_space][vc_separator css=”.vc_custom_1624528584150{padding-top: 25px !important;padding-bottom: 25px !important;}”][vc_empty_space][megatron_heading title=”Author keywords” size=”size-sm” text_align=”text-left”][vc_column_text]Design by contracts,Event-B,Java,JML,RODIN,Source codes[/vc_column_text][vc_empty_space][vc_separator css=”.vc_custom_1624528584150{padding-top: 25px !important;padding-bottom: 25px !important;}”][vc_empty_space][megatron_heading title=”Indexed keywords” size=”size-sm” text_align=”text-left”][vc_column_text]Design by Contract,Event-B,Formal Method,Java,JML,RODIN,Source Code,Verification[/vc_column_text][vc_empty_space][vc_separator css=”.vc_custom_1624528584150{padding-top: 25px !important;padding-bottom: 25px !important;}”][vc_empty_space][megatron_heading title=”Funding details” size=”size-sm” text_align=”text-left”][vc_column_text][/vc_column_text][vc_empty_space][vc_separator css=”.vc_custom_1624528584150{padding-top: 25px !important;padding-bottom: 25px !important;}”][vc_empty_space][megatron_heading title=”DOI” size=”size-sm” text_align=”text-left”][vc_column_text]https://doi.org/10.1109/ICODSE.2014.7062693[/vc_column_text][/vc_column_inner][vc_column_inner width=”1/4″][vc_column_text]Widget Plumx[/vc_column_text][/vc_column_inner][/vc_row_inner][/vc_column][/vc_row][vc_row][vc_column][vc_separator css=”.vc_custom_1624528584150{padding-top: 25px !important;padding-bottom: 25px !important;}”][/vc_column][/vc_row]