@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 = {Bj\"{o}rn 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",}