I liked this history when I first skimmed it. ¿Now, I’m not so sure. ¿

The first figure is an excellent picture of the confluence of model checking and performance analysis. ¿Model checking is a way to guarantee that a piece of software or a protocol satisfies given properties. ¿An example property is that the system will enter a desirable state. ¿Model checking tools can prove that it does or will find a counterexample. Performance analysis can calculate the probability that it will take too long.

The paper argues that one can do both at the same time by using a suitable logic. It describes one logic in the sidebar, and gives a simple example. I found the proposed marriage of logic and probability convincing, but can it become part of mainstream software engineering?

When I returned to the paper to write this review, I noticed some issues. It contains no typographical errors, but it does contain a half-dozen references that are not listed. The authors claim that these references are on the Web, but they provide no URL. Even the search engines could not find the list.

The paper mentions process algebra, but completely ignores the performance enhanced process algebra (PEPA) developed by Hillston [1]. PEPA is a similar confluence of methods, and even shares tools and theories (Markov processes). I would have liked to see a comparison.

In summary, this is a good advertisement for the authors’ research, but it is not the history I had hoped for on my first reading.