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, 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.

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.

On Thursday and Friday, I read through a 1997 paper comparing Z and VDM. This is kind of an interesting thing to do because they are probably the two most widely used and recognized formal methods. I don't know much about VDM, but apparently the underlying principles of it are not all that terribly different from Z. In addition to the general discussion, the author compared tool support for the two methods (which seems somewhat limited in both cases) and tried to compare the results seen in projects using them. However, he only chose to compare CICS and CDIS, i.e. just two data points, which is not especially useful.

Yesterday and today (I didn't accomplish anything on Saturday), I just spent a little time trying to outline a concrete plan to procede from here. By now I have a pretty good idea of what material I have, so now I'm trying to figure out what I need to get in terms of research and what I can do with what I already have. In particular, I need to start picking out some case studies and analyzing the results. However, first I want to find some more commercially-oriented cases to look at. The international survey had a few, but pretty much everything else is a safety- or security-critical project.

So I'm going to spend the next couple of days trying to plan a direction for the remainder of my research and, hopefully, hunting for some sources. That should allow me to be a little more productive from here on out. It will also give me a nice break from the constant reading. I swear, I can only read so many journal articles before my brain starts to turn to mush. I've really been running out of steam on that front the past couple of weeks.

Today I read a couple of relatively short papers. The first one was Why Are Formal Methods Not Used More Widely?, by Knight, DeJong, Gibble, and Nakano. This paper is basically a study of whether or not there is anything to the popular notion that formal methods are not for real-world projects.

The study is divided into two parts. The first presents a sort of framework for evaluating the usefulnes of formal methods. There are several points around which the framework is stated, but the gist of it is that formal methods should complement existing development practices, rather than clashing or insisting on replacing them. And, of course, this goes for tools as well as practices. From this general idea, the authors derive a list of more concrete criteria for evaluating a formal method.

The second part of the paper is a case study of a control system for a research nuclear reactor at a university. The system was specified using three different formal methods: Z, Statecharts, and PVS. These formal specifications were then examined by a team of nuclear engineers and a team of computer scientists (who lacked extensive training in FM). The results were mixed, but the general consensus was that the formal specifications were certainly better and more reliable than the natural language ones previously used.

The second paper was short article form 1999 by Chechik and Wong entitled Formal Methods When Money is Tight. This one is about how to make formal methods useful for commercial projects, where short-term costs and development time are considered more important than product reliability. Basically, most of the points were related to making FM more accessible and easier to use, especially in terms of integrating with existing methods. The idea is to use formal methods in a way that allows tem to provide concrete, short-term benefits, as opposed ot nebulous reliability increates that are supposed ot eventually trickle down to reduced costs.

Another potential source of short-term cost savings is leveraging the strict semantics of formal description languages for automated development of test cases. The authors summarized a case study they did at Nortel that involved a tool that supported formal specification and test generation. Of course, not all methods provide that, but it certainly sounds nice.

I read and took notes on two papers today. The first was Kate Finney and Norman Fenton's 1996 paper Evaluating the Effectiveness of Z: Claims Made About CICS and Where to Go From Here. It basically critiques the claims made about the benefits IBM saw from using Z in the respecificatino or parts of CICS. The more impressive claims were that the parts of the system which used Z saw 2.5 times fewer defects and that the overall project cost was reduced by 9%. Because of this, CICS is (or, at least, was) often viewed as the poster-project for formal methods success.

Basically, the paper points out that this optimism is unfounded. There is (or was - I've not seen any follow-up studies) insufficient evidence to evaluate these claims. Basically, this is because CICS was not a proper experiment. The literature is unclear on what was being compared to what and how valid those comparisons were. For example, the 9% cost saving figure seems to appear pretty much out of thin air, with no indication how it was calculated. So while CICS seems to be a success story, it should be viewed with caution.

The second paper is a 2002 article by Carol Smidts, Xin Huang, and James C. Widmaier entitled Producing Reliable Software: An Experiment. This one is interesting because it involves having two different teams independently develop the same system using different methods. There was a formal methods team that used Haskell and Specware and a conventional team the using Carnegie Melon SEI Capability Maturity Model (CMM) level 4. They were each separately contracted to build a card access system from the same specification. The contract specified reliability levels and required process documentation, design documents, and test plans. The reliability of the actual software was tested by a third party using automated test suites.

The results of both teams were pretty dismal. Neither one got close to the target 0.99 reliability for "level 1," i.e. critical, defects, with the formal team getting 0.77 and the CMM team 0.56. Furthermore, the formal methods team failed to produce much of anything in the way of documentation. A disappointing showing all around.

Well, in addition to a little more reading on Z, I finished the first volume of the International Formal Methods Survey today. The last 20 pages consisted of the rest of the formal methods overview, plus the initial survey given to the teams involved in the case studies. There's not really much to say about the survey, so I'll just give an overview of the methods.

I read about B, SCR (Software Cost Reduction), and Cleanroom yesterday. B uses an abstract machine approach with development through refinement. To me, it sounds pretty much like what I think of as a stereotypical formal method. SCR uses function tables and a "strongest postcondition" approach to exactly describe how the system state has changed. Lastely, Cleanroom is actually a hybrid development method where formal methods play a relatively small part. Appartently it uses some kind of assertion-based specification method on which I'm still a bit cloudy.

Today I covered the rest of the methods. These are:

1. The Gypsy Verification Environment, which is often used for security-related systems. It is (or was) endorsed by the National Computer Security Center and has a Pascal-based programming language and first-order predicate-calculus for an assertion language.
2. The TCAS methodology (unnamed at time of publication). This is based on Statecharts and uses tables to illustratetransitions between states.
3. The Hewlett-Packard Specification Language (HP-SL), which uses a typing system reminiscient of traditional programming language to describe systems. This is augmented by predicate logic and defived types using sets, sequences, and maps. This one appears to be mostly confined to HP.
4. The Formal Development Methodology (FDM), which is a state machine-based approach that uses Ina Jo and Ina Mod for specification and program assertions. This is also supported by the National Computer Security Center.
5. Occam/Communicating Sequential Processes (CSP), which I don't really get. Apparently it's a program transformation approach based on the idea of a process communicating with its environment. Occam is based on CSP and is the programming language used for Transputers.
6. The Rigorous Approach to Industrial Software Engineering (RAISE). I didn't really get anything concrete about it from the description, other than that it evolved from VDM.
7. Hoare Logics, which I already know all about.
8. Z, which I've been reading all about lately.

The next step is to pick out a few case studies to look over in volume two. I don't think it's necessary to go over all the case studies, since I certainly won't use all of them. In particular, I can probably skip the exploratory group. However, I think I'll definitely want to look at CICS and SACEM, and probably TCAS, MGS, and Tektronix.

Boy, I'm falling behind. I was hoping to make a lot more traction this weekend.

Today, I went back to the IFM92 survey. I finished off the last proper section of the first volume, with the conclusions and lessons learned. After reading the rest of it, there aren't really any surprises in this section. Among the observations were that there's a lack of good tools, including more "middle of the road" tools (i.e. most of the existing ones were huge suites or tiny research projects), that we lack a good cost-benefit analysis method for FM projects, and that most people don't choose to use FM because of the cost benefits.

Another interesting observation was that conventional measurements can fail to capture the scope of some of these projects. For instance, lines of code, which is often used to judge the scope of software projects, fails to capture things like safety concerns or complexity of the problem. A couple thousand lines of code doesn't seem like a lot, but safety or security concerns can add a lot to the analysis and validation of a project, thus increasing the scope disproportionately with the amount of code.

I also started reading the appendix on the formal methods used in the various projects. So far, I only got through SCR, B, and Cleanroom. Nothing terribly interesting the brief summaries of them, but I'll probably revisit them if they come up in other case studies.

Today was chapter 15 of Using Z. This one was an extended example/case study involving the basic programming interface for a filesystem.

The example involved two basic object types (files and file systems) each with four operations defined on them. The global filesystem object was defined in terms of a promotion of the local file object.

To me, the most interesting part of this chapter was to see how the schemas were factored out. For instance, in addition to the expected operation schemas describing creating and deleting files, there were also schemas for error states, such as when the file does not exist. These described constratins and also generated output parameters. The final Create, Destroy, etc. schemas were defined using these extra output schema to make them total operations.

Other than that, I guess there's not a lot to say here. This chapter didn't introduce any new material, but it did give a nice example of putting this stuff into practice.