Formal Methods Tools and Applications

This project has developed the RAISE tools and produced a number of case studies involving their use.

The RAISE tools are based on a type checker, rsltc, for the RAISE Specification Language (RSL). The type checker is portable across Unix and PC platforms and is available free from here. There are ready-built binaries for Linux (i386), Windows and Sparc/Solaris. The source code is also available, as is a user and installation guide available for download or as html.

The basic type checker has been extensively extended by UNU/IIST fellows:

     

  • Ms He Hua of Peking University, China, wrote a pretty printer.

     

  • Tan Xinming of Wuhan Jiaotong University, China, wrote a "confidence condition" generator.

     

  • Ke Wei of Academia Sinica, China, wrote a translator to Standard ML.

     

  • Ahn Yong Jun of Kim Il Sung University, DPR Korea, wrote a translator to C++.

     

  • Aristides Dasso of San Luis University, Argentina, wrote a translator to PVS.

     

  • Ms Ana Funes of San Luis University, Argentina, wrote a translator from UML to RSL.

     

  • Juan Perna of San Luis University, Argentina, wrote a translator from UML to SAL, and Ms Ana Garis, also from San Luis University, wrote a user guide for that translator.

These extensions are all included in the rsltc tool. The SML translator needs some extra files, the C++ translator needs some library files, and the PVS translator also needs a library file. The translator from UML is here.

The rsltc tool is written using the Gentle Compiler Construction System. This is well documented and free for educational use.

The RAISE tools are also available from the UNU/IIST ftp site ftp.iist.unu.edu, in /pub/RAISE/rsltc. Log in as "anonymous".