Zur Seitenansicht
 

Titelaufnahme

Titel
What You Always Wanted to Know About Model Checking of Fault-Tolerant Distributed Algorithms
VerfasserKonnov, Igor ; Veith, Helmut In der Gemeinsamen Normdatei der DNB nachschlagen ; Widder, Josef In der Gemeinsamen Normdatei der DNB nachschlagen
Erschienen in
PSI 2015, Springer International Publishing Switzerland, 2016, S. 6-21
Erschienen2016
Ausgabe
Accepted version
SpracheEnglisch
SerieLNCS ; 9609
DokumenttypAufsatz in einem Sammelwerk
Projekt-/ReportnummerS11403
Projekt-/ReportnummerS11405
Projekt-/ReportnummerP27722
Projekt-/ReportnummerICT15-103
URNurn:nbn:at:at-ubtuw:3-2942 Persistent Identifier (URN)
DOI10.1007/978-3-319-41579-6_2 
Zugriffsbeschränkung
 Das Werk ist frei verfügbar
Dateien
What You Always Wanted to Know About Model Checking of Fault-Tolerant Distributed Algorithms [0.33 mb]
Links
Nachweis
Klassifikation
Zusammenfassung (Englisch)

Distributed algorithms have numerous mission-critical applications in embedded avionic and automotive systems, cloud computing, computer networks, hardware design, and the internet of things. Although distributed algorithms exhibit complex interactions with their computing environment and are difficult to understand for human engineers, computer science has developed only very limited tool support to catch logical errors in distributed algorithms at design time.

In the last two decades we have witnessed a revolutionary progress in software model checking due to the development of powerful techniques such as abstract model checking, SMT solving, and partial order reduction. Still, model checking of fault-tolerant distributed algorithms poses multiple research challenges, most notably parameterized verification: verifying an algorithm for all system sizes and different combinations of faults. In this paper, we survey our recent results in this area which extend and combine abstraction, partial orders, and bounded model checking. Our results demonstrate that model checking has acquired sufficient critical mass to build the theory and the practical tools for the formal verification of large classes of distributed algorithms.