Runtime verification of internet of things using complex-event processing (RECEP)

Abstract

Bilgisayar teknolojilerindeki artan işlemci gücü ve bellek kapasitesi, bununla birlikte giderek azalan ölçekli mimari boyutları sayesinde endüstride yeni bir devir başladı, Endüstri 4.0. Bu gelişmeler gömülü sistemlerin kapasitesini artırarak, bunların kullanıldığı otonom sistemlerin her geçen gün daha fazla yaygınlaşmasını sağlamıştır. Nesnelerin _Interneti (Internet of Things - IoT) gömülü sistemlerin insan etkileşimine gereksinim duymadan birbiriyle etkileşebilmesini sağlayarak, endüstride pek çok yeniliğin başarılmasına yol açmıştır. IoT cihazlarından oluşan bir sistemlerin sistemi (SoS) geliştirmek büyük ölçekli sistem tasarımında yeni bir zorluk olarak karşımızaçıkmaktadır (örn., ortam destekli yaşama (ambient assisted living - AAL) uygulamasında onlarca cihaz kullanılırken, akıllı şehir uygulamalarında binlerce cihaz kullanılabilir). Bu yüzden, IoT cihazlarından oluşan SoS'lerin yazılımı geliştirilmesi ve doğrulama süreçlerinde karşılaşılan zorlukların üstesinden gelebilmek için yeni yaklaşımlara ihtiyaç vardır. Biz bu tezde IoT cihazlarından oluşan SoS'lerin koşum zamanı doğrulamasının yapılabilmesi problemini ele aldık. Öncelikle, IoT mesajlaşma öğelerinin temel davranış modelini tanımlayan bir olay kalkülüsü (event calculus - EC) öneriyoruz. EC, bize IoT cihazları arasındaki Constrained-Application Protocol(CoAP) mesajı gönderme ve alma şeklinde gerçekleşen haberleşme aksiyonlarını olaylar türünden tanımlayabilmemizi, dolayısıyla CoAP uç noktaları davranışlarını, daha sonra koşum zamanı gözlemcileri olarak kullanacağımız, karmaşık olay işleme (complex-event processing - CEP) şablonları tanımlamamıza imkan sağlıyor. Koşum zamanı doğrulama (runtime verification - RV) alanındaki mevcut çalışmalar genellikle ağır formal yöntemler içeren çözümler önermektedir; bu nedenle, RV endüstridepek yaygın kullanılmamaktadır. Bu problemi de dikkate alarak biz bu araştırmada, model-güdümlü mühendislik (model-driven engineering - MDE) yaklaşımlarını kullanarak IoT sistemlerinin RV faaliyetleri için formal yöntemlere kıyasla daha kullanılabilir bir çözüm sunduk. Bizim yaklaşımımızda, UML2.5 prolinde IoT alanınaözgü ddeğişiklikler yaparak, alana-özgü modelleme (domain-specic modelling - DSM) prensibine dayalı bir MDE çözümü sunulmuştur. Ayrıca, IoT için önerilen DSM kullanılarak davranış modellerinden CEP ifadeleri biçiminde koşum zamanı gözlemcilerini otomatik olarak üretebilmek için modelden-yazıya dönüşüm (model-to-text - M2T) tekniği ile yeni algoritmalar geliştirilmiştir. Tezde önerilen katkıların gösterimi için MDE ve M2T teknikleri çeşitli durum çalışmalarında kullanılmıştır.

Increase in the computing power and memory accompanied with decreasing architectural footprints has enabled conquering new frontiers in proliferation of technology in the next industry revolution. More autonomous systems have been deployed thanks to the advancing capabilities provided by embedded systems with such computing power. Internet of Things (IoT) has emerged as an enabler of many achievements in the industry through presenting a seamless integration of computing units, usuallyin the form of an embedded system, by allowing interconnection of such embedded systems without requiring human interaction. Engineering a system of systems (SoS) constituted by IoT devices has been the new challenge of designing large scale systems, as the scale of such a system could range from tens of devices in an ambient assisted living (AAL) example to thousands of devices in a smart city application. Therefore, the complexity of software engineering and verification of those SoS's necessitates new approaches that would facilitate those processes. In this thesis, we tackle the problem of verifying IoT SoS's at runtime. We first propose an event calculus that capturesthe fundamental behavioral model of IoT messaging primitives. The event calculus allows us to specify interaction of IoT devices in terms of events that represent sending and receiving Constrained-Application Protocol (CoAP) messages. Representing the behavior of CoAP endpoints in EC helps us define complex-event processing (CEP) patterns that will later be used as runtime monitors. Existing research on runtime verification (RV) usually presents a solution with heavy formal methods, which hinders the usefulness of method by intimidating the practitioners. We, therefore, propose a model-driven engineering (MDE) approach for RV of IoT systems, which is expected to promote the utilization of RV in industrial scenarios. We propose an extension to the UML2.5 profile, which enables us to customize a modeling tool so that we can develop a domain-specific model (DSM) for verifying IoT systems. Later, in order to allow automatically generating runtime monitors in the form of CEP statements, we contribute a model-to-text (M2T) transformation utility in the modeling tool. The contributions of the thesis are demonstrated in several case scenarios.