Constance Heitmeyer and Nancy Lynch. Formal Verification of Real-time Systems Using Timed Automata. In Constance Heitmeyer and Dino Mandrioli, editors, Chapter 4 of Trends in Formal Methods for Real-Time Computing. John Wiley and Sons, Ltd., pages 83-106, April 1996. Trends in Software series.

Abstract

The use of the Lynch-Vaandrager timed automaton model is illustrated with a solution to the Generalized Railroad Crossing problem. The solution shows formally the correspondence between four system descriptions: an axiomatic (i.e., descriptive) specification, an operational specification represented in terms of timed automata, a discrete system implementation, and a system implementation that works with a continuous gate model. Several sample proofs are given. In the development of the solution, a number of guidelines were applied. These guidelines, which should prove useful in applying formal methods to practical systems, are described and illustrated with examples.

To see an overview of the whole book, chapter titles and authors, an excerpt from the book preface, and a "how to order" form, click here.