Endüstriyel robotik sistemlerin güvenlik doğrulaması
Safety verification of industrial robotic systems
Yazar: FATİH FURKAN ARSLAN
Danışman: PROF. DR. METİN ÖZKAN
Eskişehir Osmangazi Üniversitesi / Fen Bilimleri Enstitüsü / Bilgisayar Mühendisliği Ana Bilim Dalı / Yazılım Mühendisliği Bilim Dalı
Derece: Yüksek Lisans, 2024
Konu: Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrol = Computer Engineering and Computer Science and Control

Özet:
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

Abstract:
In this master's study, security problems and security verifications arising from the
interaction of robotic systems with the environment and with each other are discussed. Safety
in robotic systems is an area where comprehensive and satisfactory results should be
obtained. For robotic systems, it is necessary to provide security according to certain
conditions and situations. Traditional methods may be insufficient in the security verification
of software developed for robotic systems. For this reason, formal methods have been
developed for security verifications. To use formal methods, a specific problem that the
robotic system is expected to be tested for is described. The type of formal method to be
used in accordance with the defined problem is determined. Within the scope of this study,
a problem has been prepared for the use of formal verification methods in robotic systems.
In this direction, scenarios were created for different products walking on the conveyor belt
to be picked up by robotic arms and transferred to the points where they belong. Model
inspection method is used in order to make the most appropriate security verification
according to the current problem in the robotic system. In this method, the UPPAAL tool,
which provides modeling of real­time systems, is preferred. In this study, scenarios are
prepared for the current problem and security verifications are made using the relevant
modules in the vehicle. It is seen that similar models are made for similar scenarios in line
with the examinations on the models prepared in the UPPAAL tool according to the
scenarios. Based on these similarities, a general template was prepared for robotic arm
systems with similar scenarios and it was revealed whether it is applicable when creating
different models. The use of the UPPAAL tool and the security validation of the models are
included in the scope of this study, while the scenario­based models prepared within the
scope of the problem are experimentally demonstrated.
Keywords: Model checker, formal verification, robotic systems, safety, timed
automatons