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:


Install SML/NJ
Take a look at INSTALL  — it’s helpful but verbose and not accurate about basic installation

Get these files:
    boot.<arch>.<os>.tgz  (boot.x86.unix.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

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
Java jar file. Easy to run. Works beautifully

Get Dresden OCL1.2 for OCL2
run using: java -jar ocl20parsertools.jar

Take a look at their Publications
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.

Formal Methods, Z Notation

Thoughts on Z

I’ve worked with Z notation now for a complete specification and here are my thoughts regarding the experience.

  1. Now I know why Z is losing clientelle and why software engineers are reluctant to use it in practical scenarios. It has all the problems normally associated with structural programming approach and none of the benefits. It also has all the drawbacks of formal methods and almost none of their benefits.
  2. It’s difficult to organize your thoughts when you’re working with a large enough specification. I saw this in the Usage Rights Document and I’ve seen it in my own work. The individual parts are easier to understand and keep track of but it’s much more difficult to keep the big picture in sight. 
  3. In my opinion, the semi-formal methods (such as UML+OCL approach) or the purely formal methods (such as those supported by Isabelle) are a much better way to go. I have seen the theory HOL-OCL (along with the complete architecture) developed by the guys at ETH, Zurich and I like that approach. It is a more streamlined approach and one that is more likely to be accepted by the industry. I’m not the only one to think along these lines either. The introductory parts of the HOL-OCL book describe why exactly Z has never gained support from the industry and why UML+OCL have succeeded in doing so.

I’ve started working on HOL-OCL and I’ll be reporting my findings and thoughts related to this approach. I know this is yet another shift in direction for me but I believe it’s necessary to try all options and then stick to one. These are just tools and my experience with each passing tool has taught me that the glue in all these formal methods nowadays is Isabelle.

[Mirror post on]

Formal Methods, Z Notation

ZETA Presentation

I’ve just finished creating the first presentation about using ZETA for creation/analysis of Z Notation. It’s a basic presentation and is not meant to be used as a reference. See a good book for Z notation (Using Z is pretty good) and the ZETA site for the tool’s reference. The presentation is more about experience in learning to use these tools.

This is the first in a series of presentations hopefully leading to the complete use of Z Notation for formal verification and specification.

See PDF here