Spi2Java is a model driven development (MDD) framework to semi-automatically generate Java security protocol implementations from verified Spi Calculus formal specifications of such protocols. The aim of the framework is to provide high correctness confidence on the generated code, thus making a step towards bridging the gap between the verified abstract formal models, and their concrete implementations.
The Spi2Java project is mantained on its own website. Please browse to the Spi2Java home page for further information.