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 wrote this article back when I was learning to cope with CSS layout. It’s not the best one around but it’s certainly the simplest. It assumes you’ve been working with CSS for font styles and colours and are comfortable with designing layouts using tables. I uploaded it on my old site but that site is no longer there, so this is an update post.
Title: CSS Layout
Tables are a powerful way of creating complex page layouts. That’s why many people simply refuse to let them go. Now, CSS designs have come a long way and have the same sort of power. Let go of your tables and come see how powerful CSS has become. The main problem I faced when I started learning CSS designs was how to get some of those DIVs floating to the right position while still keeping others in their place. HTML tables made it so easy but they have their drawbacks. I decided to redo my weblog template and write a small article in the meantime. There are a lot of CSS tutorials out there. I’m not going to go into the details of CSS. I’ll just take a design and implement it with precise values to show you just how it’s done. Having said that, be forewarned, this tutorial is not for the faint of heart.
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: