Applied Formal Methods at National Taiwan University

On 1 January, Joe wrote about his New Year's resolutions, one of which involved doing more "public" writing in 2010. He said that he had tried to draft me into this resolution with him, but was not sure whether he succeeded. He did, in fact, succeed... and so my goal, like his, is to write or edit at least 1,000 public words per day (on average).

Unfortunately, I've fallen somewhat behind. Today is 20 January, and so far this year I've submitted an 9 1/2 page paper to QSIC 2010 and given a public talk (more on that later) for which the slides (available here) comprise about 1,500 words. I figure that puts me at about 10,000 words... and therefore behind by about 10,000 words (after this post, I'll still be behind by about 9,000 words).

One of the reasons I've fallen behind (and this is not meant to be an excuse) is my holiday travel - from 31 December to 13 January, I was in Tokyo and Taipei; both are very interesting places to visit, and Tokyo at the New Year is especially interesting because that's pretty much the most important holiday on the Japanese calendar (unlike much of the rest of East Asia, where the New Year on the Chinese calendar is the most important holiday). Thus, there are multiple special events: New Year's Eve celebrations, the Emperor's annual address to the people and the opening of the Imperial Palace grounds on 2 January, special food, and of course fukubukuro (lucky bags). Sadly, I missed my chance for a lucky bag at the Apple Store in Ginza by several hours... but I digress.

The reason for mentioning my holiday travel here at all is the public talk I gave at the Department of Computer Science and Information Engineering at National Taiwan University, entitled "Building Reliable Software with Applied Formal Methods: A Brief Overview". The talk was arranged when I told a contact of mine there that I was going to be in town, and fellow Caltech Ph.D. Hsuan-Tien Lin was my very gracious host. He told me that nobody in the department really had any experience with applied formal methods, so I prepared the talk as an overview of the tools and technologies we use in our verification-centric software engineering process (described in A Verification-centric Software Development Process for Java).

I initially expected that the talk would be received in much the same way as the (very similar) talk I gave at KITECH last August, where there was also little in the way of formal methods experience in the audience; at KITECH the response was one of polite interest and some good questions were asked, but there was an overall sense that they were not likely to adopt any of the techniques I described. Imagine my surprise, then, when I ended up eating lunch with (and later answering questions from) Yih-Kuen Tsay, a professor in NTU's Department of Information Management, who was not only familiar with JML and BON but also knew specifically about KindSoftware and the Mobius PVE! Dr. Tsay is, by a remarkable coincidence, an academic nephew of mine and Joe's; his Ph.D. advisor, Rajive Bagrodia, was one of Mani Chandy's students at UT Austin.

Dr. Tsay teaches courses entitled "Software Development Methods", "Software Specification and Verification", and "Automatic Verification" (among others). He told me that he had considered using JML and its related tools (including Mobius) for his courses but that, for several reasons (primarily having to do with the maturity of the tool support), he is currently using UML/OCL and Frama-C instead. We had a very interesting discussion where he told me that he would very much like to be able to use JML in his teaching, and I told him a bit about OpenJML and the current Mobius PVE release. He also stated that, for better or worse, UML and OCL are industry standards, and wondered if we (the JML community) had ever given any thought to attempting to standardize JML, or some subset of JML, through an international standards body.

I actually don't know whether the JML community has considered attempting a "JML Standard" or not, though I suspect not... and I also don't know whether it's a good idea, though again I suspect not. My instinct is that the standardization rabbit hole is one that we (as academics) would be better off not diving into, lest we never emerge to do non-standardization work; but at the same time, actually having a standard might encourage industrial tool support, which would facilitate said non-standardization work. Certainly, it's interesting to think about what the ramifications might be.

As for the talk itself, it went quite well. It was on 8 January, the last day of instruction for the autumn semester; they have 18-week semesters at NTU, which makes me incredibly jealous, as I always have to struggle to fit material into my 10-week quarters here at UWT. The students and faculty that attended seemed quite interested, and I have no doubt that if there were easy-to-use, modern tool support for the development method I described, many of them would try it and some would end up adopting it. If only there was a way to entice more people to contribute to OpenJML development...