I’ve been working on formalization of UML and OCL for some time. Of course, specifications are necessary for formalization but they’re also helpful for learning the tools themselves. If you’re working with UML and/or OCL, you may find these specs helpful:
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:
- Download HOL-OCL from:http://www.brucker.ch/projects/hol-ocl/
- Need SML/NJ because of some datatype deficiency in Poly/ML
Take a look at INSTALL — it’s helpful but verbose and not accurate about basic installation
Get these files:
- Create a folder temp for installation source
- Unpack config.tgz to config
- Put config in temp
- 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!
- Copy other two tgz files to temp/ folder
- Go to temp folder
- Rename the main folder containing everything to smlnj
- Copy this folder to Isabelle_home/contrib/
- 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
Extract to isabelle_home/
Go to isabelle_home/hol-ocl-0.9.0/src
set environment variable HOLOCL_HOME
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.
I’ve worked with Z notation now for a complete specification and here are my thoughts regarding the experience.
- 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.
- 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.
- 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 http://securityengineering.wordpress.com]
Isabelle is a great tool for automated theorem proving. I don’t need to tell you how great. It also comes with a great PDF generating tool which can help you create proof documents really easily. Here’s how you can create PDFs from your THY files:
This is the first formal specification I’ve created using Z Notation. It’s based on the usual Birthday Book example but is a little different. It also has some information regarding use of ZETA for type-checking the units. See links below for the source and generated output.
Here’s the second presentation in the series. It deals with how HOL-Z can be used. It is only a skeletal presentation because honestly, you need to do a lot of reading before you can work with HOL-Z. This is just a rough guideline about the procedure followed. Here’s the link:
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.