Work-in-Progress: A Formal Approach to Verify Fault Tolerance in Industrial Network Systems

Distributed systems are extremely difficult to design and implement correctly because they must handle both system correctness and device failures. Most of the work focuses on the first aspect, and in particular, on the correctness of security and network configuration. The large demand for availability and reliability for critical services is actually pushing new architectures that tolerate faults, but a-priori analysis of redundancy and recovery features is still limited. To this end, we present a framework to design and formally verify the persistence of network properties, even in case of failures. The solution considers both nodes and links failure, and it is based on a formal model that takes both network topology and network device configurations into account. In contrast, most of the existing approaches only consider network topology. By analyzing the formal model, the framework can check whether the specified network services are still available after failures, and in case of success, it outputs a possible configuration of the devices to be used for automatic recovery.