Design, Formal Methods, resources

UML and OCL Official Specifications

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:

UML 2.0 Infrastructure Document v2.1.1
OCL 2.0 Sepcification

Advertisements
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.

Articles, Design, Tutorials, Typography, Web

CSS Layout

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

Abstract:
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.

Source in .zip

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 http://securityengineering.wordpress.com]