Web services can be described as local autonomous routines communicating with each other through message exchange. Hence a good understanding of the messages defined in each web service is crucial to enabling automatic composition. This paper presents a semantic specification framework for analyzing the functional composability of autonomous web services. As the locally described web services contain both semantics and business protocols, we model the former using ontologies and the latter by finite-state machines. A layered approach is adopted to analyze the web service composability, which shows how to check whether two web services are composable or not. Based on the specification and analysis, a polynomial-time algorithm is devised for checking the composability of web services efficiently.