Formalizing Monitoring Processes for Large-Scale Distributed Systems using Abstract State Machines
Sprache des Vortragstitels:
Englisch
Original Tagungtitel:
1st Workshop on Formal Approaches for Advanced Computing Systems
Sprache des Tagungstitel:
Englisch
Original Kurzfassung:
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.
Forschungs-