Adding Temporal Annotations and Associated Verification to Ravenscar Profile
A. Burns and T.-M. Lin
This paper presents a proposal for extending the Ravenscar Tasking Profile with annotations that can be used to express temporal properties. An approach using model checking for the verification of compliance to the annotations is also presented. An extended example is used to illustrate the application of the proposed approach
Download Not Available
BibTex Entry
@inproceedings{Burns2003c,
author = {A. Burns and T.-M. Lin},
booktitle = {Reliable Software Technologies---Ada-Europe 2003},
editor = {J.-P. Rosen and A. Strohmeier},
note = {Ravenscar Profile, Model Checking, UPAAL, SPARK},
pages = {80-91},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
title = {Adding Temporal Annotations and Associated Verification to Ravenscar Profile},
volume = {2655},
year = {2003}
}