FM Thesis

Yet again, it's been way too long since my last post.  While I have been busy with other things, I haven't been completely slacking off.

I've been reading and browsing through a variety of papers the last few weeks.  I've looked through a few on formal database specification in Z, as I mentioned last time (a couple by de Barros and one by Simpson and Martin).  The basics are actually quite intuitive: a relational database schema maps more or less directly to a Z schema.  The Z schema just allows for a greater level of abstraction and more detailed constraints.

I also looked at a case study using light-weight formal methods to review a GIS/database system (A Case Study using Lightweight Formalism to Review an Information System Specification, by Fiona Polack).  This one used SAZ, a combination of Z with SSADM.  Rather than a verification or design effort, this one was a review carried out more or less in parallel with development.  The goal was, apparently, detection of defects, rather than straight reduction of development costs.

Other than that, I've been trying to build up and organize ideas for the paper.  I've got several general topics I'm thinking of covering.  There's the general FM overview, various case studies, the uses and pro/con arguments, and probably something on tools.  The interesting parts (I hope) will be specific applications of FM to information systems and business type software in particular, as well as some consideration of the methods in "formal methods".  In other words, how to actually apply FM, rather than focusing just on the formalism, which seems quite comon.

OK, enough for tonight.  I'm missing House.