FM Thesis

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.