Safe Collaboration in Extensible Operating Systems: A Study on Real-Time Extensions

D. Deville, Y. Hodique, and I. Simplot-Ryl

References

  1. [1] D. Deville, A. Galland, G. Grimaud, & S. Jean, SmartCard operating systems: Past, present and future, Proc. 5thNORDU/USENIX Conf., Västerås, Sweden, February 2003, 14–28.
  2. [2] D.R. Engler, The Exokernel operating system architecture, doctoral diss., Massachusetts Institute of Technology, Cambridge, MA, 1999.
  3. [3] G.C. Necula, Proof-carrying code, Proc. 24th ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages (POPL’97), Paris, January 1997, 106–119. doi:10.1145/263699.263712
  4. [4] G. Grimaud, J.-L. Lanet, & J.-J. Vandewalle, FAÇADE: Atyped intermediate language dedicated to smart cards. Proc.Software Engineering—ESEC/FSE, Toulouse, 1999, 476–493.
  5. [5] A. Requet, L. Casset, & G. Grimaud, Application of the B formal method to the proof of a type verification algorithm. Proc.5th IEEE Int. Symp. on High Assurance Systems Engineering(HASE 2000), Albuquerque, 2000, 115–124. doi:10.1109/HASE.2000.895449
  6. [6] J.L. Lawall, G. Muller, & L.P. Barreto, Capturing OS expertisein an event type system: The Bossa experience. Proc. 10thACM SIGOPS European Workshop 2002 (EW2002), France,September 2002, 54–61. doi:10.1145/1133373.1133384
  7. [7] M.Q. Beers, C.H. Stork, & M. Franz, Efficiently verifiableescape analysis. Proc. ECOOP 2004, LNCS 3086 (Ed. M.Odersky), Oslo, 2004, 75–95.
  8. [8] J.-P. Talpin & P. Jouvelot, The type and effect discipline.Proc. 7th Annual IEEE Symp. on Logic in Computer Science,Santa Cruz, CA (Los Alamitos, CA: IEEE Computer SocietyPress, 1992), 162–173.
  9. [9] P. Cousot & R. Cousot, Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proc. 4th ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages (POPL'77), Los Angeles, CA, 1997, 238-252. doi:10.1145/512950.512973

Important Links:

Go Back