A formal approach to verify software scalability requirements using set theory and Hoare triple

Scalability is the ability of a system to handle variation in execution environment and continuing to function in order to meet user needs. For ensuring scalability, it is important to verify that programmers are writing code that can scale. However, verifying scalability from code level has its own limitations as it did not receive adequate attention from researchers. This paper proposes a formal approach to verify scalability from the code level using set theory and Hoare triple. The method denotes variables and functions involving scalability through set notations. Hoare triple is used to measure the performance fulfillment with varying workload by a code segment given that certain code quality measure like caching or data compression is applied. The methodology is presented by means of an algorithm which strictly inhibits to passover a specific scalability requirement and requires to re-apply a quality measure until a specific requirement is being satisfied. The approach is applied for developing a real life online ticketing system and results show that it provides stable response time over a wide range of user requests. This indicates that the proposed approach is capable of ensuring scalability by verifying it from system's code.