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.

Work-in-Progress: A Formal Approach to Verify Fault Tolerance in Industrial Network Systems / Sacco, Alessio; Marchetto, Guido; Sisto, Riccardo; Valenza, Fulvio. - ELETTRONICO. - (2020), pp. 1-4. (Intervento presentato al convegno 2020 16th IEEE International Conference on Factory Communication Systems (WFCS) tenutosi a Porto, Portugal nel 27-29 April 2020) [10.1109/WFCS47810.2020.9114432].

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

Alessio Sacco;Guido Marchetto;Riccardo Sisto;Fulvio Valenza
2020

Abstract

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.
File in questo prodotto:
File Dimensione Formato  
WFCS_2020_WiP_submitted.pdf

accesso aperto

Descrizione: Articolo principale
Tipologia: 2. Post-print / Author's Accepted Manuscript
Licenza: PUBBLICO - Tutti i diritti riservati
Dimensione 247.21 kB
Formato Adobe PDF
247.21 kB Adobe PDF Visualizza/Apri
09114432.pdf

non disponibili

Tipologia: 2a Post-print versione editoriale / Version of Record
Licenza: Non Pubblico - Accesso privato/ristretto
Dimensione 264.84 kB
Formato Adobe PDF
264.84 kB Adobe PDF   Visualizza/Apri   Richiedi una copia
Pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11583/2842984