Warning: A non-numeric value encountered in /home/skepticats/www/www/thesis/pathconfig.php on line 2
No Subject - FM Thesis

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.

You can reply to this entry by leaving a comment below. You can send TrackBack pings to this URL. This entry accepts Pingbacks from other blogs. You can follow comments on this entry by subscribing to the RSS feed.

Add your comments #

A comment body is required. No HTML code allowed. URLs starting with http:// or ftp:// will be automatically converted to hyperlinks.