Formal Verification of Time-Aware Cloud Resource Allocation in Business Process

Cloud computing has become an essential ingredient for any modern enterprise information systems infrastructure to effectively facilitate business-process execution with a low operating cost. Most of pricing strategies proposed by Cloud providers are based on temporal dimension. That is why time is considered one of the most important Cloud resources properties. In addition, activities in the business process are also constrained by hard timing requirements. Therefore, it is essential to ensure the matching between temporal constraints of both Cloud resources and business process activities. The aim of the present paper is to ensure a consistent time-aware Cloud resource allocation: we propose to formally specify temporal constraints on cloud resources and on process activities in business processes. This specification is translated to timed automata in order to formally validate the consistency of the time-aware Cloud resource allocation, and to analyze and check its correctness against business-process temporal constraints.