@Book{Silberschatz13,

  author =    {A.~Silberschatz and P.~B.~Galvin and G.~Gagne},

  title =        {Operating System Concepts},

  publisher =    {John Wiley \& Sons},

  year =         {2013},

  edition =   {9th}

}

@Book{liu00,

  author =    {J.~W.~S.~Liu},

  title =        {{R}eal-{T}ime {S}ystems},

  publisher =    {Prentice Hall},

  year =         {2000}

}

@Book{buttazzo,

  author =    {G.~C.~Buttazzo},

  title =     {{H}ard {R}eal-{T}ime {C}omputing {S}ystems: {P}redictable {S}cheduling 

               {A}lgorithms and {A}pplications},

  publisher =    {Springer},

  year =         {2011},

  edition =   {3rd}

}

@Book{LiYao03,

  author =    {Q.~Li and C.~Yao},

  title =        {Real-Time Concepts for Embedded Systems},

  publisher =    {CRC Press},

  year =         {2003}

}

@Book{Laplante11,

  author = 	 {P.~A.~Laplante and S.~J.~Ovaska},

  title = 	 {{R}eal-{T}ime {S}ystems {D}esign and {A}nalysis: {T}ools for the {P}ractitioner},

  publisher = 	 {Wiley-IEEE Press},

  year = 	 {2011},

  edition = 	 {4th}

}

@TechReport{Xv6,

  author =    {R.~Cox and F.~Kaashoek and R.~Morris},

  title =        {{X}v6: {A} {S}imple, {U}nix-like {T}eaching {O}perating {S}ystem},

  institution =  {MIT},

  year =         {2012}

}

@Misc{Xv6link,

  author = {R.~Cox and F.~Kaashoek and R.~Morris},

  title = {{Xv6}}, 

  note = {\url{http://pdos.csail.mit.edu/6.828/2012/xv6.html}},

}

@inproceedings{ThreadX,

  author    = {Y.~Wang and M.~Saksena},

  title     = {{S}cheduling {F}ixed-{P}riority {T}asks with {P}reemption {T}hreshold},

  booktitle = {Proc.~of the 6th Workshop on Real-Time Computing Systems and Applications (RTCSA)},

  year      = {1999},

  pages     = {328--337}

}

@inproceedings{Regehr,

  author    = {J.~Regehr},

  title     = {{S}cheduling {T}asks with {M}ixed {P}reemption {R}elations for {R}obustness

               to {T}iming {F}aults},

  booktitle = {Proc.~of the 23rd IEEE Real-Time Systems Symposium (RTSS)},

  year      = {2002},

  pages     = {315--326}

}

@INPROCEEDINGS{WINDOWSNT, 

  author={L.~Budin and L.~Jelenkovic}, 

  booktitle={Proc.~of the IEEE International Symposium on 

     Industrial Electronics (ISIE)}, 

  title={{T}ime-{C}onstrained {P}rogramming in {W}indows {NT} {E}nvironment}, 

  year={1999},

  volume={1}, 

  pages={90--94}, 

  }

@article{seL4,

  author =  {G.~Klein and

               J.~Andronick and

               K.~Elphinstone and

               G.~Heiser and

               D.~Cock and

               P.~Derrin and

               D.~Elkaduwe and

               K.~Engelhardt and

               R.~Kolanski and

               M.~Norrish and

               T.~Sewell and

               H.~Tuch and

               S.~Winwood}, 

  title =        {{seL4}: {F}ormal {V}erification of an {OS} {K}ernel},

  journal =      {Communications of the ACM},

  publisher =    {ACM},

  year =         {2010},  

  pages =        {107--115},

  volume =       53, 

  number =       6

}

@article{Davis11,

 author = {R.~I.~Davis and A.~Burns},

 title = {{A} {S}urvey of {H}ard 

          {R}eal-{T}ime {S}cheduling for {M}ultiprocessor {S}ystems},

 journal = {ACM Computing Surveys},

 volume = {43},

 number = {4},

 year = {2011},

 pages = {35:1--35:44}

} 

@phdthesis{Brandenburg11,

    Author = {B.~B.~Brandenburg},

    School = {The University of North Carolina at Chapel Hill},

    Title =  {{S}cheduling and {L}ocking in

              {M}ultiprocessor {R}eal-{T}ime {O}perating {S}ystems},

    Year =   {2011}

}

@inproceedings{ZhangUrbanWu12,

  author    = {X.~Zhang and C.~Urban and C.~Wu},

  title     = {{P}riority {I}nheritance {P}rotocol {P}roved {C}orrect},

  booktitle = {Proc.~of the 3rd Conference on Interactive Theorem Proving (ITP)},

  year      = {2012},

  pages     = {217--232},

  series    = {LNCS},

  volume    = {7406}

}

@Book{Paulson96,

  author = 	 {L.~C.~Paulson},

  title = 	 {{ML} for the {W}orking {P}rogrammer},

  publisher = 	 {Cambridge University Press},

  year = 	 {1996}

}

@Manual{LINUX,

  author =       {S.~Rostedt},

  title =        {{RT}-{M}utex {I}mplementation {D}esign},

  note =         {Linux Kernel Distribution at, 

                  www.kernel.org/doc/Documentation/rt-mutex-design.txt}

}

@Misc{PINTOS,

  author = {B.~Pfaff},

  title = {{PINTOS}}, 

  note = {\url{http://www.stanford.edu/class/cs140/projects/}},

}

@inproceedings{Haftmann08,

  author    = {F.~Haftmann and M.~Wenzel},

  title     = {{L}ocal {T}heory {S}pecifications in {I}sabelle/{I}sar},

  booktitle = {Proc.~of the International Conference on Types, Proofs and Programs (TYPES)},

  year      = {2008},

  pages     = {153-168},

  series    = {LNCS},

  volume    = {5497}

}

@TechReport{Yodaiken02,

  author =       {V.~Yodaiken},

  title =        {{A}gainst {P}riority {I}nheritance},

  institution =  {Finite State Machine Labs (FSMLabs)},

  year =         {2004}

}

@Book{Vahalia96,

  author =       {U.~Vahalia},

  title =        {{UNIX} {I}nternals: {T}he {N}ew {F}rontiers},

  publisher =    {Prentice-Hall},

  year =         {1996}

}

@Article{Reeves98,

  title =	"{R}e: {W}hat {R}eally {H}appened on {M}ars?",

  author =	"G.~E.~Reeves",

  journal =	"Risks Forum",

  year = 	"1998",

  number =	"54",

  volume =	"19"

}

@Article{Sha90,

  title =	"{P}riority {I}nheritance {P}rotocols: {A}n {A}pproach to

		 {R}eal-{T}ime {S}ynchronization",

  author =	"L.~Sha and R.~Rajkumar and J.~P.~Lehoczky",

  journal =	"IEEE Transactions on Computers",

  year = 	"1990",

  number =	"9",

  volume =	"39",

  pages =	"1175--1185"

}

@TechReport{deinheritance,

    author = {P.~J.~Moylan and R.~E.~Betz and R.~H.~Middleton},

    title = {{T}he {P}riority {D}isinheritance {P}roblem},

    institution = {University of Newcastle},

    number = {EE9345},

    year = {1993}

}  

@Book{book,

  author = 	 {R.~Rajkumar},

  title = 	 {{S}ynchronization in {R}eal-{T}ime {S}ystems: 

                  {A} {P}riority {I}nheritance {A}pproach},

  publisher = 	 {Kluwer},

  year = 	 {1991}

}

@Article{Lampson80,

  author =	"B.~W.~Lampson and D.~D.~Redell",

  title =	"{{E}xperiences with {P}rocesses and {M}onitors in {M}esa}",

  journal =	"Communications of the ACM",

  volume =	"23",

  number =	"2",

  pages =	"105--117",

  year = 	"1980"

}

@inproceedings{Wang09,

  author    = {J.~Wang and H.~Yang and X.~Zhang},

  title     = {{L}iveness {R}easoning with {I}sabelle/{HOL}},

  booktitle = {Proc.~of the 22nd International Conference on Theorem Proving in 

               Higher Order Logics (TPHOLs)},

  year      = {2009},

  pages     = {485--499},

  volume    = {5674},

  series    = {LNCS}

}

@PhdThesis{Faria08,

  author =       {J.~M.~S.~Faria},

  title =        {{F}ormal {D}evelopment of {S}olutions for {R}eal-{T}ime {O}perating {S}ystems 

                 with {TLA+/TLC}},

  school =       {University of Porto},

  year =         {2008}

}

@Article{Paulson98,

  author =       {L.~C.~Paulson},

  title =        {{T}he {I}nductive {A}pproach to {V}erifying {C}ryptographic {P}rotocols},

  journal =      {Journal of Computer Security},

  year =         {1998},

  volume =       {6},

  number =       {1--2},

  pages =        {85--128}

}

@MISC{locke-july02,

author = {D. Locke},

title = {Priority Inheritance: The Real Story},

month = July,

year = {2002},

howpublished={\url{http://www.math.unipd.it/~tullio/SCD/2007/Materiale/Locke.pdf}},

}

@InProceedings{Steinberg10,

  author =       {U.~Steinberg and A.~B\"otcher and B.~Kauer},

  title =        {{T}imeslice {D}onation in {C}omponent-{B}ased {S}ystems},

  booktitle = {Proc.~of the 6th International Workshop on Operating Systems

               Platforms for Embedded Real-Time Applications (OSPERT)},

  pages =     {16--23},

  year =      {2010}

}

@inproceedings{dutertre99b,

  title =	"{T}he {P}riority {C}eiling {P}rotocol: {F}ormalization and

		 {A}nalysis {U}sing {PVS}",

  author =	"B.~Dutertre",

  booktitle = {Proc.~of the 21st IEEE Conference on Real-Time Systems Symposium (RTSS)},

  year = {2000},

  pages = {151--160},

  publisher = {IEEE Computer Society}

}

@InProceedings{Jahier09,

  title =	"{S}ynchronous {M}odeling and {V}alidation of {P}riority

		 {I}nheritance {S}chedulers",

  author =	"E.~Jahier and B.~Halbwachs and P.~Raymond",

  booktitle =	"Proc.~of the 12th International Conference on Fundamental 

                 Approaches to Software Engineering (FASE)",

  year = 	"2009",

  volume =	"5503",

  series =      "LNCS",

  pages =	"140--154"

}

@InProceedings{Wellings07,

  title =	"{I}ntegrating {P}riority {I}nheritance {A}lgorithms in the {R}eal-{T}ime 

                 {S}pecification for {J}ava",

  author =	"A.~Wellings and A.~Burns and O.~M.~Santos and B.~M.~Brosgol",

  publisher =	"IEEE Computer Society",

  year = 	"2007",

  booktitle =	"Proc.~of the 10th IEEE International Symposium on Object 

                and Component-Oriented Real-Time Distributed Computing (ISORC)",

  pages =	"115--123"

}

@Article{Wang:2002:SGP,

  author =	"Y. Wang and E. Anceaume and F. Brasileiro and F.

		 Greve and M. Hurfin",

  title =	"Solving the group priority inversion problem in a

		 timed asynchronous system",

  journal =	"IEEE Transactions on Computers",

  volume =	"51",

  number =	"8",

  pages =	"900--915",

  month =	aug,

  year = 	"2002",

  CODEN =	"ITCOB4",

  doi =  	"http://dx.doi.org/10.1109/TC.2002.1024738",

  ISSN = 	"0018-9340 (print), 1557-9956 (electronic)",

  issn-l =	"0018-9340",

  bibdate =	"Tue Jul 5 09:41:56 MDT 2011",

  bibsource =	"http://www.computer.org/tc/;

		 http://www.math.utah.edu/pub/tex/bib/ieeetranscomput2000.bib",

  URL =  	"http://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=1024738",

  acknowledgement = "Nelson H. F. Beebe, University of Utah, Department

		 of Mathematics, 110 LCB, 155 S 1400 E RM 233, Salt Lake

		 City, UT 84112-0090, USA, Tel: +1 801 581 5254, FAX: +1

		 801 581 4148, e-mail: \path|beebe@math.utah.edu|,

		 \path|beebe@acm.org|, \path|beebe@computer.org|

		 (Internet), URL:

		 \path|http://www.math.utah.edu/~beebe/|",

  fjournal =	"IEEE Transactions on Computers",

  doi-url =	"http://dx.doi.org/10.1109/TC.2002.1024738",

}

@Article{journals/rts/BabaogluMS93,

  title =	"A Formalization of Priority Inversion",

  author =	"{\"O} Babaoglu and K. Marzullo and F. B. Schneider",

  journal =	"Real-Time Systems",

  year = 	"1993",

  number =	"4",

  volume =	"5",

  bibdate =	"2011-06-03",

  bibsource =	"DBLP,

		 http://dblp.uni-trier.de/db/journals/rts/rts5.html#BabaogluMS93",

  pages =	"285--303",

  URL =  	"http://dx.doi.org/10.1007/BF01088832",

}