PORTO @ 
Archivio Istituzionale della Ricerca
IRIS è la soluzione IT che facilita la raccolta e la gestione dei dati relativi alle attività e ai prodotti della ricerca. Fornisce a ricercatori, amministratori e valutatori gli strumenti per monitorare i risultati della ricerca, aumentarne la visibilità e allocare in modo efficace le risorse disponibili.
EnglishDistributed 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.
| Titolo: | Work-in-Progress: A Formal Approach to Verify Fault Tolerance in Industrial Network Systems | |
| Autori: | ||
| Data di pubblicazione: | 2020 | |
| Abstract: | Distributed systems are extremely difficult to design and implement correctly because they must h...andle 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. | |
| Appare nelle tipologie: | 4.1 Contributo in Atti di convegno |
File in questo prodotto:
| File | Descrizione | Tipologia | Licenza | |
|---|---|---|---|---|
| WFCS_2020_WiP_submitted.pdf | Articolo principale | 2. Post-print / Author's Accepted Manuscript | PUBBLICO - Tutti i diritti riservati | Visibile a tuttiVisualizza/Apri |
| 09114432.pdf | 2a Post-print versione editoriale / Version of Record | Non Pubblico - Accesso privato/ristretto | Administrator Richiedi una copia |
http://hdl.handle.net/11583/2842984
Copyright © 2021