Cloud computing is the infrastructure of choice for compute–intensive and data–intensive systems providing a flexible resources for software applications; that is, the processing capacity assigned to an application can be adapted to its needs. Nevertheless, in a cloud pay–per–use model, the number of demanded resources must be taken into account in order to minimise the costs. Our main goal is to reason about a cloud–aware application's resource usage by means of our Timed Process Algebra called BTC (Bounded True Concurrency), that is, to study the trade–offs between an application's response time and resource usage.

Video encoders are software applications that need a lot of resources and work on files of considerable size. Therefore, it seems reasonable to try to take advantage of the capacity offered by cloud computing to accelerate the coding process. The H.264 standard is a wide–spread encoding solution, although other standards are being developed and tested to be the former's successors, such as H.265 or HEVC.

In this paper, the video encoder H.265 will be adapted following the Map/Reduce paradigm in order to be able to be executed in Hadoop. Then, its algebraic formalization will be developed by BTC and validated on a real private cloud environment. The formal model is validated analysing the results of an H.265 encoding Hadoop application and the results show a good fit between the prediction and the observed execution time. Finally, we will carry out a performance evaluation using a a tool called BAL (no acronym) that we have developed for that purpose.