Real Time is Really Simple

It should be quite obvious that no special logic or language is needed to write or reason about real-time specifications. There’s a simple way to do it: just use a variable to represent time. Martín Abadi and I showed in [106] that this can be done very elegantly in TLA. A simpler, more straightforward approach works with any sensible formal method, but it’s too simple and obvious to publish. So instead, hundreds of papers and theses have been written about special real-time logics and languages–even though, for most purposes, there’s no reason to use them instead of the simple, obvious approach. And since no one writes papers about the simple way of handling real time, people seem to assume that they need to use a real-time logic. Naturally, I find this rather annoying. So when I heard that a computer scientist was planning to write a book about one of these real-time logics, I decided it was time to write another paper explaining the simple approach.

Since you can’t publish a new paper about an old idea, no matter how good the idea may be, I needed to find something new to add. The TLC model checker provided the opportunity I needed. The method described in [106] and [144] is good for specifying and reasoning about real-time systems, but it produces specifications that TLC can’t handle. TLC works only with the simpler approach, so I had an excuse for a new paper.

There’s a naive approach for checking real-time specifications with TLC that I had thought for a while about trying. It involves checking the specification for all runs up to some maximum time value that one hopes is large enough to find any bugs. So I did that using as examples two versions of Fischer’s mutual exclusion protocol, which is mentioned in the discussion of [106].

One possible reason to use a special real-time approach is for model checking. I figured that model checkers using special algorithms for real time should do much better than this naive approach, so I wanted some justification for using TLA+ and TLC instead. Looking through the literature, I found that all the real-time model checkers seemed to use low-level languages that could describe only simple controllers. So I added the example of a distributed algorithm that they couldn’t represent. Then I discovered that, since the papers describing it had been published, the Uppaal model checker had been enhanced with new language features that enabled it to model this algorithm. This left me no choice but to compare TLC with Uppaal on the example.

I asked Kim Larsen of Aalborg University, the developer of Uppaal, for help writing an Uppaal spec of the algorithm. Although I really did this because I’m lazy, I could justify my request because I had never used Uppaal and couldn’t see how to write a nice model with it. Larsen got his colleague Arne Skou to write a model that was quite nice, though it did require a bit of a “hack” to encode the high-level constructs of TLA+ in Uppaal’s lower-level language. Skou was helped by Larsen and his colleague, Gerd Behrmann. As I expected, Uppaal was much faster than TLC–except in one puzzling case in which Uppaal ran out of memory.

I put the paper aside for a while. When I got back to it, I realized that there’s a simple way of using TLC to do complete checking of these real-time specifications that is much faster than what I had been doing. The idea is so simple that I figured it was well known, and I kicked myself for not seeing it right away. I checked with Tom Henzinger, who informed me that the method was known, but it had apparently not been published. It seems to be an idea that is obvious to the experts and unknown to others. So this provided another incentive for publishing my paper, with a new section on how to use an explicit-time model checker like TLC to check real-time specs. Henzinger also corrected a basic misunderstanding I had about real-time model checkers. Rather than trying to be faster, most of them try to be better by using continuous time. He wrote:

If you are happy with discrete time, I doubt you can do any better [than my naive approach]. Uppaal, Kronos etc. deal with real-numbered time, and therefore rely on elaborate and expensive clock region constructions.
I was then inspired to do some more serious data gathering. I discovered the explanation of that puzzling case: Uppaal runs out of memory when the ratio of two parameters becomes too large. The results reported in the paper show that neither TLC nor Uppaal comes out clearly better on this example.

The Uppaal distribution comes with a model of a version of Fischer’s algorithm, and I decided to get some data for that example too. Uppaal did clearly better than TLC on it. However, I suspected that the reason was not because real-time model checkers are better, but because TLC is less efficient for this kind of simple algorithm than a model checker that uses a lower-level language. So I got data for two ordinary model checkers that use lower-level languages, Spin and SMV. I was again lazy and got the developers of those model checkers, Gerard Holzmann and Ken McMillan, to do all the work of writing and checking the models.

I submitted this paper to the journal Formal Methods in Systems Design. I thought that the part about model checking was interesting enough to be worth putting into a separate conference paper. I therefore wrote [157], which was accepted at the 2005 Charme conference. However, the journal submission was rejected because it didn’t contain enough new ideas.