ABSTRACT
Abstract. Cloud computing offers a pay-on-demand scalable infrastructure for data processing. Resource-aware services can exploit this infrastructure to elastically adapt to client traffic according to internal resource policies which balance provided QoS with the accrued costs of deployment. This paper presents initial work on worst-case response time analysis for services which distribute tasks to virtual machine instances with different processing speeds. We extend JML-like interfaces with response time annotations and develop a Hoare-style proof system to reason about response time guarantees for services expressed in a simple object-oriented language in which dynamically created objects differ in processing capacity. The simplified setting considered in this paper does not consider loops, concurrency, or reflection; we briefly discuss how these restrictions could be lifted.
