SafetyChip: a time monitoring and policing device

ABSTRACT

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.

REFERENCES

• 1: Alan Burns , Brian Dobbing , G. Romanski, The Ravenscar Tasking Profile for High Integrity Real-Time Programs, Proceedings of the 1998 Ada-Europe International Conference on Reliable Software Technologies, p.263-275, June 08-12, 1998
• 2: A. Burns, B. Dobbing, and T. Vardanega, "Guide for the use of the Ada Ravenscar Profile in hight integrity systems", University of York Technical Report YCS-2003-348, 2003.
• 3: S. Evangelista , C. Kaiser , J. F. Pradat-Peyre , P. Rousseau, Verifying linear time temporal logic properties of concurrent Ada programs with quasar, Proceedings of the 2003 annual ACM SIGAda international conference on Ada: the engineering of correct and reliable software for real-time & distributed systems using ada and related technologies, p.17-24, December 07-11, 2003, San Diego, CA, USA
• 4: A Method for Verifying Real-Time Properties of Ada Programs, Proceedings of the Seventh International Conference on Engineering of Complex Computer Systems, p.35, June 11-13, 2001
• 5: Altera Corporation, SignalTap II. http://www.altera.com/
• 6: ARM Limited, "Using EmbeddedICE", Application Note 31, 1999.
• 7: K. Larsen, P. Pettersson, and W. Yi, "Uppaal in a Nutshell", International Journal on Software Tools for Technology Transfer, Springer-Verlag, 1997.
• 8: Kristina Lundqvist , Lars Asplund, A Ravenscar-Compliant Run-time Kernel for Safety-Critical Systems*, Real-Time Systems, v.24 n.1, p.29-54, January 2003 [doi>10.1023/A:1021701221847]
• 9: G. Naeser and J. Furunäs, "Evaluation of Delay Queues for a Ravenscar Hardware Kernel", MRTC report ISSN 1404-3041 ISRN MDH-MRTC-176/2005-1-SE, Mälardalen Real-Time Research Centre, 2005.
• 10: Xilinx Inc., Chipscope integrated logic analyzer, San Jose, CA 95124-3400, 2000. http://www.xilinx.com/products/chipscope/
• 11: R. York and J. Sharp, "Real-time debug for systems-onchip devices", ARM Limited, June 1999.

INDEX TERMS

Primary Classification:
  B. Hardware
  B.8 Performance and Reliability
      B.8.1 Reliability, Testing, and Fault-Tolerance

General Terms:
Reliability

Keywords:
FPGA, hardware monitoring, kernel