Extending Ravenscar with CSP Channels

13 years 10 months ago

Download www-users.cs.york.ac.uk

Abstract. The Ravenscar Proﬁle is a restricted subset of the Ada tasking model, designed to meet the requirements of producing analysable and deterministic code. A central feature of Ravenscar is the use of protected objects to ensure mutually exclusive access to shared data. This paper uses Ravenscar protected objects to implement CSP channels in Ada – the proposed implementation is formally veriﬁed using model checking. The advantage of these Ravenscar channels is transforming the data-oriented asynchronous tasking model of Ravenscar into the cleaner message-passing synchronous model of CSP. Thus, formal proofs and techniques for model-checking CSP speciﬁcations can be applied to Ravenscar programs. In turn, this increases conﬁdence in these programs and their reliability. Indeed, elsewhere, we use the proposed Ravenscar channels as the basis for a cost-eﬀective technique for verifying concurrent safety-critical system.

Diyaa-Addein Atiya, Steve King

Real-time Traffic