[ main | license | developers ]

AutoJML is a JML specification generator. It generates specifications based on other, higher level, specification formalisms such as UML state diagrams, or security protocol specifications. The output is a combination of Java skeleton code and JML class and method specifications. JML stands for the Java Modeling Language.

AutoJML was initially written in the context of a research project in 2002/2003 by Engelbert Hubbers and Martijn Oostdijk of the Security of Systems group at Radboud University in Nijmegen, The Netherlands.

AutoJML takes as input finite state machine specifications in its own XML format. The back-end of AutoJML is written in Java. However, using XSL stylesheets as a front-end, it can handle some typical input formalisms such as Uppaal specifications and UML state diagrams in OMG XMI format (only tested using ArgoUML output).

An extension to also read security protocol specifications in the CAPSL input format was added in 2003.

Aleksy Schubert contributed to the project in 2006 by adding a specification generator for the SSH protocol.

AutoJML is now an Open Source project hosted at

Hosted by SourceForge Support This Project Valid XHTML 1.1 Valid CSS!
© 2006 SoS group, ICIS, Radboud University; last modified: Saturday November 25, 2006.