SafetyChip

The SafetyChip proposes a strategy where parts of the effort invested in the formal verification during the development of a system can be reused during the system's operation. The strength in a formal verification of a system is that a system can mathematically be proven to fulfil certain requ...

Full description

Saved in:
Bibliographic Details
Published in:ACM SIGAda Ada Letters 2005-12, Vol.XXV (4), p.63-68
Main Authors: Naeser, Gustaf, Asplund, Lars, Furunas, Johan
Format: Article
Language:English
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:The SafetyChip proposes a strategy where parts of the effort invested in the formal verification during the development of a system can be reused during the system's operation. The strength in a formal verification of a system is that a system can mathematically be proven to fulfil certain requirements, e.g., timing requirements. The SafetyChip uses information from verification to monitor and police a system during run-time. The monitoring is done by surveillance of the applications communication with the run-time kernel. If deviance from the predefined verified behaviour is detected, the SafetyChip can signal (police) this in different ways, e.g., by generating interrupts the system can respond to.In our experiments we use systems written in Ravenscar compliant Ada code and have automated model extraction from source code to the models used to verify the system.This paper presents the functionality and design of the SafetyChip. Properties of an implementation of the SafetyChip are also presented.
ISSN:1094-3641
DOI:10.1145/1104011.1103856