|
1 @inproceedings{ZhangUrbanWu12, |
|
2 author = {X.~Zhang and C.~Urban and C.~Wu}, |
|
3 title = {{P}riority {I}nheritance {P}rotocol {P}roved {C}orrect}, |
|
4 booktitle = {Proc.~of the 3rd Conference on Interactive Theorem Proving}, |
|
5 year = {2012}, |
|
6 pages = {217--232}, |
|
7 series = {LNCS}, |
|
8 volume = {7406} |
|
9 } |
|
10 |
|
11 @Book{Paulson96, |
|
12 author = {L.~C.~Paulson}, |
|
13 title = {{ML} for the {W}orking {P}rogrammer}, |
|
14 publisher = {Cambridge University Press}, |
|
15 year = {1996} |
|
16 } |
|
17 |
|
18 |
|
19 @Manual{LINUX, |
|
20 author = {S.~Rostedt}, |
|
21 title = {{RT}-{M}utex {I}mplementation {D}esign}, |
|
22 note = {Linux Kernel Distribution at, |
|
23 www.kernel.org/doc/Documentation/rt-mutex-design.txt} |
|
24 } |
|
25 |
|
26 @Misc{PINTOS, |
|
27 author = {B.~Pfaff}, |
|
28 title = {{PINTOS}}, |
|
29 note = {\url{http://www.stanford.edu/class/cs140/projects/}}, |
|
30 } |
|
31 |
|
32 |
|
33 @inproceedings{Haftmann08, |
|
34 author = {F.~Haftmann and M.~Wenzel}, |
|
35 title = {{L}ocal {T}heory {S}pecifications in {I}sabelle/{I}sar}, |
|
36 booktitle = {Proc.~of the International Conference on Types, Proofs and Programs (TYPES)}, |
|
37 year = {2008}, |
|
38 pages = {153-168}, |
|
39 series = {LNCS}, |
|
40 volume = {5497} |
|
41 } |
|
42 |
|
43 |
|
44 @TechReport{Yodaiken02, |
|
45 author = {V.~Yodaiken}, |
|
46 title = {{A}gainst {P}riority {I}nheritance}, |
|
47 institution = {Finite State Machine Labs (FSMLabs)}, |
|
48 year = {2004} |
|
49 } |
|
50 |
|
51 |
|
52 @Book{Vahalia96, |
|
53 author = {U.~Vahalia}, |
|
54 title = {{UNIX} {I}nternals: {T}he {N}ew {F}rontiers}, |
|
55 publisher = {Prentice-Hall}, |
|
56 year = {1996} |
|
57 } |
|
58 |
|
59 @Article{Reeves98, |
|
60 title = "{R}e: {W}hat {R}eally {H}appened on {M}ars?", |
|
61 author = "G.~E.~Reeves", |
|
62 journal = "Risks Forum", |
|
63 year = "1998", |
|
64 number = "54", |
|
65 volume = "19" |
|
66 } |
|
67 |
|
68 @Article{Sha90, |
|
69 title = "{P}riority {I}nheritance {P}rotocols: {A}n {A}pproach to |
|
70 {R}eal-{T}ime {S}ynchronization", |
|
71 author = "L.~Sha and R.~Rajkumar and J.~P.~Lehoczky", |
|
72 journal = "IEEE Transactions on Computers", |
|
73 year = "1990", |
|
74 number = "9", |
|
75 volume = "39", |
|
76 pages = "1175--1185" |
|
77 } |
|
78 |
|
79 |
|
80 @Article{Lampson80, |
|
81 author = "B.~W.~Lampson and D.~D.~Redell", |
|
82 title = "{{E}xperiences with {P}rocesses and {M}onitors in {M}esa}", |
|
83 journal = "Communications of the ACM", |
|
84 volume = "23", |
|
85 number = "2", |
|
86 pages = "105--117", |
|
87 year = "1980" |
|
88 } |
|
89 |
|
90 @inproceedings{Wang09, |
|
91 author = {J.~Wang and H.~Yang and X.~Zhang}, |
|
92 title = {{L}iveness {R}easoning with {I}sabelle/{HOL}}, |
|
93 booktitle = {Proc.~of the 22nd International Conference on Theorem Proving in |
|
94 Higher Order Logics (TPHOLs)}, |
|
95 year = {2009}, |
|
96 pages = {485--499}, |
|
97 volume = {5674}, |
|
98 series = {LNCS} |
|
99 } |
|
100 |
|
101 @PhdThesis{Faria08, |
|
102 author = {J.~M.~S.~Faria}, |
|
103 title = {{F}ormal {D}evelopment of {S}olutions for {R}eal-{T}ime {O}perating {S}ystems |
|
104 with {TLA+/TLC}}, |
|
105 school = {University of Porto}, |
|
106 year = {2008} |
|
107 } |
|
108 |
|
109 |
|
110 @Article{Paulson98, |
|
111 author = {L.~C.~Paulson}, |
|
112 title = {{T}he {I}nductive {A}pproach to {V}erifying {C}ryptographic {P}rotocols}, |
|
113 journal = {Journal of Computer Security}, |
|
114 year = {1998}, |
|
115 volume = {6}, |
|
116 number = {1--2}, |
|
117 pages = {85--128} |
|
118 } |
|
119 |
|
120 @MISC{locke-july02, |
|
121 author = {D. Locke}, |
|
122 title = {Priority Inheritance: The Real Story}, |
|
123 month = July, |
|
124 year = {2002}, |
|
125 howpublished={\url{http://www.math.unipd.it/~tullio/SCD/2007/Materiale/Locke.pdf}}, |
|
126 } |
|
127 |
|
128 |
|
129 @InProceedings{Steinberg10, |
|
130 author = {U.~Steinberg and A.~B\"otcher and B.~Kauer}, |
|
131 title = {{T}imeslice {D}onation in {C}omponent-{B}ased {S}ystems}, |
|
132 booktitle = {Proc.~of the 6th International Workshop on Operating Systems |
|
133 Platforms for Embedded Real-Time Applications (OSPERT)}, |
|
134 pages = {16--23}, |
|
135 year = {2010} |
|
136 } |
|
137 |
|
138 @inproceedings{dutertre99b, |
|
139 title = "{T}he {P}riority {C}eiling {P}rotocol: {F}ormalization and |
|
140 {A}nalysis {U}sing {PVS}", |
|
141 author = "B.~Dutertre", |
|
142 booktitle = {Proc.~of the 21st IEEE Conference on Real-Time Systems Symposium (RTSS)}, |
|
143 year = {2000}, |
|
144 pages = {151--160}, |
|
145 publisher = {IEEE Computer Society} |
|
146 } |
|
147 |
|
148 @InProceedings{Jahier09, |
|
149 title = "{S}ynchronous {M}odeling and {V}alidation of {P}riority |
|
150 {I}nheritance {S}chedulers", |
|
151 author = "E.~Jahier and B.~Halbwachs and P.~Raymond", |
|
152 booktitle = "Proc.~of the 12th International Conference on Fundamental |
|
153 Approaches to Software Engineering (FASE)", |
|
154 year = "2009", |
|
155 volume = "5503", |
|
156 series = "LNCS", |
|
157 pages = "140--154" |
|
158 } |
|
159 |
|
160 @InProceedings{Wellings07, |
|
161 title = "{I}ntegrating {P}riority {I}nheritance {A}lgorithms in the {R}eal-{T}ime |
|
162 {S}pecification for {J}ava", |
|
163 author = "A.~Wellings and A.~Burns and O.~M.~Santos and B.~M.~Brosgol", |
|
164 publisher = "IEEE Computer Society", |
|
165 year = "2007", |
|
166 booktitle = "Proc.~of the 10th IEEE International Symposium on Object |
|
167 and Component-Oriented Real-Time Distributed Computing (ISORC)", |
|
168 pages = "115--123" |
|
169 } |
|
170 |
|
171 @Article{Wang:2002:SGP, |
|
172 author = "Y. Wang and E. Anceaume and F. Brasileiro and F. |
|
173 Greve and M. Hurfin", |
|
174 title = "Solving the group priority inversion problem in a |
|
175 timed asynchronous system", |
|
176 journal = "IEEE Transactions on Computers", |
|
177 volume = "51", |
|
178 number = "8", |
|
179 pages = "900--915", |
|
180 month = aug, |
|
181 year = "2002", |
|
182 CODEN = "ITCOB4", |
|
183 doi = "http://dx.doi.org/10.1109/TC.2002.1024738", |
|
184 ISSN = "0018-9340 (print), 1557-9956 (electronic)", |
|
185 issn-l = "0018-9340", |
|
186 bibdate = "Tue Jul 5 09:41:56 MDT 2011", |
|
187 bibsource = "http://www.computer.org/tc/; |
|
188 http://www.math.utah.edu/pub/tex/bib/ieeetranscomput2000.bib", |
|
189 URL = "http://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=1024738", |
|
190 acknowledgement = "Nelson H. F. Beebe, University of Utah, Department |
|
191 of Mathematics, 110 LCB, 155 S 1400 E RM 233, Salt Lake |
|
192 City, UT 84112-0090, USA, Tel: +1 801 581 5254, FAX: +1 |
|
193 801 581 4148, e-mail: \path|beebe@math.utah.edu|, |
|
194 \path|beebe@acm.org|, \path|beebe@computer.org| |
|
195 (Internet), URL: |
|
196 \path|http://www.math.utah.edu/~beebe/|", |
|
197 fjournal = "IEEE Transactions on Computers", |
|
198 doi-url = "http://dx.doi.org/10.1109/TC.2002.1024738", |
|
199 } |
|
200 |
|
201 @Article{journals/rts/BabaogluMS93, |
|
202 title = "A Formalization of Priority Inversion", |
|
203 author = "{\"O} Babaoglu and K. Marzullo and F. B. Schneider", |
|
204 journal = "Real-Time Systems", |
|
205 year = "1993", |
|
206 number = "4", |
|
207 volume = "5", |
|
208 bibdate = "2011-06-03", |
|
209 bibsource = "DBLP, |
|
210 http://dblp.uni-trier.de/db/journals/rts/rts5.html#BabaogluMS93", |
|
211 pages = "285--303", |
|
212 URL = "http://dx.doi.org/10.1007/BF01088832", |
|
213 } |
|
214 |