Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Real-time systems : formal specification and automatic verification
Olderog E., Dierks H., Cambridge University Press, New York, NY, 2008. 344 pp. Type: Book
Date Reviewed: Sep 15 2009

The authors’ stated--and well-achieved--purpose for this advanced and highly focused book on formally specifying and automatically verifying real-time embedded safety-critical systems is to bring together duration calculus (DC), timed automata, and programmable logic controller (PLC) automata, so as “to form a seamless design flow, from real-time requirements specified in the duration calculus, via designs specified by PLC-automata, and into source code for hardware platforms of embedded systems.” The role of timed automata “as ... operational model[s] of real-time systems” is in automatic verification via model checking, with the Uppsala-Aalborg (UPPAAL) model checker. It is also remarkable that the source code element (C language or PLC structured text) in the authors’ formal abstraction through verification of the implementation is an actual compilation of the PLC automata that comprises the logical and operational semantics of the user’s design, under the auspices of the Moby/RT (real-time) tool treated in Section 6.5 (that mediates and automates the use of the UPPAAL model checker).

I hope to be of service to my fellow real-time/embedded old timers, by assuaging a discomfort born of earlier (1970s) experience with PLCs, then called programmable controllers (PCs). You may think, as I initially did, that the PLC automaton abstraction (defined by Dierks) lacks sufficient generality--since a PLC periodically polls its input and does not recognize asynchronous interrupts--but this is not the case: “We want to stress that each computing device ... equipped with a clock can be programmed to behave like a PLC.” Thus, the implementation is not restricted to PLCs.

The first chapter, “Introduction,” is an unusually clear and precise exposition of the nature and properties of real-time systems. It is, in this regard, not a small point that equivalence-by-definition has a notation that separates it from logical bi-implication. Olderog and Dierks prepare the reader for issues that may arise when time is construed as a real number--that is, as continuous, as opposed to being discrete. These issues have to do with logical decidability and with reachability of system states. In addition to the classic safety (the design must ensure that something bad never happens) and liveness (something desirable eventually happens), we are introduced to two requisite properties of a formal system: bounded response (reaction within a prescribed time interval) and duration (the cumulative time in which the system is in a given critical state has an upper bound). These two properties have a key formal methods attribute--falsifiability in finite time.

Two safety-critical applications--the generalized railroad crossing and the gas burner--are treated in increasingly refined ways throughout the book. They receive their initial, already somewhat precise, formalizations in the first chapter. The authors also introduce the fundamental pattern wherein formalized design implies (syntactically or semantically) formalized requirements and safety properties.

Chapter 2 introduces the syntax, semantics, and proof rules of DC--a species of (interval) temporal logic, complete with modal box and diamond operators, which expresses “a high-level declarative view of real-time systems without implementation bias.” Here, I found the rigorous formalization of the ubiquitous timing diagram--its rendering as a building block for proofs--to be an excellent example of how to formalize such an everyday object. Regarding the soundness and completeness of DC--an issue in all species of logic--DC formulas that “depend on facts of the real numbers” cannot be complete. The book expounds the next best thing, relative completeness (if time were a real number rather than discrete).

Chapter 3 elaborates on properties and subsets of DC. It contrasts discrete time with continuous time, with respect to realization (the decidability thereof) of a given DC formula; continuous time again yields undecidability. A notion of “implementables” serves to overcome some problems and enables a correctness proof of the gas burner controller. Kleuker’s constraint diagrams are introduced as a visual realization of a DC subset.

Chapter 4 discusses timed automata (TA). It defines handshaking for networks of TA, expresses tracks and gates of a railroad crossing and the latter’s safety properties, and expounds on “Zeno behavior”--although progress is being made, the system never reaches its destination.

Chapter 5 presents PLC automata’s three advantageous properties: implementability (on computers or PLCs); desirable, formal semantics for industrial control; and verifiability via formal proofs.

The final chapter 6 closes the loop via an exposition of automatic verification. It posits the notion of test automata and describes the ways UPPAAL is used. It ends with a mention of current research directions, aimed at dealing with verification complexity.

The appendix on notations is an excellent summary of logic, set theory, relations, functions, real numbers, languages, and automata. (The definition of partial function is erroneous, the error being a seeming oversight.)

This excellent advanced book deserves--and will reward--diligent study and work on the well-designed exercises. I recommend it highly.

Reviewer:  George Hacken Review #: CR137302 (1009-0857)
Bookmark and Share
  Featured Reviewer  
 
Real-Time And Embedded Systems (C.3 ... )
 
 
Automata (F.1.1 ... )
 
 
General (B.8.0 )
 
 
Specifying And Verifying And Reasoning About Programs (F.3.1 )
 
Would you recommend this review?
yes
no
Other reviews under "Real-Time And Embedded Systems": Date
Real-time and systems programming for PCs
Vickery C., McGraw-Hill, Inc., New York, NY, 1993. Type: Book (9780070674660)
Oct 1 1994
Manipulation of terrain data for a real-time display application
Vaughan J., Brookes G., Fletcher M., Wills D. Microprocessors & Microsystems 15(7): 347-353, 1991. Type: Article
Apr 1 1993
Parallel processing in industrial real-time applications
Lawson H., Prentice-Hall, Inc., Upper Saddle River, NJ, 1992. Type: Book (9780136545187)
Jun 1 1994
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy