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

Abstract

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, usually in 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 veri fication 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 captures the 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 defi ne complex-event processing (CEP) patterns that will later be used as runtime monitors. Existing research on runtime verifi cation (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 profi le, which enables us to customize a modeling tool so that we can develop a domain-specifi c 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.

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 veri fication - RV) alanındaki mevcut çalışmalar genellikle ağır formal yöntemler içeren çözümler önermektedir; bu nedenle, RV endüstride pek 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 pro linde IoT alanına özgü ddeğişiklikler yaparak, alana-özgü modelleme (domain-speci c 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.