D. R. Engler, The Exokernel operating system architecture, Massachusetts Institute of Technology (MIT), 1999.

C. Rippert and J. Stefani, Building secure embedded kernels with the think architecture, Proceedings of the workshop on Engineering Context-aware Object-Oriented Systems and Environments, 2002.
URL : https://hal.archives-ouvertes.fr/hal-00310149

A. Senart, O. Charra, and J. Stefani, Developing dynamically reconfigurable operating system kernels with the think component architecture, Proceedings of the workshop on Engineering Context-aware Object-Oriented Systems and Environments, 2002.

J. L. Lawall, G. Muller, and L. P. Barreto, Capturing OS expertise in an event type system, Proceedings of the 10th workshop on ACM SIGOPS European workshop: beyond the PC , EW10, pp.54-61, 2002.
DOI : 10.1145/1133373.1133384

A. Colin and I. Puaut, Worst-case execution time analysis of the RTEMS real-time operating system, Proceedings 13th Euromicro Conference on Real-Time Systems, pp.191-198, 2001.
DOI : 10.1109/EMRTS.2001.934029

O. Kömmerling and M. G. Kuhn, Design principles for tamper-resistant smartcard processors, USENIX Workshop on Smartcard Technology, pp.9-20, 1999.

D. R. Engler and M. F. Kaashoek, Exterminate all operating system abstractions, Proceedings 5th Workshop on Hot Topics in Operating Systems (HotOS-V), 1995.
DOI : 10.1109/HOTOS.1995.513459

G. Grimaud, J. Lanet, and J. Vandewalle, FACADE, Software Engineering?ESEC/FSE, 1999.
DOI : 10.1145/318774.319265

C. George and . Necula, Proof-carrying code, Proceedings of the 24th ACM SIGPLAN- SIGACT Symposium on Principles of Programming Langauges (POPL '97), pp.106-119, 1997.

A. Requet, L. Casset, and G. Grimaud, Application of the B formal method to the proof of a type verification algorithm, Proceedings. Fifth IEEE International Symposium on High Assurance Systems Engineering (HASE 2000), 2000.
DOI : 10.1109/HASE.2000.895449

D. Deville, A. Galland, G. Grimaud, and S. Jean, Smart Card operating systems: Past, Present and Future, the 5 th NORDU/USENIX Conference, 2003.

J. Regehr, Using Hierarchical Scheduling to Support Soft Real-Time Applications on General-Purpose Operating Systems, 2001.

Z. Deng and J. Liu, Scheduling real-time applications in an open environment, Proceedings Real-Time Systems Symposium, pp.308-319, 1997.
DOI : 10.1109/REAL.1997.641292

C. L. Liu and J. W. Layland, Scheduling algorithms for multiprogramming in a hard-real-time environment, pp.46-61, 1973.

I. Unité-de-recherche, . Lorraine, . Loria, and . Technopôle-de-nancy, Brabois -Campus scientifique 615, rue du Jardin Botanique -BP 101 -54602 Villers-lès-Nancy Cedex (France) Unité de recherche INRIA Rennes : IRISA, Campus universitaire de Beaulieu -35042 Rennes Cedex (France) Unité de recherche INRIA Rhône-Alpes : 655, avenue de l'Europe -38334 Montbonnot Saint-Ismier (France) Unité de recherche INRIA Rocquencourt, Domaine de Voluceau -Rocquencourt -BP 105 -78153 Le Chesnay Cedex (France) Unité de recherche INRIA Sophia Antipolis : 2004, route des Lucioles -BP 93 -06902 Sophia Antipolis Cedex

I. De-voluceau-rocquencourt, BP 105 -78153 Le Chesnay Cedex (France) http://www.inria.fr ISSN, pp.249-6399