B2jml : a sound translation from the b language into the java modeling language (jml).

We propose to define a sound translation from Event into JML, its implementation as the tool EventB2Jml. The proposed work will enable the B refinement calculus community to do static analysis and verification of B models (called machines) by using JML analysers and verification tools. Hence, given the popularity of JML and the automation power of the existing JML tools, a wider range of problems and audiences could fall within the scope of EventB provers.