Developing translation rules of Java-JML source code to Event-B

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.