To provide an effective service-oriented solution for a business problem by composing existing services, it is necessary to explore all available options for providing the required functionality while considering both the users’ preferences between various non-functional properties (NFPs) and any low-level constraints. Existing service composition frameworks often fall short of this ideal, as functional requirements, low-level behavioral constraints, and preferences between non functional properties are often not considered in one unified framework. We propose a new service composition framework that addresses all three of these aspects by integrating existing techniques in requirements engineering, preference reasoning, and model checking. We prove that any composition produced by our framework provides the required high-level functionality, satisfies all low-level constraints, and is at least as preferred (w.r.t. NFPs) as any other possible composition that fulfills the same requirements. We also apply our framework to examples adapted from the existing service composition literature.