Formalizing Monitoring Processes for Large-Scale Distributed Systems using Abstract State Machines
Sprache des Vortragstitels:
1st Workshop on Formal Approaches for Advanced Computing Systems
Sprache des Tagungstitel:
Large-Scale Distributed Systems are characterized by high complexity and heterogeneity, which might lead to unexpected failures. The role of a robust monitoring framework is to gather low-level data and assess the status of the components of the system. The framework collaborates with adapters for ensuring steady recovery plans and improving the availability of services. Monitors, as part of the system, are also affected by unavailability or random failures. In order to increase the reliability of the solution we verify the trustworthiness of the monitors and emphasize the need of redundancy. This paper introduces a formal approach for modeling and verifying a monitoring solution for an application designed for smart cities. We formalize the behavior of the monitors with the aid of Abstract State Machines and employ the ASMETA toolset for simulating and analyzing properties of the model. The tool also supports the verification process by translating a simplified
version of the model to an NuSMV specification, on top of which model checking can be applied. Properties of the model are expressed with the aid of computation tree logic.