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

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.

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.