Adding Temporal Annotations and Associated Verification to Ravenscar Profile

Alan Burns, Tse-Min Lin

Research output: Contribution to conferencePaperpeer-review


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.
Original languageUndefined/Unknown
Publication statusPublished - 2003

Bibliographical note


Cite this