Adding Temporal Annotations and Associated Verification to Ravenscar Profile

Alan Burns, Tse-Min Lin

Research output: Contribution to conferencePaperpeer-review

Abstract

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
Pages80-91
Publication statusPublished - 2003

Bibliographical note

ISBN:3-540-40376-0

Cite this