Reading and research

Well, this has been a largely unproductive thesis week. I was hoping to get more done, but I had a lot of other things going on.

On Monday, I read a 1998 paper entitled On the Need for Practical Formal Methods. One of the more interesting points was the distinction between "light-weight" and "heavy-duty" formal methods. The idea is that light-weight methods are those that are largely automated and/or do not require a great deal of mathematical acumen to use. Automated consistency checking is a good example, as it can be more or less completely automated and the results are clear: either the specification is consistent, or two or more portions conflict. By way of contrast, automated theorem provers are an example of a heavy-duty method, because automation is less complete. And even if the automation is complete, mechanical theorem provers tend to produce proofs that are not especially easy to understand or work with. Thus some mathematical sophistication is required to make them useful. Model checkers fall in the middle, because setting up the models can be difficult.

The paper also gives a few examples of FM application and a list of guidelines for practical use of FM. Nothing ground-breaking there. Pretty much just the same old tool and integration points. However, it did mention that AMD used formal methods to verify a portion of their 586 processor microcode, which I had not heard before.

In other news, I did a little more thinking and outlining tonight. I also started doing some more on-line research. I'm looking for newer papers now, since most of the ones I have are from the 1990s. I ran a few searches on the ACM's portal, which has an index of all their published articles. It's actually quite handy, since it seems like the ACM and IEEE account for about three quarters (if not more) of the academic computer science articles published in English. The ACM also includes abstracts and a list of references for many of the articles. You can also get full text, if you're wealthy enough to pay for the hundreds of dollars worth of memberships and subscriptions you need to qualify for a free download, or if you're willing to pay $10 per article. I suspect I'll end up just be spending a few Saturdays at Binghamton University and copying them for seven cents a page.

Time to get back to posting

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.