A Ravenscar-Compliant Run-time Kernel for Safety-Critical Systems* |
| |
Authors: | Lundqvist Kristina Asplund Lars |
| |
Affiliation: | (1) Department of Computer Systems, Uppsala University, Information Technology, Sweden |
| |
Abstract: | The Ravenscar tasking profile for Ada 95 has been designed to allow implementation of highly safety critical systems. Ravenscar defines a tasking system with deterministic behavior and low complexity. We provide a formal model using UPPAAL of the primitives provided by Ravenscar including exceptions. This formal model is used to verify the correctness of the Ravenscar model and can be used to verify safety properties of applications using the Ravenscar profile. As an illustration of this, we model a sample application using all features of Ravenscar and formally verify its correctness. Furthermore, an introduction to the Ravenscar model is given. |
| |
Keywords: | safety-critical systems Ravenscar run-time kernel formal modeling model checking Ada UPPAAL |
本文献已被 SpringerLink 等数据库收录! |