On the timed automata-based verification of Ravenscar systems

Abstract:
The Ravenscar profile for Ada enforces several restrictions on the usage of general-purpose tasking constructs, thereby facilitating most analysis tasks and in particular functional and timing verification using model checking. This paper presents an experiment in translating the Ravenscar fragment of Ada into the input language of the timed model checker IF, discusses the difficulties and proposes solutions for most constructs supported by the profile. The technique is evaluated in a small case study issued from a space application, on which we present verification results and conclusions.

Reference:

@inproceedings{pldi08,
title={On the timed automata-based verification of Ravenscar systems},
author={I. Ober and N. Halbwachs},
booktitle={13th International Conference on Reliable Software Technologies -
Ada-Europe 2008},
address={Venice, Italy},
month=jun,
year=2008
}

PDF file