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.

Wow, it's been a whole month since my last post! That's not good....

While I've been busy with other things lately, I have not been totally ignoring my thesis work. I just haven't been getting as much done as I would have hoped. I spent a couple of weeks pretty much just tossing out thoughts and ideas, noting them down in KDissert, and trying vainly to organize them into a coherent outline. So far, I'm not meeting with too much success on that front. It seems that my meditation on the items I've come up with has raise more questions for me than answers.

I spent some time this month playing around with some of the freely available Z tools. I tried a few Z type-checkers, but the one that comes with the Community Z Tools was the only one I could get to work. ZTC didn't run and fuzz2000 didn't compile. However, I have had success in picking up LaTeX, which seems to be the prefered markup form for Z and VDM. Given the fact that software specifications are written to be printed and the high quality of the documents LaTeX produces, I guess this shouldn't be too surprising.

I've been doing a little more research the past week or two. I spent one Friday afternoon in the BU library failing miserably to find several articles that were in the proceedings of obscure Formal Methods conferences (though I did find a couple of interesting articles on Formal Methods in CS education. I guess I shouldn't be surprised by that. I did later find a few of them available online, thanks to Google and professors such as Jonathan Bowen, who saw fit to archive several years worths of papers, including the revisitation of the Ten Commandments of Formal Methods, on his web site. It's funny how many academic articles you can find online once you have an exact title for which to search.

I've been trying to do some research on other common methods as well. I've found a decent reference on VDM, which I'm starting to look through. I also found a draft specification of Object-Z, an object-oriented extension of standard Z. I was very glad to find this online, because I wanted to read more about Object-Z, but the main book on it costs approximately $1.15 per page (no, that's not an exageration). However, beyond the variations on Z and VDM, formal methods seems to be somewhat balkanized. It seems that Z is the most represented method in the practical literature, with VDM being somewhat common as well, but I don't see much of anything else with any consistency. Statecharts seemed to be big for a while in the early '90s, but I haven't found much on it that was recent. CSP comes up fairly often as well, but I don't know if I'll want to deal with that. It seems to be useful mostly for communications, e.g. networking or IPC, which is a little more complicated than I wanted to get. Plus I don't really know anything about networking or IPC.

I found a few other interesting papers on Z today. One is a Masters thesis including a Z specification describing the relational model of databases. There is also a paper describing the use of Z in a graduate-level course on database design. I've been looking for papers like this, as relational databases are a staple of the type of software I'm interested in.

I think from here I need to start doing some focused reading. The obvious course of action is to start at the end and figure out the application of formal methods to the more pedestrian software I'm looking at. After that, I can worry about the "introductory" material, such as case studies in formal methods use and descriptions of popular methods.

Well, it's time to get back to posting regularly. I've been sort of meditating on where to go now for the last week or so. I've also been kind of busy, so I haven't gotten too much done to report on. Hopefully that will change this week.

I'm working on building a basic outline and expanding it into a real paper. I'm trying to see how FM can be used in small-scale business projects. To do that, I figure I need to examine at least four basic areas: cases where FM have been applied (preferably in non-safety-critical projects), the methods themselves, the tool support for those methods (which will be very important for use by non-experts), and the problem domain, i.e. business software. I'm working on breaking those down into their constituent issues now.

There are several things that concern me here. First, in the formal methods literature, the vast majority of case studies are safety- or security-critical applications. Despite claims of FM leading to lower total project cost, I have seen relatively few cases of serious FM being applied to projects where security and/or safety are not overriding concerns. Since this is precisely the area I'm interested in, it would be nice to have some more real-world (as opposed to academic) case studies to work with.

Another area of concern is tools. There still appears to be a dearth of formal methods tools. Also, it seems that most of the good ones are commercial products which I can't afford, so I obviously won't have any real experience to go on. And, of course, many if not most of the free tools kind of suck. However, I'll mainly be interested in tools for their existence and how they work, so it's not like I'll really be using them too much.

And speaking of tools, I finally got around to installing the Community Z Tools on my system. Honestly, they're not real impressive, but are better than nothing. Right now, it appears that all they have are a JEdit plug-in for editing specification, some export/conversion facilities, and a type checker. This would be fine, if not for the fact that it's such a big pain in the neck to install.