© 2020 Elsevier B.V. Cloud is an increasingly popular computing paradigm that provides on-demand services to organizations for deploying their business processes over the Internet as it reduces their needs to plan ahead for provisioning resources. Cloud providers offer competitive pricing strategies (e.g., on-demand, reserved, and spot) specified based on temporal constraints to accommodate organizations’ changing and last-minute demands. Despite their varieties and benefits to optimize business process deployment cost, using those pricing strategies can lead to violating time constraints and exceeding budget constraints due to inappropriate decisions when allocating cloud resources to business processes. In this paper, we present an approach to guarantee a correct and optimal time-aware allocation of cloud resources to business processes. Correct because time constraints on these processes are not violated. And, optimal because the deployment cost of these processes is minimized. For this purpose, our approach uses timed automata to formally verify the matching between business processes’ temporal constraints and cloud resources’ time availabilities and linear programming to optimize deployment costs. Experiments demonstrate the technical doability of our proposed approach.