Web services are beginning to play an increasingly important role in scientific, engineering, government, health-care, and business applications. Complex applications call for tools that support users to assemble composite services from independently developed component services to achieve the desired functionality. This research brings together a team of investigators with complementary expertise in formal methods, artificial intelligence, and software engineering to develop novel approaches to service composition that address this need. The main contributions of this research include powerful interactive methods for service composition with provable guarantees with respect to user-specified functional and non-functional requirements. A main focus of the research is on investigation of functional and non-functional failure analysis of composition, and user-guided and automated reformulation of requirements based on such analysis, techniques for handling semantic mismatches between user specifications and service descriptions, and the use of interactive as opposed to fully automated methods. Products of the research include software tools for interactive service composition as well as benchmarks for evaluation of alternative approaches to service composition. Broader impact of the research includes enhanced opportunities for research-based training of graduate students. Results of the research including publications, software, and benchmarks will be disseminated through the project web-page at http://www.moscoe.org.