1: \begin{thebibliography}{10}
2:
3: \bibitem{AD94}
4: R.~Alur and D.~L. Dill.
5: \newblock A theory of timed automata.
6: \newblock {\em Theoretical Computer Science}, 126(2):183--235, Apr. 1994.
7:
8: \bibitem{AH+98}
9: R.~Alur, T.~A. Henzinger, F.~Y.~C. Mang, S.~Qadeer, S.~K. Rajamani, and
10: S.~Tasiran.
11: \newblock {MOCHA}: Modularity in model checking.
12: \newblock In {\em CAV'98}, volume 1427 of {\em Lecture Notes in Computer
13: Science}, pages 521--525. Springer, 1998.
14:
15: \bibitem{AB02}
16: P.~Ammann, P.~E. Black, and W.~Ding.
17: \newblock Model checkers in software testing.
18: \newblock NIST-IR 6777, National Institute of Standards and Technology, 2002.
19:
20: \bibitem{ABM98}
21: P.~Ammann, P.~E. Black, and W.~Majurski.
22: \newblock Using model checking to generate tests from specifications.
23: \newblock In {\em ICFEM'98}, pages 46--. IEEE Computer Society, 1998.
24:
25: \bibitem{BP03}
26: A.~Bertolino and A.~Polini.
27: \newblock A framework for component deployment testing.
28: \newblock In {\em ICSE'03}, pages 221--231. IEEE Computer Society, 2003.
29:
30: \bibitem{BOY00}
31: P.~E. Black, V.~Okun, and Y.~Yesha.
32: \newblock Mutation operators for specifications.
33: \newblock In {\em ASE'00}, pages 81--. IEEE Computer Society, 2000.
34:
35: \bibitem{BW98}
36: A.~Brown and K.~Wallnau.
37: \newblock The current state of {CBSE}.
38: \newblock {\em IEEE Software}, 15(5):37--46, Sep/Oct 1998.
39:
40: \bibitem{CSE96}
41: J.~Callahan, F.~Schneider, and S.~Easterbrook.
42: \newblock Automated software testing using modelchecking.
43: \newblock In {\em SPIN'96}, 1996.
44:
45: \bibitem{CE81}
46: E.~M. Clarke and E.~A. Emerson.
47: \newblock Design and synthesis of synchronization skeletons using branching
48: time temporal logic.
49: \newblock In {\em Workshop of Logic of Programs}, volume 131 of {\em Lecture
50: Notes in Computer Science}. Springer, 1981.
51:
52: \bibitem{CES86}
53: E.~M. Clarke, E.~A. Emerson, and A.~P. Sistla.
54: \newblock Automatic verification of finite-state concurrent systems using
55: temporal logic specifications.
56: \newblock {\em ACM Transactions on Programming Languages and Systems},
57: 8(2):244--263, Apr. 1986.
58:
59: \bibitem{CGP99}
60: E.~M. Clarke, O.~Grumberg, and D.~A. Peled.
61: \newblock {\em Model Checking}.
62: \newblock The MIT Press, 1999.
63:
64: \bibitem{cousotcousot-77}
65: P.~Cousot and R.~Cousot.
66: \newblock Abstract interpretation: a unified lattice model for static analysis
67: of programs by construction or approximation of fixpoints.
68: \newblock In {\em POPL'77}, pages 238--250, 1977.
69:
70: \bibitem{EFM97}
71: A.~Engels, L.~Feijs, and S.~Mauw.
72: \newblock Test generation for intelligent networks using model checking.
73: \newblock In {\em TACAS'97}, volume 1217 of {\em Lecture Notes of Computer
74: Science}, pages 384--398. Springer, 1997.
75:
76: \bibitem{FK01}
77: K.~Fisler and S.~Krishnamurthi.
78: \newblock Modular verification of collaboration-based software designs.
79: \newblock In {\em FSE'01}, pages 152--163. ACM Press, 2001.
80:
81: \bibitem{GH99}
82: A.~Gargantini and C.~Heitmeyer.
83: \newblock Using model checking to generate tests from requirements
84: specifications.
85: \newblock In {\em ESEC/FSE'99}, volume 1687 of {\em Lecture Notes in Computer
86: Science}, pages 146--163. Springer, 1999.
87:
88: \bibitem{GL02}
89: I.~Gorton and A.~Liu.
90: \newblock Software component quality assessment in practice: successes and
91: practical impediments.
92: \newblock In {\em ICSE'02}, pages 555--558. ACM Press, 2002.
93:
94: \bibitem{GPY02}
95: A.~Groce, D.~Peled, and M.~Yannakakis.
96: \newblock Amc: An adaptive model checker.
97: \newblock In {\em CAV'02}, volume 2404 of {\em Lecture Notes in Computer
98: Science}, pages 521--525. Springer, 2002.
99:
100: \bibitem{henzinger98you}
101: T.~A. Henzinger, S.~Qadeer, and S.~K. Rajamani.
102: \newblock You assume, we guarantee: Methodology and case studies.
103: \newblock In {\em CAV'98}, volume 1427 of {\em Lecture Notes in Computer
104: Science}, pages 440--451. Springer, 1998.
105:
106: \bibitem{H97}
107: G.~J. Holzmann.
108: \newblock The model checker {SPIN}.
109: \newblock {\em IEEE Transactions on Software Engineering}, 23(5):279--295, May
110: 1997.
111: \newblock Special Issue: Formal Methods in Software Practice.
112:
113: \bibitem{M93}
114: {K.L. McMillan}.
115: \newblock {\em {S}ymbolic {M}odel {C}hecking}.
116: \newblock Kluwer Academic Publishers, Norwell Massachusetts, 1993.
117:
118: \bibitem{KB98}
119: W.~Kozaczynski and G.~Booch.
120: \newblock Component-based software engineering.
121: \newblock {\em IEEE Software}, 15(5):34--36, Sep/Oct 1998.
122:
123: \bibitem{KV97}
124: O.~Kupferman and M.~Vardi.
125: \newblock Module checking revisited.
126: \newblock In {\em CAV'97}, volume 1254 of {\em Lecture Notes in Computer
127: Science}, pages 36--47. Springer, 1997.
128:
129: \bibitem{Lam83}
130: L.~Lamport.
131: \newblock Specifying concurrent program modules.
132: \newblock {\em ACM Transactions on Programming Languages and Systems (TOPLAS)},
133: 5(2):190--222, 1983.
134:
135: \bibitem{LKF02}
136: H.~Li, S.~Krishnamurthi, and K.~Fisler.
137: \newblock Verifying cross-cutting features as open systems.
138: \newblock {\em ACM SIGSOFT Software Engineering Notes}, 27(6):89--98, 2002.
139:
140: \bibitem{Ariane}
141: J.~L. Lions.
142: \newblock Ariane 5 flight 501 failure report by the inquiry board, July 1996,
143: {http://java.sun.com/people/jag/Ariane5.html}.
144:
145: \bibitem{lynch87hierarchical}
146: N.~Lynch and M.~Tuttle.
147: \newblock Hierarchical correctness proofs for distributed algorithms.
148: \newblock Proc. 6th ACM Symp. on Principles of Distributed Computing, pp.
149: 137--151, 1987.
150:
151: \bibitem{ME03}
152: S.~McCamant and M.~D. Ernst.
153: \newblock Predicting problems caused by component upgrades.
154: \newblock In {\em FSE'03}, pages 287--296. ACM Press, 2003.
155:
156: \bibitem{OHR01}
157: A.~Orso, M.~J. Harrold, and D.~Rosenblum.
158: \newblock Component metadata for software engineering tasks.
159: \newblock volume 1999 of {\em Lecture Notes in Computer Science}, pages
160: 129--144, 2001.
161:
162: \bibitem{Peled03CAV}
163: D.~Peled.
164: \newblock Model checking and testing combined.
165: \newblock In {\em ICALP'03}, volume 2719 of {\em Lecture Notes in Computer
166: Science}, pages 47--63. Springer, 2003.
167:
168: \bibitem{PVY99}
169: D.~Peled, M.~Y. Vardi, and M.~Yannakakis.
170: \newblock Black box checking.
171: \newblock In {\em {FORTE}/{PSTV}'99}, pages 225--240. Kluwer, 1999.
172:
173: \bibitem{Pnu85}
174: A.~Pnueli.
175: \newblock In transition from global to modular temporal reasoning about
176: programs, 1985.
177: \newblock In K.R. Apt, editor, Logics and Models of Concurrent Systems,
178: sub-series F: Computer and System Science.
179:
180: \bibitem{Rosenblum97}
181: D.~Rosenblum.
182: \newblock Adequate testing of component based software, 1997.
183: \newblock Department of Information and Computer Science, University of
184: California, Irvine, Irvine, CA, Technical Report 97-34, August 1997.
185:
186: \bibitem{SC85}
187: A.~P. Sistla and E.~M. Clarke.
188: \newblock Complexity of propositional temporal logics.
189: \newblock {\em Journal of ACM}, 32(3):733--749, 1983.
190:
191: \bibitem{SW00}
192: J.~Stafford and A.~Wolf.
193: \newblock Annotating components to support component-based static analyses of
194: software systems.
195: \newblock Proceedings of the Grace Hopper Celebration of Women in Computing
196: 2000, Hyannis, Massachusetts, September 2000.
197:
198: \bibitem{SZY03}
199: C.~Szyperski.
200: \newblock Component technology: what, where, and how?
201: \newblock In {\em ICSE'03}, pages 684--693. IEEE Computer Society, 2003.
202:
203: \bibitem{VW86}
204: M.~Y. Vardi and P.~Wolper.
205: \newblock An automata-theoretic approach to automatic program verification
206: (preliminary report).
207: \newblock In {\em {LICS}'86}, pages 332--344. IEEE Computer Society, 1986.
208:
209: \bibitem{Voas98}
210: J.~Voas.
211: \newblock Certifying off-the-shelf software components.
212: \newblock {\em IEEE Computer}, 31(6):53--59, June 1998.
213:
214: \bibitem{Voas00}
215: J.~Voas.
216: \newblock Developing a usage-based software certification process.
217: \newblock {\em IEEE Computer}, 33(8):32--37, August 2000.
218:
219: \bibitem{WML02}
220: J.~Whaley, M.~C. Martin, and M.~S. Lam.
221: \newblock Automatic extraction of object-oriented component interfaces.
222: \newblock In {\em ISSTA'02}, pages 218--228. ACM Press, 2002.
223:
224: \end{thebibliography}
225: