Paper Info
Title
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 a timed model checker (IF [7, 8]), 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.
Year
DOI
Venue
2008
10.1007/978-3-540-68624-8_3
Ada-Europe
Keywords
Field
DocType
general-purpose tasking construct,ravenscar fragment,model checker,analysis task,present verification result,model checking,ravenscar systems,timing verification,input language,ravenscar profile,small case study,timed automata-based verification
Programming language,Model checking,Computer science,Automaton,Ravenscar profile,Real-time computing,Earliest deadline first scheduling
Conference
Volume
ISSN
Citations 
5026
0302-9743
2
PageRank 
References 
Authors
0.38
14
2
Name
Order
Citations
PageRank
Iulian Ober134230.96
Nicolas Halbwachs23957426.43