As of today, modern software is already provided as-a-service and no longer sold as monolithic application. Tomorrow, with visions as on-the-fly computing, these services will be created automatically, composed from existing services according to the request of a user, based in an actual business domain. Therefore, correctness of such a composition has to be guaranteed on the fly, as well.Verifying software in an on-the-fly context leads to a major challenge: It can only yield results if it is rooted in formal specification. At the same time, verification meets the domains of service description, composition, and knowledge modeling, all using different formalisms with different semantics. Therefore, we need a framework which enables domain knowledge modeling as well as service and composition specification, while at the same time using a shared theoretical foundation to enable formal verification.This thesis provides such a framework. It uses predicate logic as a common ground to build an integrated framework to model knowledge, use this knowledge to create service descriptions, and to define a workflow, or composition, language. Additionally, it lifts compositions to templates, and provides a semantics which is parameterized not only in the logical structures, but also in the possible instantiations of templates in arbitrary business domains.It also provides a sound and complete proof calculus to show correctness of templates. Additionally, it leverages the use of the framework in an on-the-fly context by replacing the need of composition verification with a check of side conditions of a template during instantiation, and by providing an encoding of correctness checks to make use of automatic verification using satisfiability solvers.