FM Thesis

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:

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.