A Circus semantics for Ravenscar protected objects

D A Atiya; S King; J C P Woodcock

A Circus semantics for Ravenscar protected objects

Computer Science

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

Abstract

The Ravenscar profile is a subset of the Ada 95 tasking model: it is certifiable, deterministic, supports schedulability analysis, and meets tight memory constraints and performance requirements. A central feature of Ravenscar is the use of protected objects to ensure mutually exclusive access to shared data. We give a semantics to protected objects using Circus, a combination of Z and CSP, and prove several important properties; this is the first time that these properties have been verified. Interestingly, all the proofs are conducted in Z, even the ones concerning reactive behaviour.

Original language	English
Title of host publication	FME 2003: FORMAL METHODS, PROCEEDINGS
Editors	K Araki, S Gnesi, D Mandrioli
Place of Publication	BERLIN
Publisher	Springer
Pages	617-635
Number of pages	19
ISBN (Print)	3-540-40828-2
Publication status	Published - 2003
Event	12th International Symposium of Formal Methods Europe - PISA Duration: 8 Sept 2003 → 14 Sept 2003

Conference

Conference	12th International Symposium of Formal Methods Europe
City	PISA
Period	8/09/03 → 14/09/03

Keywords

Ravenscar
Ada protected objects
formal semantics
Z
Circus
TASKING PROFILE

Cite this

@inproceedings{7d50b78b093f40aea27ff7fac5f6a257,

title = "A Circus semantics for Ravenscar protected objects",

abstract = "The Ravenscar profile is a subset of the Ada 95 tasking model: it is certifiable, deterministic, supports schedulability analysis, and meets tight memory constraints and performance requirements. A central feature of Ravenscar is the use of protected objects to ensure mutually exclusive access to shared data. We give a semantics to protected objects using Circus, a combination of Z and CSP, and prove several important properties; this is the first time that these properties have been verified. Interestingly, all the proofs are conducted in Z, even the ones concerning reactive behaviour.",

keywords = "Ravenscar, Ada protected objects, formal semantics, Z, Circus, TASKING PROFILE",

author = "Atiya, {D A} and S King and Woodcock, {J C P}",

year = "2003",

language = "English",

isbn = "3-540-40828-2",

pages = "617--635",

editor = "K Araki and S Gnesi and D Mandrioli",

booktitle = "FME 2003: FORMAL METHODS, PROCEEDINGS",

publisher = "Springer",

address = "Germany",

note = "12th International Symposium of Formal Methods Europe ; Conference date: 08-09-2003 Through 14-09-2003",

}

TY - GEN

T1 - A Circus semantics for Ravenscar protected objects

AU - Atiya, D A

AU - King, S

AU - Woodcock, J C P

PY - 2003

Y1 - 2003

N2 - The Ravenscar profile is a subset of the Ada 95 tasking model: it is certifiable, deterministic, supports schedulability analysis, and meets tight memory constraints and performance requirements. A central feature of Ravenscar is the use of protected objects to ensure mutually exclusive access to shared data. We give a semantics to protected objects using Circus, a combination of Z and CSP, and prove several important properties; this is the first time that these properties have been verified. Interestingly, all the proofs are conducted in Z, even the ones concerning reactive behaviour.

AB - The Ravenscar profile is a subset of the Ada 95 tasking model: it is certifiable, deterministic, supports schedulability analysis, and meets tight memory constraints and performance requirements. A central feature of Ravenscar is the use of protected objects to ensure mutually exclusive access to shared data. We give a semantics to protected objects using Circus, a combination of Z and CSP, and prove several important properties; this is the first time that these properties have been verified. Interestingly, all the proofs are conducted in Z, even the ones concerning reactive behaviour.

KW - Ravenscar

KW - Ada protected objects

KW - formal semantics

KW - Z

KW - Circus

KW - TASKING PROFILE

M3 - Conference contribution

SN - 3-540-40828-2

SP - 617

EP - 635

BT - FME 2003: FORMAL METHODS, PROCEEDINGS

A2 - Araki, K

A2 - Gnesi, S

A2 - Mandrioli, D

PB - Springer

CY - BERLIN

T2 - 12th International Symposium of Formal Methods Europe

Y2 - 8 September 2003 through 14 September 2003

ER -