Tsai has been investigating the reliability of real-time systems for about a decade; the references section of this paper lists many of her previous papers. Wang’s work has been previously published, but this is her first real-time topic. Apparently, though, it’s been a productive relationship: the authors published a new paper, “Specification and timing analysis of real-time systems” [1], only four months after this one.
As stated in the abstract, the purpose of this paper is to demonstrate that correct behavior can be asserted, and those assertions executed and evaluated to provide fault tolerance, in a manner that constrains overhead to an acceptable level for real-time systems. First, the authors develop interval temporal logic (ITL) from classic predicate logic, and present the syntax and semantics of ITL formulas. Using a train set control program as an example, they derive some safety constraints that define correct behavior, and then implement programs (presented in the appendix) that include correctness checks of the executing system. Performance figures are reported for different configurations of the system.
The reported overhead varied from a few percentage points to more than a third of the processing time, depending on how the experiment was structured. It struck me as being too dependent on the nature of the application to be universally tolerable. The overhead will be acceptable in some situations, but, in others, assertion checks will have to be artificially delayed in order to reduce it. The requirements for implementation are also fairly exotic: an ITL parser and evaluation library, and a C-based communicating sequential processes (CCSP) parser.
Several decades ago, there were many papers describing how to create compiler tools, but it took “the dragon book” [2] (it had a dragon on the cover) to show most of us how to do it. The good news in this paper is that executable assertions for real-time systems are on the way, but it will take a few more papers from Tsai before I will understand how to sit down and code something in C or Java.
