Verification and validation of robotic systems's safety
Robotik sistemlerin emniyetinin doğrulanması ve onaylanması
Yazar: ZEKERİYYA DEMİRCİ
Danışman: PROF. DR. AHMET YAZICI ; DOÇ. DR. METİN ÖZKAN
Eskişehir Osmangazi Üniversitesi / Fen Bilimleri Enstitüsü / Bilgisayar Mühendisliği Ana Bilim Dalı
Derece: Yüksek Lisans, 2023
Konu: Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrol = Computer Engineering and Computer Science and Control
Dizin: Formel doğrulama = Formal verification ; Model doğrulama = Model check

Özet:
Robotik sistemler, gün geçtikçe artan kabiliyetleri sayesinde başta endüstri olmak
üzere savunma, hizmet, sağlık ve tarım gibi çok çeşitli alanlarda uygulamalarda yer
almaktadırlar. Belirli bir işi yapmak üzere programlanan robotlar aynı işi tekrar tekrar,
yüksek verimlilikte ve kalitede yapabilmektedir. Bu, insan faktöründen kaynaklı hataların
azaltılmasına ve işlemlerin daha hızlı tamamlanmasına olanak tanır. Ayrıca, robotik
sistemler, işlemlerin kesintisiz bir şekilde yapılmasına ve aynı zamanda enerji tasarrufu
sağlamasına yardımcı olabilir. Bu nedenle robotik sistemler birçok sektörde verimliliği
arttırmak için kullanılmaktadır. Robotlar, bazı görevlerde tamamen insanların yerini alırken
bazı görevlerde ise insanlarla birlikte çalışabilirler. Robotik sistemlerin insanlarla aynı
çalışma ortamını paylaşması, çeşitli emniyet endişeleri doğurabilir. Robotik sistemlerin
hatalı veya yanlış programlanması sonucu insanlara zarar verebilmesi mümkündür. Ayrıca,
robotların hızlı hareket etmesi veya yüksek güçlere sahip olması durumunda, yanlış
kullanıldığında veya kontrol edilemediğinde ciddi yaralanmalara neden olabileceği gibi
ölümcül kazalara da sebebiyet verebilir. Robotlar, insanlara zarar vermemek için belirli bir
emniyet mesafesi korunması gerektiği gibi insanların robotların hareketleri veya faaliyetleri
hakkında doğru bilgiye sahip olması da hayati önem taşır. Bu nedenle, robotik sistemlerin
emniyeti için uygun önlemlerin alınması ve çalışma ortamlarının robotlarla birlikte
çalışmaya uygun hale getirilmesi gerekmektedir. Bu nedenle, robotik sistemlerin istenilen
davranışları sergilediğinden emin olmak için yazılım geliştirme sürecinde doğrulama ve
onaylama yöntemlerini kullanmak kritik öneme sahiptir. Doğrulama ve onaylama süreci,
robotik sistemlerin tasarım, prototip, test ve son kullanıcıya sunulmasına kadar birçok
aşamayı kapsar. Bu süreçte sistemlerin belirli kabul kriterleri ve gereksinimleri karşıladığı
doğrulanır. Bu kriterler işlevsellik, güvenlik, performans, dayanıklılık ve maliyet gibi pek
çok alanda belirlenir. Doğrulama ve onaylama süreci, robotik sistemlerin insanlarla birlikte
çalıştığı ortamlarda kullanılacağı durumlarda da hayati önem taşır. İnsanların emniyeti,
öncelikle doğrulama ve onaylama sürecinde belirlenen kriterlerin karşılanması ile sağlanır.
Bu süreç, aynı zamanda robotik sistemlerin yasal ve düzenleyici gereksinimlere uygun
olduğunu da doğrular. Özellikle, endüstriyel robotik sistemlerin kullanımı için, belirli standartlar ve düzenlemeler vardır ve bu standartlara uygunluğun doğrulanması
gerekmektedir.
Bu çalışmada, robotik sistemler için model tabanlı bir belirtim ve doğrulama yöntemi
olan Model Destekli Çalışma Zamanı Doğrulama Aracı (MARVer) önerilmiştir. Önerilen
yaklaşımın amacı, resmi doğrulama tekniklerini, özellikle model kontrolü ve çalışma zamanı
doğrulamasını birleştirerek robotik sistemler için emniyeti, yeniden kullanılabilirliği ve
doğrulama kolaylığını arttırmaktır. Bu tekniklerin kombinasyonu, robotik sistemlerin
emniyeti için daha kararlı ve titiz bir süreç ortaya koyar. Bu nedenle, önerilen yöntem,
karmaşık robotik sistemlerin doğrulanmasıyla ilgili zorlukların üstesinden gelmek için
kapsamlı bir çözüm sunar. Ayrıca MARVer, doğrulama sürecini yönetmek için bir arayüz
sunarak karmaşık terminal işlemlerine olan ihtiyacı ortadan kaldırır. Bu özellik, doğrulama
sürecini kolaylaştırır ve kullanıcıların robotik sistemleri kolayca denetlemesine ve
yönetmesine olanak tanır. Çalışma kapsamında MARVer'in yeteneklerini göstermek için
deneyler yapılmıştır. Deneyde otobüs şasesini gezerek belirli noktalarda fotoğraflar çeken
bir robot emniyet açısından doğrulanmıştır. Robotun hareketi esnasında altı farklı noktadan
alınan alınan uzaklık verileri gözlemlenerek belirlenen emniyet eşik değerinin aşılıp
aşılmadığı doğrulanmıştır. Deneyde hem simülasyon hem de gerçek ortam testleri
yapılmıştır. Çalışmanın sonuçları, önerilen yöntem ve aracın robotik sistemlerin emniyetini
doğrulamada etkili olduğunu ve test eforunu azalttığını göstermiştir.

Abstract:
Robotic systems are widely used in many fields, especially in industrial production,
thanks to their increasing capabilities with sensor and software technologies. While they
completely replace people in some tasks, they can work with people in some tasks.
Therefore, an error that may occur in very complex systems such as robotic systems can
affect not only itself but also its surroundings. This raises serious safety concerns. Thus, it
is critical to utilize verification and validation in the software development of robotic
systems to ensure that they perform expected behaviors. In this study, a Model-Aided
Runtime Verification Tool (MARVer) tool is proposed, which implements a model-based
specification and verification method for robotic systems. The objective of the proposed
approach is to enhance the reliability, reusability, and ease of verification for robotic systems
by merging formal verification techniques, specifically model checking and runtime
verification. The combination of these techniques leads to a more stable and rigorous process
for evaluating the safety of robotic systems. Therefore, the proposed method provides a
comprehensive solution to address the challenges associated with verifying complex robotic
systems. Furthermore, MARVer offers an interface for managing the verification process,
eliminating the need for complex terminal operations. This feature streamlines the
verification process and allows users to easily oversee and manage the evaluation of robotic
systems. Within the scope of the study, experiments are conducted to show the capabilities
of MARVer. A specific test case was conducted to evaluate the system's ability to avoid
obstacles safely while following pre-defined trajectory plans. In the experiment, a robot that
took pictures at certain points by walking around a bus body-in-white was verified for safety.
It was verified whether the determined safety distance threshold value was exceeded by
observing the distance data taken from six different points during the movement of the robot.
In the experiment, both simulation and real environment tests were carried out. The study's
results indicated that the proposed method and tool are effective in verifying the safety of
robotic systems.