diff -r 0f2d4b78f839 -r 7f2493296c39 Journal/document/root.bib --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Journal/document/root.bib Mon Dec 17 12:34:24 2012 +0000 @@ -0,0 +1,214 @@ +@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}, + 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", +} +