xie_dang.bbl
\begin{thebibliography}{10}

\bibitem{grail}
Grail homepage.
\newblock http://www.csd.uwo.ca/research/grail/.

\bibitem{AL93}
Mart�n Abadi and Leslie Lamport.
\newblock Composing specifications.
\newblock {\em TOPLAS}, 15(1):73--132, 1993.

\bibitem{AH+98}
Rajeev Alur, Thomas~A. Henzinger, Freddy Y.~C. Mang, Shaz Qadeer, Sriram~K.
  Rajamani, and Serdar Tasiran.
\newblock {MOCHA}: Modularity in model checking.
\newblock In {\em CAV'98}, volume 1427 of {\em LNCS}, pages 521--525. Springer,
  1998.

\bibitem{BP03}
A.~Bertolino and A.~Polini.
\newblock A framework for component deployment testing.
\newblock In {\em ICSE'03}, pages 221--231. IEEE Press, 2003.

\bibitem{692525}
Ed~Brinksma and Jan Tretmans.
\newblock Testing transition systems: An annotated bibliography.
\newblock In {\em Proc. 4th Summer School on Modeling and Verification of
  Parallel Processes}, pages 187--195. Springer-Verlag, 2001.

\bibitem{CSE96}
J.~Callahan, F.~Schneider, and S.~Easterbrook.
\newblock Automated software testing using modelchecking.
\newblock WVU Technical Report \#NASA-IVV-96-022.

\bibitem{CLM89}
E.~Clarke, D.~Long, and K.~McMillan.
\newblock Compositional model checking.
\newblock In {\em LICS'89}, pages 353--362. IEEE Press, 1989.

\bibitem{CGK97}
A.~Coen-Porisini, C.~Ghezzi, and R.~A. Kemmerer.
\newblock Specification of realtime systems using {ASTRAL}.
\newblock {\em TSE}, 23(9):572--598, 1997.

\bibitem{AlfaroHenzinger2001}
Luca de~Alfaro and Thomas~A. Henzinger.
\newblock Interface automata.
\newblock In {\em FSE'01}, pages 109--120. ACM Press, 2001.

\bibitem{EFM97}
A.~Engels, L.M.G. Feijs, and S.~Mauw.
\newblock Test generation for intelligent networks using model checking.
\newblock In {\em TACAS'97}, volume 1217 of {\em LNCS}, pages 384--398.
  Springer, 1997.

\bibitem{FK01}
Kathi Fisler and Shriram Krishnamurthi.
\newblock Modular verification of collaboration-based software designs.
\newblock In {\em ESEC/FSE'01}, pages 152--163. ACM Press, 2001.

\bibitem{FQ03}
C.~Flanagan and S.~Qadeer.
\newblock Thread-modular model checking.
\newblock In {\em SPIN'03}, volume 2648 of {\em LNCS}, pages 213--225.
  Springer, 2003.

\bibitem{GH99}
Angelo Gargantini and Constance Heitmeyer.
\newblock Using model checking to generate tests from requirements
  specifications.
\newblock In {\em ESEC/FSE'99}, volume 1687 of {\em LNCS}, pages 146--163.
  Springer, 1999.

\bibitem{GhoshMathur99}
S.~Ghosh and P.~Mathur.
\newblock Issues in testing distributed component-based systems.
\newblock In {\em First ICSE Workshop on Testing Distributed Component-Based
  Systems}, 1999.

\bibitem{Giannakopoulou04}
Dimitra Giannakopoulou, Corina~S. Pasareanu, and Jamieson~M. Cobleigh.
\newblock Assume-guarantee verification of source code with design-level
  assumptions.
\newblock In {\em ICSE'04}, pages 211--220. IEEE Press, 2004.

\bibitem{336532}
Mary~Jean Harrold.
\newblock Testing: a roadmap.
\newblock In {\em Proceedings of the conference on the future of software
  engineering}, pages 61--72. ACM Press, 2000.

\bibitem{HenzingerJhalaMajumdar}
Thomas~A. Henzinger, Ranjit Jhala, Rupak Majumdar, , and Shaz Qadeer.
\newblock Thread-modular abstraction refinement.
\newblock In {\em CAV'03}, volume 2725 of {\em LNCS}, pages 262--274. Springer,
  2003.

\bibitem{DH03}
Ralph~D. Jeffords and Constance~L. Heitmeyer.
\newblock A strategy for efficiently verifying requirements.
\newblock In {\em FSE'03}, pages 28--37. ACM Press, 2003.

\bibitem{Jon83}
C.B. Jones.
\newblock Tentative steps towards a development method for interfering
  programs.
\newblock {\em TOPLAS}, 5(4):596--619, 1983.

\bibitem{570533}
Pramod~V. Koppol, Richard~H. Carver, and Kuo-Chung Tai.
\newblock Incremental integration testing of concurrent programs.
\newblock {\em TSE}, 28(6):607--623, 2002.

\bibitem{Lam83}
Leslie Lamport.
\newblock Specifying concurrent program modules.
\newblock {\em TOPLAS}, 5(2):190--222, 1983.

\bibitem{LKF02}
Harry Li, Shriram Krishnamurthi, and Kathi Fisler.
\newblock Verifying cross-cutting features as open systems.
\newblock {\em ACM SIGSOFT Software Engineering Notes}, 27(6):89--98, 2002.

\bibitem{lynch87hierarchical}
N.~Lynch and M.~Tuttle.
\newblock An introduction to input/output automata.
\newblock {\em CWI-Quarterly}, 2(3):219--246, 1989.

\bibitem{1007520}
Lev Nachmanson, Margus Veanes, Wolfram Schulte, Nikolai Tillmann, and Wolfgang
  Grieskamp.
\newblock Optimal strategies for testing nondeterministic systems.
\newblock In {\em ISSTA'04}, pages 55--64. ACM Press, 2004.

\bibitem{OHR01}
Alessandro Orso, Mary~Jean Harrold, and David~S. Rosenblum.
\newblock Component metadata for software engineering tasks.
\newblock In {\em EDO'00}, volume 1999 of {\em LNCS}, pages 129--144. Springer,
  2000.

\bibitem{PVY99}
Doron Peled, Moshe~Y. Vardi, and Mihalis Yannakakis.
\newblock Black box checking.
\newblock In {\em {FORTE}/{PSTV}'99}, pages 225--240. Kluwer, 1999.

\bibitem{IO03}
Alexandre Petrenko, Nina Yevtushenko, and Jia~Le Huo.
\newblock Testing transition systems with input and output testers.
\newblock In {\em TestCom'03}, volume 2644 of {\em LNCS}, pages 129 -- 145.
  Springer, 2003.

\bibitem{Pnu85}
A.~Pnueli.
\newblock In transition from global to modular temporal reasoning about
  programs, 1985.
\newblock In K.R. Apt, editor, Logics and Models of Concurrent Systems,
  sub-series F: Computer and System Science.

\bibitem{Rosenblum97}
D.~Rosenblum.
\newblock Adequate testing of componentbased software.
\newblock Department of Information and Computer Science, University of
  California, Irvine, Technical Report 97-34, August 1997.

\bibitem{SZY03}
C.~Szyperski.
\newblock Component technology: what, where, and how?
\newblock In {\em ICSE'03}, pages 684--693. IEEE Press, 2003.

\bibitem{TC96}
C.~Tai and R.~H. Carver.
\newblock Testing of distributed programs.
\newblock In {\em Parallel and Distributed Computing Handbook}, pages 955--978.
  McGraw-Hill, 1996.

\bibitem{torx}
Jan Tretmans and Ed~Brinksma.
\newblock Torx: Automated model-based tesing.
\newblock In {\em First European Conference on Model-Driven Software
  Engineering}, pages 31--43, 2003.

\bibitem{Voas00}
J.~Voas.
\newblock Developing a usage-based software certification process.
\newblock {\em IEEE Computer}, 33(8):32--37, August 2000.

\bibitem{WML02}
John Whaley, Michael~C. Martin, and Monica~S. Lam.
\newblock Automatic extraction of object-oriented component interfaces.
\newblock In {\em ISSTA'02}, pages 218--228. ACM Press, 2002.

\bibitem{XD2004FSE}
Gaoyan Xie and Zhe Dang.
\newblock Model-checking driven black-box testing algorithms for systems with
  unspecified components.
\newblock In {\em FATES'04}, LNCS, (to appear).

\end{thebibliography}
