A framework for model-checking timed CSP
A framework for model-checking timed CSP
- Author(s): J. Ouaknine
- DOI: 10.1049/ic:19990011
For access to this article, please select a purchase option:
Buy conference paper PDF
Buy Knowledge Pack
IET members benefit from discounts to all IET publications and free access to E&T Magazine. If you are an IET member, log in to your account and the discounts will automatically be applied.
IEE Colloquium. Applicable Modelling, Verification and Analysis Techniques for Real-Time Systems — Recommend this title to your library
Thank you
Your recommendation has been sent to your librarian.
- Author(s): J. Ouaknine Source: IEE Colloquium. Applicable Modelling, Verification and Analysis Techniques for Real-Time Systems, 1999 page ()
- Conference: IEE Colloquium. Applicable Modelling, Verification and Analysis Techniques for Real-Time Systems
Timed CSP is a well-known process algebra, built as an extension to Hoare's original CSP, designed to handle concurrency combined with timing considerations. It achieves this over a continuous time domain (the non-negative real numbers), which has the drawback of precluding standard model-checking approaches, as the state-space of any process is naturally a priori (uncountably) infinite. This paper shows how to circumvent this problem by translating and reinterpreting timed CSP processes within a new model of standard CSP. In this discrete model, which draws on previous work by A.W. Roscoe (1997) and A. Mukkaram (1993), timing of events is provided by the consistent and regular communication of a special tock event, analogous to the `tick' of a clock. The various parallel components of a process are therefore required to synchronise on tock, ensuring a uniform rate of passage of time. General results yielding tight bounds on the loss of information inherent to the translation are given. (4 pages)
Inspec keywords: communicating sequential processes
Subjects: Parallel programming and algorithm theory; Formal logic
Related content
content/conferences/10.1049/ic_19990011
pub_keyword,iet_inspecKeyword,pub_concept
6
6