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.
[ 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 SourceForge.net.
