Endüstriyel robotik sistemlerin güvenlik doğrulaması

Bu çalışmada robotik sistemlerin emniyeti için yazılımlarının doğrulamasına yönelik yöntem geliştirmesi amaçlanmaktadır. Robotik sistemlerin karmaşık yapısı nedeni ile yeterince doğrulaması yapılamadan kullanıma başlanabilir. Sonradan ortaya çıkabilecek yazılım hataları nedeni ile maddi ve zaman açısından kayıplar yaşanabileceği gibi insanlarında hayati kazalarla karşılaşmasına neden olabilir. Bundan dolayı bu sistemlerin yazılımlarının emniyet açısından doğrulaması için etkin yöntemlere ihtiyaç vardır. Robotik sistemler için yaygın olarak kullanılan doğrulama yöntemlerinden benzetim ve elle yapılan testler sistemdeki tüm olası durumları değerlendiremediği için yetersiz kalabilmektedir. Bu nedenle güvenlik doğrulamaları için formal yöntemler geliştirilmiştir. Model tabanlı formal yöntemler sistemin tüm durumlarını ve olası durum geçişlerini denetleyebilmektedir. Ancak model oluşturma ve model üzerinden doğrulama yaklaşımlarının güçlükleri robotik sistem geliştirenlerin bu teknikleri kullanmasının önünde bir engel oluşturmaktadır. Bu çalışmada, robotik sistem yazılımlarının modellenmesi ve model üzerinden doğrulanmasını kolaylaştıracak yöntem geliştirilmiştir. Önerilen yöntemde sistem yazılım davranışları zamanlı otomata olarak modellenmektedir. Ancak bu modellerin karmaşıklığını gidermek için robotik sistemlerdeki ortak fonksiyonelliğe sahip bileşenler birer şablon (model blok) olarak tasarlanmaktadır. Bu şablonlar temsil ettikleri fonksiyonu gerçekleştiren zamanlı otomataları içermektedir. Robotik sistem geliştiricileri bu şablonlardan sisteme uygun olanları seçip aralarındaki ilişkileri ve parametrelerini tanımlamaktadır. Önerilen yöntemde, şablonların kullanımı ile oluşturulmuş olan model, doğrulama amaçlı kullanılabilmektedir. Elde edilen modelin doğrulaması için model denetleme tekniği kullanılmaktadır. Bu çalışmada model denetleme tekniğini gerçekleştirmek üzere UPPAAL adlı yazılım aracından faydalanılmaktadır. Önerilen yöntemin uygulanabilirliğini göstermek üzere, iki farklı endüstriyel üretim içeren robotik sistem ele alınmıştır. Anahtar Kelimeler: Model denetimi (model checker), formal doğrulama, robotik sistemler, emniyet sağlama, zamanlı otomatlar