FM Thesis

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.

Today was chapter 14, on preconditions. Basically, this covered methods for calculating preconditions of schemas, in order to do things lik establish basic consistency.

The first section described the initialization theorem. Basically, this just says that if you can establish that there exists a state satisfying the initialization schema, then the schema requirements must be consistent. This seems fairly obvious.

After that, it got into calculating preconditions. To be honest, this is where my eyes started to glaze over. Let's face it: the mechanics of doing logic just isn't that interesting. Even the author left out large sections of proof at various points. I pretty much just plowed through this and literally tried my best to stay awake.

So section two discussed various general concerns related to preconditions (e.g. conceptual stuff, like remembering to factor out the things in the declarations). It also introduced the pre precondition operator for schemas.

Section three got seriosly into the mechanics of calculating and simplifying preconditions. It also included a basic algorithm/method for calculating the precondition of a schema.

Section four discussed the structure of operations and the effect on preconditions. For instance, it discussed distributivity of the precondition operator (it distributes over disjunction, but not conjunction).It also including some stuff on free promotion. The punchline seems to be that the precondition of a global operation under a free promotion is equivalent to the conjunction of the preconditions of the local operation and promotion schema. Not that I fully grasp promotions yet, but I'm sure that will make sense later.

Today I finally finished reading chapter 13 of Using Z. I've been looking at this for days, and I'm still not sure I get it. I'll probably have to come back to it later.

This chapter covers schema factorization and promotion. It seems that this relates to how you can model indexed collections of things. The examples include things like arrays and the player scores in Trivial Pursuit. The basic idea seems to be that, given the right conditions, you can describe the global state in terms of local states. So, instead of having a schema to describe the global state, you can factor this out as a schema describing the local state and a promotion schema, which basically determines how changes in the local state affect the global state.

What I don't get is why you would want to define things in terms of promotion schemas and how to you would go about constructing them. Maybe I've just put up a mental block, but it kind of seems like this method is overly complicated. The concept seems reasonable enough, but the examples just seem to make things more difficult than they need to be. Perhaps promotion suffers from the same problem as teaching object-orientation - all the good examples are too comlicated for beginners and all the examples beginners can handle are incredibly stupid applications of the concept.

It doesn't help that I'm starting to drown in the notation in this chapter. I think I'm going to have to go back over the last few chapters again soon. For instance, I keep wondering where the thetas are coming from. Of course, the theta operator indicates a characteristic binding, which was never really defined with any clarity. The book pretty much just said it's a binding that characterizes a schema by binding, e.g. element a to a, b to b, and so on. What, exactly, that means and why I should care is still an open question.

That's enough for now. It's late, I'm tired, and I just don't care anymore. Plus I'm pissed off because VMware's network bridging module has been causing kernel panics every time I try to use it.

Wow, a whole week since my last post. I'll have to try not to repeat that again. However, there were extenuating circumstances: I felt really crumby for the past week. I came down with a nasty cold on Friday and couldn't really concentrate on anything up until this morning. As a result of this, I only read two and a half chapters of Using Z this week, and I'm not at all confident that I understood them. I'll probably have to go back over them later (but I was most likely going to do that anyway).

Chapter eleven was on schemas. As I understand it, schemas are basically Z's equivalent of abstract data types. They consist of a declaration section and a predicate section. The declaration just introduces the variables used in the schema, while the predicate section is a set of predicates involving these variables that every object in the schema must, by definition, satisfy.

Just to complicate things, schemas can also be used as types, declarations, and predicates. The type part seems obvious enough. For declarations, using a schema introduces the variables in the declaration and puts them under the appropriate constraint. As predicates, a schema defines constraints on the variables, provided they have already been introduced.

One note of interest is schema normalization. Basically, this just means putting all the constraint information in the schema in the predicate part. For example, if two schemas are the same, except that one declares a variable as being in the natural nubmers, while the other declares it as being in the integers, we would change the first schema to have that variable in Z and add a constraint to the predicate section that it is an element of N. The same sort of thing can happen with functions and relations.

Last, but not least, it is possible to have generic schemas that are parameterized by a type. However, that's about all I know about them at this point.

Chapter 12 was on schema operators: conjunction, disjunction, negation, composition, as well as sections on quantification and decorators. It introduced the notation for schema states and state changes (using the familiar ΔState), plus the conventional ? and ! decorators for input and result variables.

Chapter 13 is on promotion. I'm only part way through that one, and I didn't really grok it while I was reading it, so I'll leave that to tomorrow. Right now, it's late and I'm tired, so it's bed time.

Well, it's been a couple of days, but there's not an awful lot to say, so this will be short. It's also late, so I don't feel like going into great detail.

On Tuesday, I read chapter 10 of Using Z. That was the chapter on free types. Basically, it introduced how to define an arbitrary type, such as enumerated types. It also showed how to use free types to model a binary tree, which was kind of interesting.

Basically, there are a couple of ways to define a free type. One is by explicitly enumerating the possible values, like this:
Colors::= red|gree|blue
Another is with a constructor function. The general case of the constructor looks like this:
FreeType::= constant|constructor <<source>>
This is convenient for recursive definitions, as you can have a constant as your base case and reference the free type in the constructor. The simplest example was defining the natural numbers as follows:
nat::= zero | succ <<nat>>
Another interesting example was the following definition of a binary tree:
Tree::= leaf <<N>> | branch <<Tree x Tree>>
This defines a tree as either a numbered leaf node or an ordered pair of trees.

In addition to the expected sections on induction and primitive recursion that this chapter included, there was also a breif section on consistency. Free types makes it possible to introduce contradictions into our math. The example given was the definition:
T::= d <<&weierp; T>>
The problem here is that power sets are not finitary, whatever that means. The text leaves the term undefined, except to say that we basically need to stick to finite constructs to maintain consistency. Apparently the idea is that non-finitary (or is it infinitary?) constructs generate too many values, so we would end up with a set T that must be bigger than itself.

Anyway, yesterday and today I spent in reviewing the past five chapters of Using Z. Basically just looking over the key points and taking some notes. The symbols were all starting to run together, so I figured it would help make them stick in my memory if I wrote them down.