A method of modeling for datacenters computer monitoring system customization based on TLA

摘要

Heterogeneous device access integration technology is an important part of monitoring system. Since customization system is reasonably complex and needs a high level of confidence on discrete and ordered, formal methods are useful. In fact, the design of devices and interfaces were strongly based on formal methods, where the Temporal logic of action + (TLA+) language and its associated model-checker, TLC, were the supporting design tool. Customization method was proposed by using formal specification and verification. Finally, the case for modeling of customization and verification is provided.