Formal Methods

Installing and Configuring HOL-OCL

I’ve just finished installing/configuring HOL-OCL (except for the X-symbols configuration). This was a pretty complex process and the documentation is pretty scattered. Here’s the flow I followed:

Get HOL-OCL

Install SML/NJ
From: http://www.smlnj.org/dist/working/110.56/index.html
Take a look at INSTALL  — it’s helpful but verbose and not accurate about basic installation

Get these files:
    config.tgz
    boot.<arch>.<os>.tgz  (boot.x86.unix.tgz)
    runtime.tgz
    smlnj-lib.tgz
    MLRISC.tgz
    ml-yacc.tgz
    ml-lex.tgz
    cml.tgz

  1. Create a folder temp for installation source
  2. Unpack config.tgz to config
  3. Put config in temp
  4. Put  from temp/config/* to temp/*  — I don’t think all files are needed here. I just haven’t got around to finding which ones are!
  5. Copy other two tgz files to temp/ folder
  6. Go to temp folder
  7. Rename the main folder containing everything to smlnj
  8. Copy this folder to Isabelle_home/contrib/
  9. Run install.sh

Setting up Isabelle to Use HOL+OCL

Take a look at Section 7.2.1 of HOL-OCL Book
After copying smlnj folder to isabelle_home/contrib/:
Recompile Isabelle using sml/nj :
Overwrite $hol-ocl_dir$/contrib/defs.ML to $isabelle_home$/src/Pure/defs.ML — you can get this file from the hol-ocl installation folder
edit: /usr/local/Isabelle2005/etc/settings — uncomment smlnj portion, comment out polyml portion
Go to isabelle_home
build -m HOL-Complex HOL
this may take a while … sml/nj is a little slow during compilation

get Hol-ocl
Extract to isabelle_home/
Go to isabelle_home/hol-ocl-0.9.0/src
isatool make
set environment variable HOLOCL_HOME

Get ArgoUML
http://argouml.tigris.org/
Java jar file. Easy to run. Works beautifully

Get Dresden OCL1.2 for OCL2
From: http://dresden-ocl.sourceforge.net/index.html
run using: java -jar ocl20parsertools.jar

Take a look at their Publications
http://www.brucker.ch/projects/hol-ocl/
A Model Transformation Semantics and Analysis Methodology for SecureUML.

And now that I’ve done it, I’m not sure I’m going to use it but I may give it a try. It seems promising for a specific area of application of formal methods.

Advertisements

2 thoughts on “Installing and Configuring HOL-OCL”

Comments are closed.