Modelling OpenComRTOS tasks interaction

Abstract

The model of tasks interaction in Open Communication Real Time Operation System (OpenComRTOS) is developed and discussed in the paper. The main feature of the proposed approach is the using the intermediate hub entity for decoupling interacting tasks. Different temporal semantics (waiting, non waiting and waiting timeout) of tasks synchronization mechanism is introduced. Emerging the effects (i.e. synchronisation or the absence of it) in the case when the tasks actions have different temporal semantics is analysed. The different approaches for expanding the hub model with using TLA and Hoare triplets are proposed.

У статті розроблюється й обговорюється модель взаємодії задач в операційній системі реального часу OpenComRTOS. Головна особливість запропонованого підходу – використання сутності синхронізації Hub як проміжної ланки в механізмі взаємодії задач. Проаналізована різна часова семантика процесу синхронізації задач (очікування, неочікування, очікування протягом періоду часу). Розглянуто виникнення ефекту синхронізації у випадку, коли дії задач мають різну часову семантику. Запропоновані різні підходи для розширення моделі Hub з використанням TLA (Temporal Logic of Actions) і трійок Hoare (Hoare triplets).

В статье разрабатывается и обсуждается модель взаимодействия задач в операционной системе реального времени OpenComRTOS. Главная особенность предложенного подхода – использование сущности синхронизации Hub как промежуточного звена в механизме взаимодействия задач. Проанализирована различная временная семантика процесса синхронизации задач (ожидание, неожидание, ожидание в течение периода времени). Рассмотрено возникновение эффекта синхронизации в случае, когда действия задач имеют различную временную семантику. Предложены различные подходы для расширения модели Hub с использованием TLA (Temporal Logic of Actions) и троек Hoare (Hoare triplets).