Web service composition is an important topic. Typically, no single service can fulfil all user requirements for a system. Specifying and analysing the non-functional properties (NFPs) is essential to successful service composition. Only where NFPs have been specified, can we choose between services with similar or identical functionality, based on which would better satisfy our non-functional requirements. Specifying NFPs is a complex issue as there are dependencies between them and different factors that influence them (e.g., usage profiles, resources, composition type). Formal models, which can allow precise analysis, are created by abstracting from those factors to determine the relevant concepts for the specification of service NFPs. In this paper we discuss general requirements on specification languages for NFPs of services and their composition. We then specifically discuss our plans for a specification language and analysis technique for provenance awareness. Index Terms — Non-functional properties, Provenance Awareness, Formal Specification, SOA, Web Service Composition.