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.