# Using CSP to verify a timed protocol over a fair medium

Conference paper

First Online:

## Abstract

Standard timed models of CSP are based upon finite observations, and are thus unsuitable for the analysis of fairness conditions. The addition of infinite observations to the standard timed failures model permits an adequate treatment of fairness in a timed context. The resulting model admits a complete proof system for admissible specifications, and supports a theory of timed refinement for untimed programs. This is demonstrated with a study of a familiar protocol—the alternating bit protocol—communicating over an unreliable but fair medium.

## Keywords

Inference Rule Semantic Model Proof System Proof Obligation Behavioural Specification
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

## Preview

Unable to display preview. Download preview PDF.

## References

- [ACD90]R. Alur, C. Courcoubetis and D. Dill,
*Model checking for real time systems*, Proceedings of the 5th Logics in Computer Science, 1990Google Scholar - [AlH91]R. Alur and T. Henzinger,
*Logics and models of real-time: a survey*, Proceedings of REX '91, to appear in Springer LNCSGoogle Scholar - [BaB91]J. C. M. Baeten and J. A. Bergstra,
*Real time process algebra*., Formal Aspects of Computing, Volume 3, Number 2, 1991Google Scholar - [BrR85]S. D. Brookes and A. W. Roscoe,
*An improved failures model for communicating sequential processes*, Proceedings of the Pittsburgh Seminar on Concurrency, Springer LNCS 197, 1985Google Scholar - [Dav91]J. Davies,
*Specification and proof in real-time systems*, Programming Research Group Monograph PRG-93, Oxford University, 1991Google Scholar - [Fra86]N. Francez, Fairness, Springer-Verlag 1986Google Scholar
- [HeR91]M. Hennessy and T. Regan,
*A process algebra for timed systems*, Report 5-91, School of Cognitive and Computing Sciences, University of Sussex 1991Google Scholar - [Hoa85]C. A. R. Hoare,
*Communicating Sequential Processes*, Prentice-Hall 1985Google Scholar - [Hoo91]J. Hooman,
*Specification and compositional verification of real-time systems*, Ph.D thesis, University of Eindhoven, 1991Google Scholar - [Jac90]D. M. Jackson,
*Specifying timed communicating sequential processes using temporal logic*, PRG Report TR-5-90, Oxford University 1990Google Scholar - [JaM86]F. Jahanian and A.K. Mok,
*Safety analysis of timing properties in real-time systems*, IEEE Transactions on Software Engineering, SE-12, 1986Google Scholar - [Jef92]A. S. Jeffrey,
*Observation spaces and timed processes*, Oxford University D.Phil thesis, 1992Google Scholar - [MoT90]F. Moller and C. Tofts,
*A temporal calculus of communicating systems*, Proceedings of CONCUR 90, Springer LNCS 458, 1990Google Scholar - [Mur90]D. V. J. Murphy,
*Time, causality and concurrency*, Surrey University Ph.D thesis, 1990Google Scholar - [Nic90]X. Nicollin, J.-L. Richier, J. Sifakis and J. Voiron,
*ATP: an algebra for timed processes*, Proceedings of the IFIP Conference on Programming Concepts and Methods, 1990Google Scholar - [NSY91]X. Nicollin, J. Sifakis and S. Yovine,
*From ATP to timed graphs and hybrid systems*, Proceedings of REX '91, to appear in Springer LNCSGoogle Scholar - [OrF91]Y. Ortega-Mallen and D. de Frutos-Escrig,
*A complete proof system for timed observations*, Proceedings of TAPSOFT 91, Springer LNCS 493, 1991Google Scholar - [Ree88]G. M. Reed,
*A uniform mathematical theory for real-time distributed computing*, Oxford University D.Phil thesis, 1988Google Scholar - [ReR86]G. M. Reed and A. W. Roscoe,
*A timed model for communicating sequential processes*, Proceedings of ICALP'86, Springer LNCS 226, 1986Google Scholar - [Ros88]A. W. Roscoe,
*Unbounded nondeterminism in CSP*, Programming Research Group Technical Monograph PRG-67, Oxford University, 1988Google Scholar - [Sch92]S. Schneider,
*Unbounded nondeterminism in Timed CSP*, to appearGoogle Scholar

## Copyright information

© Springer-Verlag Berlin Heidelberg 1992