The operation of distributed systems relies on the timely exchange of message data via dependable communication networks. Previous works suggest hardware redundancy for potential faults in the underlying network infrastructure to achieve dependability. However, software faults and faults that cannot be resolved on the hardware level are not considered in the existing literature. This work proposes a new method for software fault-tolerant communication in distributed real-time systems with communication networks that support time-slotted operation and broadcast transmission.Our method implements a dependability plane to be integrated to the existing network stack. It processes dependability information that is piggybacked on application message and uses a time synchronized checkpointing/rollback recovery strategy. The proposed dependability plane is modeled in the framework of timed input/output automata (TIOA) to formally prove its correctness and determine tight bounds for fault-recovery times. Model checking tools are employed to verify the timing and dependability properties of real-time systems. To this end, we present an algorithmic approach for converting TIOA models to be used as input of a well known model checking software tool UPPAL. We apply our dependability plane design and integrate it to a previously developed real-time communications framework. We further verify the TIOA models of the overall protocol stack by employing our algorithmic conversion to UPPAAL.

Dağıtık sistemler güvenilir haberleşme ağlarına ihtiyaç duymaktadır. Her ne kadar güvenilirlikkonusu donanım yedekleme şeklinde literatürde işlenmiş bir konu olsa da yazılım güvenilirliği ve donanım yedekleme ile giderilemeyecek hata durumları ele alınmamıştır. Bu çalışmada, yaygın haberleşme yapan gerçek zamanlı dağıtık sistemlerde hata toleransı sağlanabilmesi için senkronize hata bloğu oluşturma ve geri dönmeye dayalı özgün bir güvenilirlik katman tasarımı önerilmektedir. Bahsi geçen güvenilirlik katmanı Zaman Girişli/Çıkışlı Otomat sentaksı kullanılarak modellenmiştir. Bu sayede hem işlevsel doğruluğunun formal yollarla kanıtlanması sağlanmış hem de hata kurtarma işlemindeki gecikmeler sıkı zaman kısıtları dahilinde öngörülebilmiştir. Zaman Girişli/ Çıkışlı Otomat (TIOA) işçerçevesi dağıtık sistemlerin modellenmesinde, UPPAAL yazılım paketi ise sistem modellemesi, simülasyonu ve doğrulamasında sıklıkla kullanılan araçlardır. Bu çalışmada, TIOA sentaksında modellenen güvenilirlik katmanının UPPAAL ortamına aktarılması için algoritmik bir yöntem geliştirilmiş ve çevrim yapılabilmesi için TIOA modellerinde bulunması gereken özellikler listelenmiştir. Literatürdeki diğer çalışmalardan farklı olarak önerilen çevrim yöntemi gerçek-zamanlı dağıtık sistemler üzerinde kullanılabilmektedir. Çalışma kapsamında gerçek-zamanlı dağıtık ve güvenilir bir haberleşme iş çerçevesi (D3RIP) uygulama örneği olarak verilmektedir.