Extending ravenscar with CSP channels

D A Atiya; S King

Extending ravenscar with CSP channels

D A Atiya, S King

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

The Ravenscar Profile 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 verified 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 specifications can be applied to Ravenscar programs. In turn, this increases confidence in these programs and their reliability. Indeed, elsewhere, we use the proposed Ravenscar channels as the basis for a cost-effective technique for verifying concurrent safety-critical system.

Original language	English
Title of host publication	RELIABLE SOFTWARE TECHNOLOGY ADA-EUROPE 2005, PROCEEDINGS
Editors	T Vardanega, A Wellings
Place of Publication	BERLIN
Publisher	Springer
Pages	79-90
Number of pages	12
ISBN (Print)	3-540-26286-5
Publication status	Published - 2005
Event	10th Ada-Europe International Conference on Reliable Software Technologies - York Duration: 20 Jun 2005 → 24 Jun 2005

Conference

Conference	10th Ada-Europe International Conference on Reliable Software Technologies
City	York
Period	20/06/05 → 24/06/05

Cite this

@inproceedings{9d4a7290a73b4ffd8155f91231e2ed6a,

title = "Extending ravenscar with CSP channels",

abstract = "The Ravenscar Profile 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 verified 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 specifications can be applied to Ravenscar programs. In turn, this increases confidence in these programs and their reliability. Indeed, elsewhere, we use the proposed Ravenscar channels as the basis for a cost-effective technique for verifying concurrent safety-critical system.",

author = "Atiya, {D A} and S King",

year = "2005",

language = "English",

isbn = "3-540-26286-5",

pages = "79--90",

editor = "T Vardanega and A Wellings",

booktitle = "RELIABLE SOFTWARE TECHNOLOGY ADA-EUROPE 2005, PROCEEDINGS",

publisher = "Springer",

address = "Germany",

note = "10th Ada-Europe International Conference on Reliable Software Technologies ; Conference date: 20-06-2005 Through 24-06-2005",

}

TY - GEN

T1 - Extending ravenscar with CSP channels

AU - Atiya, D A

AU - King, S

PY - 2005

Y1 - 2005

N2 - The Ravenscar Profile 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 verified 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 specifications can be applied to Ravenscar programs. In turn, this increases confidence in these programs and their reliability. Indeed, elsewhere, we use the proposed Ravenscar channels as the basis for a cost-effective technique for verifying concurrent safety-critical system.

AB - The Ravenscar Profile 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 verified 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 specifications can be applied to Ravenscar programs. In turn, this increases confidence in these programs and their reliability. Indeed, elsewhere, we use the proposed Ravenscar channels as the basis for a cost-effective technique for verifying concurrent safety-critical system.

M3 - Conference contribution

SN - 3-540-26286-5

SP - 79

EP - 90

BT - RELIABLE SOFTWARE TECHNOLOGY ADA-EUROPE 2005, PROCEEDINGS

A2 - Vardanega, T

A2 - Wellings, A

PB - Springer

CY - BERLIN

T2 - 10th Ada-Europe International Conference on Reliable Software Technologies

Y2 - 20 June 2005 through 24 June 2005

ER -