| dc.description.abstract | A paradigm shift has occurred in the Information and Communication Technology sector. The main obstacle to relegate complex and sensitive tasks is not the inadequate speed and unsatisfactory computing power of the existing machines. However, the inability to design and implement the systems, with a desirable degree of confidence in the correctness and reliability, under different circumstances, has crept in to be the primary concerns in achieving high performance. The hardware and software systems are growing inevitably in scale and functionality, such as cloud computing systems and Data Center (DC). In the said perspective, the complexity of the systems is also increasing. The likelihood of elusive errors is directly proportional to the complexity of the systems that also increase the cost of errors while the systems are operational. In large scale systems the density of computational devices is in order of tens of thousands of servers. Moreover, the effects of errors and miscalculations are substantial. Furthermore, if the specified quality of service is not delivered by the cloud service providers, then the reputation may fall down and users will not use the services, resulting in huge financial lose. Therefore, the reliability, robustness, and availability of systems are very essential. In the said perspective, to increase the reliability and correctness of the systems, we propose the use of Formal Methods (FM). The FM use sound mathematical foundations to prove program correctness. The aim of our research is to deploy various FM tools and techniques to formally analyze the behavior and correctness of the strategies, such as routing algorithms and virtualization models that are implemented in large scale computing systems. The goal of our research is to thoroughly study the strategies, highlight the grey areas that can be further exploit to increase the reliability and performance, and propose a feasible solution. The large scale computing systems, specifically DC exhibits different architectural characteristics, such as predefined complex architectural and topological pattern composed in different layers. The aforementioned characteristics of the underlying network along with the large scale of the servers situate several challenges for the adoption of FMs strategies. | en_US |
