This thesis concerns the relationship between continuous and discrete modelling paradigms for timed concurrent systems, and the exploitation of this relationship towards applications, in particular model checking. The framework we have chosen is Reed and Roscoe's process algebra Timed CSP, in which semantic issues can be examined from both a denotational and an operational perspective. The continuous-time model we use is the timed failures model; on the discrete-time side, we build a suitable model in a CSP-like setting by incorporating a distinguished tock event to model the passage of time. We study the connections between these two models and show that our framework can be used to verify certain specifications on continuous-time processes, by building upon and extending results of Henzinger, Manna, and Pnueli's. Moreover, this verification can in many cases be carried out directly on the model checker FDR. (FDR is a commercial product of Formal Systems (Europe) Ltd.) Results are illustrated with a small railway level crossing case study. We also construct a second, more sophisticated discrete-time model which reflects continuous behaviour in a manner more consistent with one's intuition, and show that our results carry over this second model as well.
Ph.D. Thesis, Oxford University, 2001. 178 pages.
Technical Report PRG-RR-01-06, Oxford University Computing
Laboratory.
PostScript / PDF
© 2001 Joël Ouaknine.