Implementing and Verifying EDF Preemption-Level Resource Control

M.L. Fairbairn; A. Burns

Implementing and Verifying EDF Preemption-Level Resource Control

M.L. Fairbairn, A. Burns

Computer Science

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

Abstract

To support Earliest Deadline First (EDF) dispatching of application tasks the Ada language has had to incorporate Baker's Stack Resource Protocol (SRP). This protocol has proved problematic both in terms of its language definition and implementation. This paper proposes a means of verifying the implementation of complex language features. It describes a prototype tool that allows a comparison to be made between the output of an executing program and a diverse simulator that directly implements EDF+SRP. The tool creates a collection of cases (scenarios); for each of which a program is automatically generated (and executed) and a separate simulation script produced. Tests on an existing run-time for Ada has shown that in certain circumstances an Ada pro-gram and its corresponding simulation diverge.

Original language	Undefined/Unknown
Title of host publication	Proceedings Reliable Software Technology - Ada-Europe
Editors	M. Brorsson, L.M. Pinho
Publisher	Springer
Pages	193-206
Number of pages	14
Volume	LNCS 7308
Publication status	Published - 2012

Cite this

@inproceedings{6922e87f8444450ab5e3b50db61721c4,

title = "Implementing and Verifying EDF Preemption-Level Resource Control",

abstract = "To support Earliest Deadline First (EDF) dispatching of application tasks the Ada language has had to incorporate Baker's Stack Resource Protocol (SRP). This protocol has proved problematic both in terms of its language definition and implementation. This paper proposes a means of verifying the implementation of complex language features. It describes a prototype tool that allows a comparison to be made between the output of an executing program and a diverse simulator that directly implements EDF+SRP. The tool creates a collection of cases (scenarios); for each of which a program is automatically generated (and executed) and a separate simulation script produced. Tests on an existing run-time for Ada has shown that in certain circumstances an Ada pro-gram and its corresponding simulation diverge.",

author = "M.L. Fairbairn and A. Burns",

year = "2012",

language = "Undefined/Unknown",

volume = "LNCS 7308",

pages = "193--206",

editor = "M. Brorsson and L.M. Pinho",

booktitle = "Proceedings Reliable Software Technology - Ada-Europe",

publisher = "Springer",

address = "Germany",

}

TY - GEN

T1 - Implementing and Verifying EDF Preemption-Level Resource Control

AU - Fairbairn, M.L.

AU - Burns, A.

PY - 2012

Y1 - 2012

N2 - To support Earliest Deadline First (EDF) dispatching of application tasks the Ada language has had to incorporate Baker's Stack Resource Protocol (SRP). This protocol has proved problematic both in terms of its language definition and implementation. This paper proposes a means of verifying the implementation of complex language features. It describes a prototype tool that allows a comparison to be made between the output of an executing program and a diverse simulator that directly implements EDF+SRP. The tool creates a collection of cases (scenarios); for each of which a program is automatically generated (and executed) and a separate simulation script produced. Tests on an existing run-time for Ada has shown that in certain circumstances an Ada pro-gram and its corresponding simulation diverge.

AB - To support Earliest Deadline First (EDF) dispatching of application tasks the Ada language has had to incorporate Baker's Stack Resource Protocol (SRP). This protocol has proved problematic both in terms of its language definition and implementation. This paper proposes a means of verifying the implementation of complex language features. It describes a prototype tool that allows a comparison to be made between the output of an executing program and a diverse simulator that directly implements EDF+SRP. The tool creates a collection of cases (scenarios); for each of which a program is automatically generated (and executed) and a separate simulation script produced. Tests on an existing run-time for Ada has shown that in certain circumstances an Ada pro-gram and its corresponding simulation diverge.

M3 - Conference contribution

VL - LNCS 7308

SP - 193

EP - 206

BT - Proceedings Reliable Software Technology - Ada-Europe

A2 - Brorsson, M.

A2 - Pinho, L.M.

PB - Springer

ER -