SafeJML

SafeJML

SafeJML is a dialect of JML designed for specification of Safety Critical Java (SCJ) code.

SafeJML Implementation

The SafeJML implementation is built as an extension to [JAJML]. To install it, first install JAJML, then get the sources for SafeJML from subversion, using the URL: http://refine.eecs.ucf.edu/svn/scjml.

Next, build SafeJML using 'ant build'. The frontend for SafeJML is called SafeJMLChecker and is located inside the drivers package.

SafeJML Duration RAC

The SafeJML Duration annotation and Duration Runtime Assertion Checker is an extension to [JAJML]. The RAC works with SCJ code only. For that, it is currently maintained in a separate branch. To install it, follow the following steps:

1. Follow the instructions on the JastAdd Extensible Java Compiler page to checkout and test the following four projects (Java1.4Frontend, Java1.4Backend, Java1.5Frontend, Java1.5Backend)
2. Checkout the project SafeJML from https://jmlspecs.svn.sourceforge.net/svnroot/jmlspecs/JAJML/branches/SafeJML . This must be checked out into a directory that is a sibling of the directories for Java1.4Frontend, Java1.4Backend, Java1.5Frontend, and Java1.5Backend; that is, they must all be under the same directory.

3. Rename the directory SafeJML to be named JAJML

       mv SafeJML JAJML
   

4. Checkout the project SafeJMLRAC from https://jmlspecs.svn.sourceforge.net/svnroot/jmlspecs/JAJML/branches/SafeJMLRAC . Again this must be checked out into a directory that is a sibling of all the directories checked out in the previous steps.

5. Compile and package the SafeJMLRAC into a jar file by running the build.xml ant build file using the jar option. On a Windows machine, it seems to help if you use -Xms128M -Xmx786M as arguments for the Java Virtual Machine, otherwise the building seems to die. In Eclipse this can be set globally from Window > Preferences and then search for "Installed JREs" (or go to Java > Installed JREs) and then clicking on the particular JRE you run, and then the "Edit..." button, and then paste in -Xms128M -Xmx786M in the box labeled "Default VM arguments". Or you can set it in a particular External Tools Configurations, which you access from the Run > External Tools > External Tool Configurations, and then go to the "JRE" tab, and put in that string under "VM arguments". On Linux, in order to execute the ant command successfully, you need to pass the JVM argument in the $ANT_OPTS environment then run the ant command. This can be done as follows:

   cd SafeJMLRAC
   ANT_OPTS="-Xms128M -Xmx786M"
   ant jar
   

6. Follow the instructions on http://code.google.com/p/scj-jsr302/ to install oSCJ and the FijiVM. FijiVM is available under academic license, so you need to contact the developers to obtain its distribution.

7. To run the SafeJML compiler, you use the command java -jar JAJMLRAC.jar (which was produced in step 3 above) instead of javac.

   1. For example, in examples/miniCDx, replace javac with java -jar JAJMLRAC.jar. The SafeJML RAC Compiler is a complete Java compiler with RAC support for duration annotations. To do that, replace the following commands in section (COMPILE & JAR) in the file (build.sh)

      # COMPILE & JAR
      find ./cdx -name *.java > list
      find ./simulator -name *.java >> list
      javac -cp $FIJI_HOME/lib/scj.jar -d build/ @list    
      cd build/ && find . -name "*.class" | xargs jar cf ../minicdx.jar && cd ..
      rm -rf list
      

with this set of commands

        # COMPILE & JAR
        find ./cdx -name *.java > list
        find ./simulator -name *.java >> list
        java -jar JAJMLRAC.jar -print -cp $FIJI_HOME/lib/scj.jar:./JAJMLRAC.jar -d build/ @list
        cd build/ && sudo jar xf ../jmlrac.jar && find . -name "*.class" | xargs jar cf ../minicdx_safejml.jar && cd ..
        rm -rf list

2. Make sure you copy the following files into the examples/minicdx project: 
  1. `jmlrac.jar`: This file has some supporting classes that need to be built into the system. It is available in the JAJMLRAC/resources folder. Copy this file into the examples/minicdx folder. 
  2. `CheckDurationData.java`: This is a helper file to be able to run RAC on duration annotations. It is available in the JAJMLRAC/resources folder. Copy this file into the examples/minicdx/cdx/cdx folder

1. In order for the duration analysis to execute, initialize the RAC analyzer at the startup of the program. For example, in ImmortalEntry.run(), issue the following call

           CheckDurationData.getInstance().setup();
   

2. In order to view the results of the analysis, issue the following commands towards the end of the software, for example, in Level0Safelet.dumpresults(), issue the following calls:

           CheckDurationData.getInstance().checkResults();
           CheckDurationData.getInstance().printMethods();
           CheckDurationData.getInstance().dumpResults();
   

3. Start using the DurationRAC by annotating methods and running the analysis.

Tests

Run the tests inside testFramework/ as Junit tests.

Acknowledgments

The development of SafeJML was supported in part by NSF grant CCF-0916350 titled ``SHF: Specification and Verification of Safety Critical Java._ The authors also thank Ales Plesk and Purdue team for their support and help. _