Back to posting

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.

Yipe! It's been too long

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.

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.

Catching back up

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.

Evaluating FM

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.

A software experiment and an analysis of CICS

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.

One IFM volume down

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.

Back to the IFM

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.

Z and IFM

Yesterday I muddled through chapter seven of Using Z. That was the chapter on relations. Mostly review, so there's not much to mention.

Today, I read through section nine of the IFM92 survey. This was the section discussing the formal methods used by the various projects and some of the possible areas for further research and development. It even included a hand breakdown of the projects and the methods, their uses, the tools involved, and things they needed. For purposes of this section, the exploratory cluster of projects were rolled into the other two, with TBACS going in with the regulatory cases and LaCoS and HP going in with the commercial.

There were a few general trends to note. First, the formal methods used tended toward those involving first-order logic and/or state machines. State machines were a bit more common in the regulatory cases, whereas Z dominated in the commercial cases. As previously noted, proof and refinement were more of a concern in the regulatory cases, but were largely unused in the commercial ones. It was also noted that the formal methods used were lacking in some areas, such as real-time and concurrency issues.

Another note of interest on the methods themselves was confusion over notation. Several projects had difficulty with non-FM experts being able to follow the notation. In some cases, graphical methods (diagrams, animations) were used to overcome this.

In terms of tools, they were lacking. Some projects used nothing at all, while most of the other projects used an incomplete toolset. The study authors generally concluded that improved support for automated deduction would have been a great boon to most projects. Also, a better selection of Z tools would have been helpful to the commercial cluster.

The last major point was regarding integration of FM with more conventional development methodologies. It seems obvious that this is a very important factor and that balkanizing formal and conventional methods leaves us with a sub-optimal process at best. The authors think that the SACEM and INMOS projects provide good examples of how FM can be integrated with the rest of the development process.

Predicate logic review

Another slow couple of days. Yesterday and today I just spent a little time reading the next to chapters of Using Z. Nothing interesting in these; just propositional and predicate logic review. The next two chapters are also mathematical background. It looks like I'll start getting into the meat of Z around chapter six.

Catching back up

Well, I didn't get around to posting my day's progress on Wednesday, so I guess I'll be summarizing more than usual today. Unfortunately, I didn't get anything done yesterday night, as I had other things I needed to do.

Wednesday and today I got through some more of the IFM92 survey. I covered the commercial case cluster, the exploratory cluster, and the event and timing section.

The commercial cluster consisted of five projects:

  1. The INMOS Transputer, which used FM for the floating-point unit and virtual channel processor.
  2. The Tektronix oscilloscope.
  3. The "Structured System Analysis and Design Method" toolset developed by Praxis.
  4. IBM's legendary CICS respecification.
  5. The "COBOL Structuring Facility" which used the Cleanroom method.

There are a few things to note here. First, the COBOL/Sf project was the only one that didn't use Z in some way. However, there were minor problems in that Z could not be used to model interfaces or real-time properties. Second, it seems that only INMOS attempted any sort of formal proof of correctness. Apparently this was not a big concern for the other organizations, although the formal specifications did at least help in generating test cases.

Overall, the results were not too surprising. FM were seen to have a generally good impact on the projects. Although only INMOS attempted verification, the CICS and Tektronix people apparently thought the formal specification gave them more "intellectual ownership" of the systems.

There was apparently no dramatic affect on the economic factors involved in most of the products. Although it seems that most saw improved quality (at least subjectively), there was no substantial difference between the cost of the project and the estimated time and cost to do it using conventional methods. The only exception was INMOS, who reported saving an estimated three months and three million pounds due to the FM reducing the amount of testing they needed to do. In terms of ongoing maintenance costs, there was little data collected. The only data point is COBOL/SF, which required one person/year for maintenance, which is less than would normally be expected. However, that might be due as much to the other aspects of Cleanroom as it is to FM.

There were three exploratory projects:

  1. The LaCoS (Large Correct Systems) project, which mades a toolset for a variant of VDM with the explicit goal of technology transfer.
  2. The TBACS (Token-based Access Control System) smartcard system.
  3. The HP Medical Instruments case, which involved the creation of a VDM-based specification language with the goal of transferring FM technology to the rest of the organization.

To me, the results of this cluster seem less than stellar. All the groups learned a great deal from their respective projects, but there wasn't an awful lot of actual technology transfer. For instance, the LaCoS project, which seems to be the most successful, did transfer its work successfully to its partners, but it doesn't seem like they've done an awful lot with it.

The HP project didn't go so well. Apparently FM did not significantly increase the product's quality or time to market. Apparently management didn't see significant advantages to be gained and ended up disbanding the Fm groups.

The TBACS project seems to have had mixed results. The FM used did find a flaw in the prototype smartcard that would not have been detected by testing, and in that sense, were a success. However, other factors led the developers to decide against adopting them. Apparently they decided to file them away for use in future projects.

There weren't too many conclusions to be drawn in the event and timeline section. The common events seem to be the ones that introduced organizations to FM, i.e. the desire to try out new methods and the recognition of a serious problem that they could not solve with their current methods. There was not much commonality in timeframes or in events that kept them on the "formal methods path." However, with two exceptions (Tektronics and HP), all the organizations continue to use FM. Apparently Tektronix converted the Z specification to object-oriented code and decided to simply continue with that.

In other news, I also started reading up on Z a bit. I managed to get through the introductory chapter of Using Z: Specification, Refinement, and Proof tonight. Obviously I haven't gotten to the good part yet, so there's not much to say about it. However, I did see that the book includes a number of case studies that used Z, which may come in handy later.

FM on Slashdot?

My reading today included an article that was recently linked on Slashdot of all places. The article was entitled Correctness by Construction: A Manifesto for High-Integrity Software and was written by Martin Croxford and Rod Chapman at Praxis HIS. It didn't contain too much I hadn't read before, but it did reference a couple of more recent projects. Other than that, it was just a general discussion of the "Correctness by Construction" method Praxis uses with some guidelines for use and statistics about their impressive productivity and defect rates.

I also slogged through another section of the 1992 International Formal Methods Survey (hereafter IFM92). This section was a summary of the results of the regulatory cases.

There were a few noteworthy things in this section. First, the emphasis of these projects was, unsurprisingly, on correctness and, in particular, the ability to offer proof of correctness, or, at least, to increase comprehensibility. In fact, the entire formal methods portion of the Darlington Nuclear Generator project was a post-hoc verification of an existing system in order to obtain certification.

Another interesting fact is that the regulatory cases were much more expensive than the other cases. In the case of Darlington, this is not surprising, as the entire FM effort was post-hoc and so could not reduce costs. What was surprising is that the price tag for FM at Darlington was $4,000,000, not lost profits for the certification delay. The SACEM project was also quite an effort, with the quoted statistic being 120,000 man-hours of effort.

Though the impact of FM on individual projects was good, the impact on the process/organization was mixed. GEC Alsthom subsequently used the methods developed for SACEM in other projects and the TCAS team received FM well. However the Darlington and MGS people were less enthusiastic and didn't display much interest in further pursuing FM.

A last tidbit was the use of tools. SACEM and MGS used tool support extensively, but Darlington and TCAS used none at all. The authors believe this is due to the relative immaturity of the methods used in those cases.

And as for maintenance of the software, the authors believe that FM will help, but did not have enough data to justify any conclusion.

Short day

Another short day today. I read a few more pages of the Craigen, Gerhart, and Ralston study I mentioned yesterday. I got through the section on the research methodology. They used a "common sense" approach rather than any sociological method, so there's not much to talk about. They sent out surveys to the companies involved, read any relevant literature on the projects, and then went for an interview which was guided by another survey. Then they gathered their notes and reported on each case.

The general breakdown of the case studies is fairly intuitive. They were concerned focus on determining the type of company and project in question, what the goals of the project were, and formal methods applied. Point of interest include why formal methods were introduced and how the company introduced them into the process.

I also started thinking about my research outline today. Basically, I'm trying to outline a path for my research to take. The idea is to give myself some direction and impose some sort of sequence or natural progression on the whole research process.

So far, I'm thinking that I'll start by picking some promising case studies, then identifying the formal methods involved and getting some general material on them. I'm obviously starting with the 1992 International Survey, which I think is a good beginning source, by virtue of its volume, if nothing else (the two PostScript files occupy in excess of 300 pages). This obviously suggests several methods, with Z and Gypsy (which I remember from another paper) standing out for further investigation. The papers from Praxis also seem promising, so SPARK will no doubt be added to the list.

Those are the obvious ones, though. I think I need to try for a little diversity. The SRT and radiotherapy machine papers are nice for a start, but I think I'm going to need to hit the library again. I'd like to find something more recent and, if possible, something where safety and security are not necessarily critical features.

I'll start drawing up some sort of plan based on my research mindmap tomorrow. Hopefully I'll be able to pull out a few papers to at least give me ideas of other places to look.

Starting the Internation Survey

Today I started looking over An International Survey of Industrial Applications of Formal Methods, a study of 12 formal methods projects sponsored by the US Dept. of Commerce, among others, and published in 1993 (available here). I got through the first 23 pages (of the PostScript file) of Volume 1: Purpose, Approach, Analysis, and Conclusions.

So far, it's mostly just summary. I've read about this paper before, so I've yet to find any revelations. I did see the summaries of the 12 case studies, though. They were divided into three categories: regularotry, commercial, and exploratory. The project breakdown goes as follows:

Regulatory projects

  1. Darlington Nuclear Generator Station (DNGS): Post-hoc verification of the software shutdown system using the Software Cost Reduction approach in order to get a license to operate.
  2. Multinet Gateway System (MGS): A security-sensitive internet gateway project that used the Gypsy Verification Environment.
  3. SACEM: Also known as the Paris metro project to increase "person-flow" by having less time between trains. Used B and Hoare Logic to help meet safety requirements.
  4. Traffic Alert and Collision Avoidance System (TCAS): The title says it all - a system to keep planes from hitting each other. The summary didn't say much, but I believe from other reading that this may have been one of Praxis's projects.

Commercial projects

  1. Structured Systems Analysis and Design Method Toolset: A project by Praxis to build tools to support this design method, using a Z specification.
  2. Customer Information Control System (CICS): a trnasaction processing system that IBM partially redesigned using Z. From other reading, there is apparently there is some disagreement over exactly how successful this project was.
  3. Cleanroom Software Methodology: A pair of projects for NASA and IBM. These are a system for ground control of satelites and a system to convert COBOL systems into a "structured programming equivalent."
  4. Tektronix Oscilloscope: An oscilloscope project using Z.
  5. INMOS Transputer: INMOS used Z, Occam, Communicating Sequential Processes, and the Calculus of Communicating Systems to design their Transputer family of VLSI circuits.

Exploratory projects

  1. Large Correct Systems (LaCoS): A technology transfer project involving the Rigorous Approach to Industrial Software Engineering (RAISE), a variant of VDM.
  2. Token-based Access Control System (TBACS): A prototype smart card system for network access that used theorem proving.
  3. Hewlett-Packard Medical Instruments: A real-time medical database that was developed using a variant of VDM. Was considered a failure because time to market was the key feature.

Research mind-map

Here is the complete mind-map of my accumulated research papers. It's about 80 documents, only about half of which will likely be useful, depending on which way I go. I've broken down the categories a little more than the preliminary version, but there aren't many big differences. Just the addition of about 20 documents.

I've uploaded the mind map in three formats:

  1. PNG Image
  2. HTML outline
  3. KDissert file

The image just gives the structure of the tree and title of each document while the HTML page displays the content of each node in outline form (despite the fact that the nodes are not ordered). The kdissert file has everything, as the others were generated from it. (Note: all links resolve to my local disk.)

Now it's time to figure out where to go with all this. I think I'll do that in a separate post.

I'm done abstracting

I've gotten through the remainder of my paper articles. I still have to go over my accumulated notes, but most of them are on the articles I've been cataloging here.

I had 10 articles today. They include:

  1. An article describing a wp() refinement calculus. It seems to focus on a "refinement relation" for preserving total correctness between steps in program derivation.
  2. An article on integrating FM into development. It describes the Secure Release Terminal (a system for changing classified document security) and the use of the the Ina Jo specification language.
  3. An interesting article on teaching FM in a "general education" computer science course.
  4. A paper describing KIDS, an interactive system for automatically developing programs. The idea is that all the hard work is automated and you can build a formal specification just by selecting various high-level transformations. It gives a derivation of a program to solve the k-queens problem as an example.
  5. An interesting looking article on reasoning about the effects of program changes. It uses an approximate logic and works on the structure, rather than semantics, of the program.
  6. Greg Nelson's generalization of Dijkstra's calculus. Essentially, he removed the Law of the Excluded Miracle, i.e. wp(S, false)=false. This gives us the possibility for partial commands and other things I don't want to think about at 10:30 at night.
  7. A round-table series of articles on formal methods. It's just a series of one-page articles on FM topics ranging from education to industrial use.
  8. An article on the Penelope "verification editor" for Larch/Ada. Apparently it's another interactive tool, but this one uses the Larch Shared Language to generate verification conditions for a subset of Ada.
  9. A paper on "debugging" Larch specifications. It describes a couple of tools that check various claims that can be included in Larch specifications.
  10. An article on using the Boyer-Moore prover to automatically verify concurrent programs. Describes the logic and semantics used and gives the example of a distributed program to compute a minimum value in a tree.

I guess tomorrow I'll pick up on finishing off my mind-map and start thinking about a topic summary. That should be interesting, as staying on topic was where I had my problems the first time.

Starting the paper

Slow day today on the thesis front. I was hoping to get more done, but my computer malfunctioned last night and I spend most of this evening reinstalling and reconfiguring Kubuntu. On the up side, at least it went faster this time than the first time I installed it.

I only got through 11 paper articles today. By my count, I now have 12 left, although I think a couple of them are duplicates of electronic documents. Anyway, today's papers included:

  1. An interesting experiment that involved a formal methods team and a conventional CMM level 4 team independently implementing the same system.
  2. An article on software development productivity which doesn't seem to directly relate to formal methods. Not sure why that was in there....
  3. An article by Hoare illustrating several different types of formal programming methods, including logical, functional, algebraic, etc. On the down side, he uses a simple greatest common divisor example to illustrate.
  4. Two breif articles on the use of formal methods in standards, including military and safety standards.
  5. Two articles on the Praxis CDIS project. One is a reflective article by Anthony Hall, while the other is an independent analysis of the fault data recorded by Praxis.
  6. Hall's famous list of Seven Myths of Formal Methods, in which he relates misconceptions about FM using the Praxis CASE project as an example.
  7. A brief overview of some formal methods projects as part of the introduction to an IEEE FM special issue.
  8. An article by Craigen, Gerhart, and Ralston discussing the regulatory part of their massive 2 volume, 12 project formal methods study.
  9. A book chapter by Craigen, Gerhart, and Ralston discussing technology transfer from formal methods practitioners to the main stream and why there isn't more of it.

A preliminary research list

As promised, here is a preliminary mind map and categorized list of my electronic research documents. I still have a (comparatively) small stack of paper documents and notes to go over, which I will include in a later version.

So far, I have categorized my research into two broad areas: practical and theoretical. By this, I'm refering primarily to the distinction between documents relating to more abstract mathematical concerns, such as semantic formalizations for programming constructs, and ones focused more on real-world activities, such as case studies or discussion of industrial considerations when using formal methods.

It seems I've got a lot of stuff to go on here. As is evident from the previous posts, my existing research base covers a wide range, from the highly abstract mathematics to in-depth industrial case studies. I seem to have a bit more material on the academic side, but I've got lots of practical stuff too. I'm going to have a hard time figuring out where to go with this. Of course, that's part of the reason I had to get organized and start this log in the first place.

Anyway, here are the documents in question. A picture of the mind map and the HTML document generated from it. Both of these documents were generated by KDissert 0.9. And just for the record, don't bother clicking any of the links in the HTML document - they all resolve to the files on my local machine. Anyone who's interested in seeing the documents in question should e-mail me or leave a comment.

The electronic articles are done!

Well, I got through the remaining 14 articles sitting in the thesis folder on my hard drive. This batch was considerably easier and more homogenous than yesterday's. Today I had:

  1. An article by Naumann on total-correctness semantics for an Oberon-like language (called Io - Idealized Oberon) with record-type, procedure-type, and global variables. The semantics uses a set-theoretic predicate transformer model, which sounds pretty interesting.
  2. A Cavalcanti and Naumann article on the semantics of ROOL involving specification statements in the language, or something like that. It appears that ROOL also uses a set-based predicate transformer semantics.
  3. And then I had 12 documents on SPARK from the good people at Praxis Critical Systems.

The SPARK articles included a number of case studies and a few articles on proving the absence of runtime exceptions. The MULTOS CA (a smart-card system) and SHOLIS (helicopter control system) were cited in several articles. SHOLIS is interesting because there was, apparently, a great deal of proof work done, both in SPARK and in Z. The MULTOS CA was interesting to me because of the use of off-the-shelf software in the form of Windows and MFC.

I think I can justify a light day on a Saturday, so that's about it. I do have some text files of notes that I need to link to the corresponding articles, so I'll probably do that tonight. I might start organizing my mind map as well, but I'll probably do the bulk of that tomorrow.

The electronic documets: day 3

Well, I got through 20 articles today. Today's batch includes:

  1. Two non-technical articles I apparently found on the web. One compared FM with XP, while the other just had some useful references to programming languages with a formal semantics.
  2. Both volumes of An Internationsl Survey of Industrial Applications of Formal Methods. This one is a collection of 12 case studies in real formal methods use.
  3. Two items on ROOL, the Refinement Object-Oriented Language, by Cavalcanti and Naumann. One is actually just some lecture slides, but the other is a wp() semantics of the language.
  4. An extensive guide to formal methods that was written to supplement the FAA's Digital Systems Validation Handbook. I don't know where I found that.
  5. Two papers on Z. One answers a challenge to examine the questions raised in converting an English specification (of an invoicing system) into a formal one, while the other compares Z to VDM and some other formal methods.
  6. A truly baffling article by Naumann called A Categorical Model for Higher Order Imperative Programming. I'm still not sure exactly what it's about, but it appears to involve set theory. At least, that's what I got from skimming the introdiction. The abstract might as well have been gibberish for all the good it did me.
  7. An interesting sounding paper that used case studies to examine why formal methods are not more widely used.
  8. A doctoral thesis of a formal verification of thttpd, a secure web server.
  9. An article on formal reasoning about pointers using Higher Order Logic. (Used Isabelle/HOL for automated proofs.)
  10. A case study on using "lightweight" formal methods to analyze and detect problems with the design of a radiation therapy machine.
  11. A paper that gives a sound and complete Hoare logic for a language with recursion and unbounded nondeterminism. (This one also uses Isabelle/HOL. I guess I should look into that.)
  12. An intriguing critique of Hoare logics in general. Apparently, Hoare logics are generally not "inferentially sound," but rather "theorem sound," which the author finds unacceptable. Apparently, this is related to the difference between partial and total correctness. The author also bangs on about goto statements. This one sounds very interesting.
  13. An apparently reworked version of Nelson and Broy's article on adding fair-choice to Dijkstra's calculus. It looked an awful lot like the one from yesterday, but the publication date was four years later. Maybe the ACM just published an edited version.
  14. A "practical guide" to defining programming languages using Prolog and Metamorphosis Grammars, which includes relational, denotational, and axiomatic semantics.
  15. An article describing a verification tool that works by verifying abstract programs and relating them to concrete programs.
  16. Last, but not least, an account of the Stanford Pascal verifier.

Looks like I'm nearly done. I've got about 15 documents left. Most of them are on SPARK and written by good people at Praxis Critical Systems.

Adding to the research map

Today I continued with mapping out and (briefly) abstracting my computerized research papers. I got 18 of them today before I ran out of steam. Today's set included a lot of more academic articles, as well as a few of the seminal papers on formal semantics. I've only been reading abstracts and skimming, but some of these look very interesting.

The papers from today include:

  1. Three papers from Clarke and Halpern (though not necessarily together) on constructing complete Hoare axiom systems for certain classes of programming language.
  2. Another paper that introduces a language with a complete Hoare axiomatization.
  3. A paper on teaching denotational semantics by translaing the rules into Prolog.
  4. A paper on an undergrad compiler project in Ada95. Not sure what that has to do with formal methods, unless they're using SPARK. Or maybe I just downloaded it because of my Ada95 fetish.
  5. Two papers dealing with the semantic effects of aliases, one of which took an interesting sounding approach to the axiomatic semantics.
  6. Two papers related to automated theorem proving.
  7. A paper giving an axiomatic treatment of the effects of exception handling.
  8. Three foundational papers on axiomatic semantics, including the article that introduced Hoare logics, Dijkstra's guarded command article, and Gries's article on the semantics of procedure calls.
  9. A more philosophical paper by Dijkstra on why formal methods seem to be looked down upon.
  10. An article on rigorous proof of correctness without actually using the notation of formal methods.
  11. A paper on using formal methods to keep costs down in commercial projects.
  12. An overview of various research areas in programming languages which includes sections on semantics.

I should be able to finish most of the electronic papers tomorrow. Then I can move on to that pile of paper sitting on my shelf. And after that, I can start organizing my mind map and start figuring out where to go from here.

Getting started

I have commenced my "master plan" to finally finish my Master's thesis. I will be in regular contact with Roger to ensure that I make steady progress and I will be making daily blog entries summarizing what I've done. With any luck, this will keep me on pace to finish by August, or by the end of the year at worst.

My first goal is to go over my accumulated research and write up a summary of my thesis topic and where I'd like to go with it. I need to have that done and mailed to Roger by January 15. That will serve as my jumping off point to direct further research and build an outline.

To that end, today I started going through the collection of research papers I've accumulated. Lots of them of PDF files culled from the internet or from the online archives of the ACM and IEEE.

Right now, I'm going through the papers and starting to map them out using KDissert, a KDE-based mind-mapping tool designed for helping students create documents like dissertations and theses. I'm currently in the process of creating nodes for all my documents. I'm adding the titles, a link to the file, and a very brief abstract of the topic of the paper. I'll post the the map when I get everything added.

I didn't have too long to work today, so I only got through 15 documents. I've probably got at least 50, not counting the ones on paper. Today's selection included:

  1. Four general discussion/survey articles on formal methods.
  2. Four academic articles on various types of formal semantics.
  3. Tony Hoare's Turing Award lecture (don't know how that got filed with the research....)
  4. Three case-studies on applications of formal methods.
  5. A formal verification of a Java compiler.
  6. Something I didn't really understand that relates to using axioms for JUnit testing.
  7. An axiomatic semantics of an object-oriented language that supports aliases.

I should probably post the actual article names and authors for future reference, but it's late and I have to get up for work in the morning. I'll continue to list tomorrow.