@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"
}
@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",
}