--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/document/root.bib Thu Dec 06 15:12:49 2012 +0000
@@ -0,0 +1,205 @@
+
+@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",
+}
+