Adding Temporal Annotations and Associated Verification to Ravenscar Profile

Research output: Contribution to conferencePaper



Publication details

DatePublished - 2003
Original languageUndefined/Unknown


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.

Bibliographical note


Discover related content

Find related publications, people, projects, datasets and more using interactive charts.

View graph of relations