Atiya, Diyaa-Addein and King, Steve and Woodcock, Jim (2003) A Circus semantics for Ravenscar protected objects. In: Araki, K. and Gnesi, S. and Mandrioli, D., eds. LECTURE NOTES IN COMPUTER SCIENCE. SPRINGER-VERLAG BERLIN, HEIDELBERGER PLATZ 3, D-14197 BERLIN, GERMANY pp. 617-635. ISBN 3-540-40828-2.
|The full text of this publication is not available from this repository. (Contact us about this Publication)|
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.
|Item Type:||Conference or workshop item (UNSPECIFIED)|
|Subjects:||Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,|
|Divisions:||Faculties > Science Technology and Medical Studies > School of Computing > Systems Architecture Group|
|Depositing User:||Mark Wheadon|
|Date Deposited:||24 Nov 2008 18:00|
|Last Modified:||27 Feb 2009 15:31|
|Resource URI:||http://kar.kent.ac.uk/id/eprint/13836 (The current URI for this page, for reference purposes)|
- Depositors only (login required):