Today, the significant volumes of network traffic circulate through the Internet. The sources of such traffic are, in particular, the diverse territory distributed “smart” devices. The number of named devices is about billions. As a consequence, the relevance of bringing to practice the core concepts of the Internet of Things paradigm is constantly becoming more and more topical. It’s bound with the problem of granting the interoperability between the components of distributed software systems, built over the aforementioned devices. The web services are typically considered as the components of the system. To this end, to establish the interoperability between the components, despite the standardization, the need for the development of effective tools and techniques, granting the interoperability between the web services, arises. The goal of the work is to increase the effectiveness of the Internet of Things system engineering process by way of checking the interoperability between the components during the designing. The goal is achieved through the development of formal model for checking the interoperability between the components of the Internet of Things system by way of model checking in an automated manner. The novelty of proposed solution is grounded on the usage of Temporal Logic of Actions, corresponding formalism and the concept of action as the basis for compact and easily reconfigurable formal specifications synthesis. The adequacy of proposed model has been proved through the case study. The verification-related time costs have been estimated.

În prezent, Internetul generează sume importante de trafic, ale căror surse sunt adesea diferite tipuri de dispozitive "inteligente". Numărul de astfel de dispozitive se cifrează la miliarde. Ca urmare, implementarea paradigmei Internet of Things (IoT) devine din ce în ce mai importantă. Aceasta implică asigurarea compatibilității între componentele sistemelor software distribuite, construite pe dispozitivele care interacționează. În acest sens, rolul componentelor sistemului este adesea serviciile web. În acest sens, pentru a asigura compatibilitatea între componente, pe lângă standardizare, este necesară dezvoltarea unor instrumente și mecanisme eficiente pentru a asigura și verifica coerența interacțiunii dintre serviciile web. Scopul lucrării este creșterea eficienței procesului de dezvoltare a internetului obiectelor. Acest obiectiv este realizat prin dezvoltarea unui model formal de verificare a compatibilității componentelor sistemului Internet of Things, care este destinat să servească drept bază pentru efectuarea unei verificări automate utilizând metoda de verificare a modelului la etapa de proiectare a sistemului. Cel mai important rezultat al lucrării este acela că a fost propus un model formal al specificației sistemului IoT, care se bazează pe logica temporală a acțiunilor (Temporal Logic Actions) și pe formalismul corespunzător. Noutatea științifică a lucrării constă în utilizarea conceptului de "acțiune" al logicii temporale menționate mai sus, care a făcut posibilă obținerea unor specificații formale compacte reconfigurabile care reflectă specificul sistemului în cauză - modificarea cerințelor privind caracteristicile sistemului în funcție de schimbările condițiilor externe. Adecvarea modelului propus este confirmată de exemplul unui scenariu de domeniu. Se măsoară costurile de timp asociate verificării automate a specificațiilor, sintetizate conform modelului propus.

В настоящее время в сети Интернет генерируются значительные объемы трафика, источниками которого, зачастую, являются различного рода «умные» устройства. Количество подобных устройств исчисляется миллиардами. В результате этого все большую актуальность приобретает реализации парадигмы Интернета вещей. Это сопряжено с обеспечением совместимости между компонентами распределенных программных систем, построенных поверх взаимодействующих устройств. В роли компонентов системы при этом, зачастую, выступают веб-сервисы. В связи с этим, для обеспечения совместимости между компонентами, помимо стандартизации, возникает потребность разработки эффективных средств и механизмов обеспечения и проверки согласованности взаимодействия между веб-сервисами. Цель работы – повышение эффективности процесса разработки системы Интернета вещей. Поставленная цель достигается за счет разработки формальной модели проверки совместимости компонентов системы Интернета вещей, предназначенной служить базисом для проведения автоматизированной верификации методом проверки на модели на этапе проектирования системы. Наиболее существенный результат работы состоит в том, что была предложена формальная модель спецификации системы Интернета вещей, которая основывается на темпоральной логике действий (Temporal Logic of Actions) и соответствующем формализме. Научная новизна работы состоит в использовании концепции «действия» названной темпоральной логики, что позволило получать компактные реконфигурируемые формальные спецификации, отражающие специфику рассматриваемой системы – изменение требований к характеристикам системы в зависимости от изменения внешних условий. Адекватность предложенной модели подтверждена на примере сценария предметной области. Измерены временные затраты, сопутствующие автоматизированной верификации спецификации, синтезированной согласно предложенной модели. Эти затраты охарактеризованы как приемлемые – с учетом вычислительной сложности решаемой задачи и относительно низких вычислительных возможностей использованной аппаратной платформы. Отмечено, что названные затраты в дальнейшем могут быть снижены