Today I read the sequences chapter of Using Z. I'd not been exposed to sequences before, so this was relatively new to me. Intuitively, a sequence is an ordered series of items that allows repetition, such as <a, b, b, c, a>. It turns out that sequences can also be viewed as functions from the natural numbers to some set of objects. Needless to say, this simplifies things from a conceptual standpoint, as it allows the reuse of a lot of mathematical language.

The chapter covered basics such as the definition of a sequence, operations such as concatenation and filtering, as well as functions for the head and tail of the sequence, reversing, etc.

This chapter also went into structural induction to prove properties of sequences. This was initially confusing to me, as they didn't give the usual symbolic statement of the proof rule for structural induction. They also define axioms for the equivalence of the predicate to be proved and construct the proof using those. It took me a couple of proofs to realize that the defined axiom was how they were getting form "P s" to some complex predicate.

Lastly, they introduced the idea of bags, which are basically sequences without order. Bags can be represented as a function from a set of objects to the natural number, where the number in the range represents the number of times the item is in the bag. This section also introduced bag-equivalents of set membership and subset, as well bag union and difference operators. The latter simply involve adding or subtracting the number of elements for each bag involved to get the resulting bag. The only odd thing I found was that the difference operator is a union cup with a minus sign in it, whereas I'd have thought an intersection cap would have been more appropriate. Oh well....

Slow weekend for research. I spent all weekend visiting my in-laws, so the only thing I managed to get done was to finish chapter 8 of Using Z. That was the one on functions.

Maybe I'm just getting rusty, but this chapter was a little confusing. It covered lambda notation (which I think I get), functions on relations (which I also think I get, though the examples were a little confusing), function overriding (which seems pretty basic), properties of functions, and finite sets. It got really confusing in the properties of functions chapter when they introduced different styles of arrows to denote different types of functions. So injective functions got one style of arrow, surjective another, and bijective yet another. Plus there was a vertical line through the arrow to denote partial functions and, later, a double line to indicate the set of all finite functions on two sets. I think I'm going to have to go back and make myself a cheat-sheet of all the symbols I've seen in the past few chapters.

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.

So yesterday I polished off chapters 4 and 5 of Using Z and I finished chapter 6 tonight. With any luck, I'll get a good start on chapter 7 before bed. It's a much faster read than I would have expected, but that might just be because I haven't gotten into the really heavy stuff yet.

Chapter four discussed rules for equality of expressions and introduced the "one-point" rule for reasoning with existential quantifiers. It also included some interesting examples of predicates describing uniquness with quantifiers and introduced the mu notation for definite description. That was something I had not seen before. The notation is (μ x: a | p), which denotes the unique object x in set a which satisfies predicate p.

Chapter five was an overview of basic set theory, including things like the inference rules regarding set conprehension. It also included basics such as definitions of the union, intersection, and difference operations, and all that good stuff. It also included a brief definition of types in Z. It turns out that Z types are maximal sets, often defined in terms of power sets or Cartesian products.

Chapter six was an introduction to defining things in Z. This includes defining types, declaring objects, and introducing axioms. The basic syntax is fairly straight forward so far. The only problem I had was trying to figure out the relevance of power sets of power sets.

To take the example from page 82, the predicate "is a crowd" was formalized as:crowds: P(P Person) crowds = {s: P Person | #s >= 3}This indicates that crowds is an element of the power set of the power set of all people and that crowds is the set of all members of the power set of people with three or more members. After thinking about this for a few minutes, it started to become clear what that means. The set of all crowds is a set of sets, so its elements obviously have to belong to the power set of all people. But since a type is a maximal set, what is the type of crowds? Obviously it must be P(P Person), since crowds must be an element of that. And since crowds contains elements of P Person, we end up with each element of crowds being a set of individual people.

It all makes perfect sense, really. It's just a different type and level of abstraction than I'm used to using. I just needed to stop for a few minutes and wrap my brain around.

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.

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:

The INMOS Transputer, which used FM for the floating-point unit and virtual channel processor.
The Tektronix oscilloscope.
The "Structured System Analysis and Design Method" toolset developed by Praxis.
IBM's legendary CICS respecification.
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:

The LaCoS (Large Correct Systems) project, which mades a toolset for a variant of VDM with the explicit goal of technology transfer.
The TBACS (Token-based Access Control System) smartcard system.
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.

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.

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.

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

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.
Multinet Gateway System (MGS): A security-sensitive internet gateway project that used the Gypsy Verification Environment.
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.
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

Structured Systems Analysis and Design Method Toolset: A project by Praxis to build tools to support this design method, using a Z specification.
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.
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."
Tektronix Oscilloscope: An oscilloscope project using Z.
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

Large Correct Systems (LaCoS): A technology transfer project involving the Rigorous Approach to Industrial Software Engineering (RAISE), a variant of VDM.
Token-based Access Control System (TBACS): A prototype smart card system for network access that used theorem proving.
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.

Well, I spent some time thinking about it tonight and I banged out two topic ideas. Since I'm having trouble deciding whether to go for a more theoretical/academic approach or a more research oriented topic regarding industrial applications, I worked up one topic for each.

On the industrial applications side, I'm thinking of a two-pronged analysis of various formal methods and case studies. On the one hand, I would examine various industrial projects that used formal methods, such as CICS, or SHOLIS, or whatever. Praxis has a lot of decent case study material, and I have a number of other case study papers. The idea is that I'd examine the project, the formalism used, and the results. I would then try to draw some conclusions about the efficacy of the methods used. The second prong would be to try to analyze how those conclusions would apply to other types of projects. For example, since most formal methods projects are large projects in safety- or security-critical domains, I would try to do an analysis of how they could be profitably applied to, say, small to medium sized business projects. If it was required/warranted, I could even attempt such an application, i.e. trying to design a simple business system while applying some "light-weight" formal methods.

Because my interests run towards the practical, my "theoretical" topic is actually more of a project. I have a number of papers on formalizations of programming languages and ways to formalize various language features, such as recursion or exceptions. My idea is to actually apply this to define a formal semantics for a meaningful subset of a widely used language. I'm thinking either Python or PHP might be good candidates. This adds a little novelty to the topic in that both are dynamic languages, i.e. variables are created and typed dynamically, which I've never seen before. PHP also has that array/hashtable hybrid type, which could provide for an interesting treatment. I have material on most of the basic aspects of imperative languages, so this would essentially be an attempt to aggregate that research and extend it to a language in practical use.

I'll write that up in a more formal way and send it to Roger tomorrow. For now, I'm going to get a glass of water and go to bed.

Now that I've finished going over my accumulated research papers, it's time to solidify my topic. I've got two broad areas to chooes from: practical and theoretical. So far, I've sort of been moving willy-nilly between the two with no real direction.

On the practical side, I've got a whole lot of case studies of the use of formal methods in industrial projects and a whole lot of discussions of methodology. In other words, people talking about how formal methods were used or how the should be used.

On the theoretical side, I've got a bunch of papers describing different types of formalizations and how to extend/generalize/refine those formalizations. In other words, lots of abstract math and logic.

Honestly, I'm probably more interested in the actual application of formal methods. The theory and math behind it is very interesting, but what I'd really like is to see this stuff in action. The only problem is that I don't work for Praxis Critical Systems or anyplace else that uses FM on a regular basis. I also don't know anyone who works for such a company. Nor do I have access to a team of developers to run experiments in applying formal methods, like in the Smidts, Huang, and Widmaier article (The Journal of Systems and Software, vol 61, 2002, p 213-224).

So with the practical side, it's not really that clear where I could go. Yeah, I can aggregate research on formal methods projects, but that's boring and isn't really doing anything new. I suppose I could apply formal methods to a project on my own, but I'm not sure about the appropriateness or scope of that. Obviously just specifying an application in Z and then building it isn't sufficient. However, is something like the thttpd verification a realistic project?

On the theoretical side, there is a lot of interesting sounding stuff that I could look into. The only problem is that there's a very real posibility that I could drown in the math. If the truth were known, my abstract math background really isn't as strong as it should be. (I was a philosophy major - what do you expect?) That is not a good thing, as most of the academic papers I've collected have some fairly advanced looking stuff in them. Given enough time and research, I'm sure I could get a handle on all the math, but the question is, how much time would it take?

I think it would be interesting to do something that could, at least theoretically, have some real-world application. The thttpd verification sticks out in my mind as a very cool project. It would be interesting to study the formalization of some programming language construct or to try to apply a formalization to an existing codebase. Or, perhaps, adapt a formalization to a different programming language. Cavalcanti and Naumann's work on the axiomatic semantics of object-oriented languages might be a goot place to start. I wonder how they would work with a less Java-like languages than ROOL?

At any rate, I'll continue my musings tomorrow. Right now, it's 11:30 and I have to get up for work in the morning. Although, on the up side, I've got a long weekend coming up. Holidays: one of the best parts of being a public servant.

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:

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'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:

An article describing a wp() refinement calculus. It seems to focus on a "refinement relation" for preserving total correctness between steps in program derivation.
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.
An interesting article on teaching FM in a "general education" computer science course.
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.
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.
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.
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.
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.
A paper on "debugging" Larch specifications. It describes a couple of tools that check various claims that can be included in Larch specifications.
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.

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:

An interesting experiment that involved a formal methods team and a conventional CMM level 4 team independently implementing the same system.
An article on software development productivity which doesn't seem to directly relate to formal methods. Not sure why that was in there....
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.
Two breif articles on the use of formal methods in standards, including military and safety standards.
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.
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.
A brief overview of some formal methods projects as part of the introduction to an IEEE FM special issue.
An article by Craigen, Gerhart, and Ralston discussing the regulatory part of their massive 2 volume, 12 project formal methods study.
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.

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.

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:

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

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

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.
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.
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.
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.
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.
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.
An interesting sounding paper that used case studies to examine why formal methods are not more widely used.
A doctoral thesis of a formal verification of thttpd, a secure web server.
An article on formal reasoning about pointers using Higher Order Logic. (Used Isabelle/HOL for automated proofs.)
A case study on using "lightweight" formal methods to analyze and detect problems with the design of a radiation therapy machine.
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.)
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.
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.
A "practical guide" to defining programming languages using Prolog and Metamorphosis Grammars, which includes relational, denotational, and axiomatic semantics.
An article describing a verification tool that works by verifying abstract programs and relating them to concrete programs.
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.

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:

Three papers from Clarke and Halpern (though not necessarily together) on constructing complete Hoare axiom systems for certain classes of programming language.
Another paper that introduces a language with a complete Hoare axiomatization.
A paper on teaching denotational semantics by translaing the rules into Prolog.
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.
Two papers dealing with the semantic effects of aliases, one of which took an interesting sounding approach to the axiomatic semantics.
Two papers related to automated theorem proving.
A paper giving an axiomatic treatment of the effects of exception handling.
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.
A more philosophical paper by Dijkstra on why formal methods seem to be looked down upon.
An article on rigorous proof of correctness without actually using the notation of formal methods.
A paper on using formal methods to keep costs down in commercial projects.
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.

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:

Four general discussion/survey articles on formal methods.
Four academic articles on various types of formal semantics.
Tony Hoare's Turing Award lecture (don't know how that got filed with the research....)
Three case-studies on applications of formal methods.
A formal verification of a Java compiler.
Something I didn't really understand that relates to using axioms for JUnit testing.
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.

Blogging my MS thesis on formal methods

Site Map

Location

Search

News Feeds