Использование метамодели для построения моделей взаимодействий задач в операционной системе реального времени

Использование метамодели для построения моделей взаимодействий задач в операционной системе реального времени

В статье строятся и исследуются свойства моделей взаимодействий задач в операционной системе реального времени OpenComRTOS. Главная особенность предложенного подхода состоит в использовании метамодели для построения моделей взаимодействий, обладающих заданными свойствами. В частности, рассмотрено во...

Повний опис

Збережено в:
Бібліографічні деталі
Дата:2010
Автор: Межуев, В.И.
Формат: Стаття
Мова:Russian
Опубліковано: Інститут кібернетики ім. В.М. Глушкова НАН України 2010
Назва видання:Математичне та комп'ютерне моделювання. Серія: Фізико-математичні науки
Онлайн доступ:http://dspace.nbuv.gov.ua/handle/123456789/18775
Теги: Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
Назва журналу:Digital Library of Periodicals of National Academy of Sciences of Ukraine
Цитувати:Использование метамодели для построения моделей взаимодействий задач в операционной системе реального времени / В.И. Межуев // Математичне та комп'ютерне моделювання. Серія: Технічні науки: зб. наук. пр. — Кам’янець-Подільський: Кам'янець-Подільськ. нац. ун-т, 2010. — Вип. 3. — С. 125-137. — Бібліогр.: 9 назв. — рос.

Репозитарії

Digital Library of Periodicals of National Academy of Sciences of Ukraine
id irk-123456789-18775
record_format dspace
spelling irk-123456789-187752013-02-13T03:19:31Z Использование метамодели для построения моделей взаимодействий задач в операционной системе реального времени Межуев, В.И. В статье строятся и исследуются свойства моделей взаимодействий задач в операционной системе реального времени OpenComRTOS. Главная особенность предложенного подхода состоит в использовании метамодели для построения моделей взаимодействий, обладающих заданными свойствами. В частности, рассмотрено возникновение эффекта синхронизации в случае, когда действия задач имеют различную временную семантику. The models of tasks interactions in the OpenComRTOS real time operation system are developed and investigated in the paper. The main feature of the proposed approach is the use of a metamodel for development of models of the interactions, which having the needed properties. In particular, occurrence of a synchronization effect in the case when actions of tasks have different time semantics is considered. 2010 Article Использование метамодели для построения моделей взаимодействий задач в операционной системе реального времени / В.И. Межуев // Математичне та комп'ютерне моделювання. Серія: Технічні науки: зб. наук. пр. — Кам’янець-Подільський: Кам'янець-Подільськ. нац. ун-т, 2010. — Вип. 3. — С. 125-137. — Бібліогр.: 9 назв. — рос. XXXX-0060 http://dspace.nbuv.gov.ua/handle/123456789/18775 004.451.24,004.451.62 ru Математичне та комп'ютерне моделювання. Серія: Фізико-математичні науки Інститут кібернетики ім. В.М. Глушкова НАН України
institution Digital Library of Periodicals of National Academy of Sciences of Ukraine
collection DSpace DC
language Russian
description В статье строятся и исследуются свойства моделей взаимодействий задач в операционной системе реального времени OpenComRTOS. Главная особенность предложенного подхода состоит в использовании метамодели для построения моделей взаимодействий, обладающих заданными свойствами. В частности, рассмотрено возникновение эффекта синхронизации в случае, когда действия задач имеют различную временную семантику.
format Article
author Межуев, В.И.
spellingShingle Межуев, В.И.
Использование метамодели для построения моделей взаимодействий задач в операционной системе реального времени
Математичне та комп'ютерне моделювання. Серія: Фізико-математичні науки
author_facet Межуев, В.И.
author_sort Межуев, В.И.
title Использование метамодели для построения моделей взаимодействий задач в операционной системе реального времени
title_short Использование метамодели для построения моделей взаимодействий задач в операционной системе реального времени
title_full Использование метамодели для построения моделей взаимодействий задач в операционной системе реального времени
title_fullStr Использование метамодели для построения моделей взаимодействий задач в операционной системе реального времени
title_full_unstemmed Использование метамодели для построения моделей взаимодействий задач в операционной системе реального времени
title_sort использование метамодели для построения моделей взаимодействий задач в операционной системе реального времени
publisher Інститут кібернетики ім. В.М. Глушкова НАН України
publishDate 2010
url http://dspace.nbuv.gov.ua/handle/123456789/18775
citation_txt Использование метамодели для построения моделей взаимодействий задач в операционной системе реального времени / В.И. Межуев // Математичне та комп'ютерне моделювання. Серія: Технічні науки: зб. наук. пр. — Кам’янець-Подільський: Кам'янець-Подільськ. нац. ун-т, 2010. — Вип. 3. — С. 125-137. — Бібліогр.: 9 назв. — рос.
series Математичне та комп'ютерне моделювання. Серія: Фізико-математичні науки
work_keys_str_mv AT mežuevvi ispolʹzovaniemetamodelidlâpostroeniâmodelejvzaimodejstvijzadačvoperacionnojsistemerealʹnogovremeni
first_indexed 2025-07-02T19:44:30Z
last_indexed 2025-07-02T19:44:30Z
_version_ 1836565629380853760
fulltext Серія: Технічні науки. Випуск 3 125 УДК 004.451.24,004.451.62 В. И. Межуев, канд. пед. наук Бердянский государственный педагогический университет, г. Бердянск ИСПОЛЬЗОВАНИЕ МЕТАМОДЕЛИ ДЛЯ ПОСТРОЕНИЯ МОДЕЛЕЙ ВЗАИМОДЕЙСТВИЙ ЗАДАЧ В ОПЕРАЦИОННОЙ СИСТЕМЕ РЕАЛЬНОГО ВРЕМЕНИ В статье строятся и исследуются свойства моделей взаи- модействий задач в операционной системе реального времени OpenComRTOS. Главная особенность предложенного подхода состоит в использовании метамодели для построения моделей взаимодействий, обладающих заданными свойствами. В част- ности, рассмотрено возникновение эффекта синхронизации в случае, когда действия задач имеют различную временную семантику. Ключевые слова: модель, метамодель, взаимодействие задач, операционная система реального времени. Введение. OpenComRTOS (Open Communication Real Time Opera- tion System) является операционной системой реального масштаба вре- мени, предназначенной для использования во встроенных (embedded) системах [1, 2]. Основными понятиями OpenComRTOS являются зада- ча (task) и характерные для параллельного программирования объек- ты синхронизации — порт (port), событие (event), семафор (sema- phore), ресурс (resource), FIFO и др. Данные объекты синхронизации обобщаются в OpenComRTOS в едином понятии концентратора (hub). В статье [3] нами была рассмотрена возможность порождения моделей распределенных параллельных приложений реального вре- мени при помощи метамодели, построенной на основании теории графов. Узлами графа в этом случае являются задачи и объекты син- хронизации OpenComRTOS, а ребрами — взаимодействия между ними. Такой подход позволяет использовать методы теории графов для решения задач рассматриваемой предметной области (ПрО), в частности, для генерации кода моделируемой программной системы. Целью данной работы является расширение семантики моделей программных систем, порождаемых из основанной на теории графов метамодели. Для этого конкретизируется структура, а также вводятся дополнительные свойства узлов и ребер графа модели программного приложения. Такой подход позволяет породить семантики взаимо- действий задач в распределенной параллельной системе, обладающие требуемыми свойствами. © В. И. Межуев, 2010 Математичне та комп’ютерне моделювання 126 В частности, выделим следующие необходимые свойства семан- тик взаимодействия задач:  безопасность взаимодействия задач (гарантированное осуществ- ление синхронизации);  защита внутреннего состояния задач при их взаимодействии;  возможность асинхронной работы в системе, обладающей огра- ниченными ресурсами;  поддержка различной временной семантики взаимодействий;  возможность построения объектов синхронизации, специфич- ных для предметной области;  композиция более сложных программных систем из базовых элементов (задач и объектов синхронизации);  возможность формальной проверки моделей программных систем. Данная статья посвящена построению моделей взаимодействий задач в распределенной параллельной системе, обладающих задан- ными свойствами. 1. Основные идеи и структура работы Рассмотрим ключевые принципы, которые позволяют построить модели взаимодействий задач, обладающие перечисленными выше свойствами. Прежде всего, это наложение ограничений на субъекты и объекты взаимодействий. Задачи OpenComRTOS являются активными объектами, которые могут взаимодействовать только через пассивные объекты синхронизации посредством пересылки особых структур дан- ных — пакетов (packet). Преимущество данного подхода состоит в том, что объекты синхронизации разделяют взаимодействующие задачи. Под разделением мы понимаем семантику поведения, в которой задача не знает о другой задаче, с которой она взаимодействует. В процессе взаимодействия в пакете передается копия значений переменных зада- чи, что является способом защиты внутреннего состояния задачи. Такой подход позволяет определить задачу OpenComRTOS как компонент. Выполняя композицию компонентов, осуществляющих взаимодействие через объекты синхронизации, можно создавать сложные параллельные системы. Для использования компонента дос- таточно знать лишь его интерфейсы; доступ к его внутреннему со- стоянию не является необходимым. Этот способ построения параллельных систем был впервые формализован в алгебре взаимодействующих последовательных про- цессов Хоара — CSP (Communicating Sequential Processes) [4]. В CSP параллельная система состоит из процессов и каналов. Процесс вы- полняется при помощи (возможно бесконечного числа) последова- тельных шагов. Последовательность индивидуальных шагов (назы- Серія: Технічні науки. Випуск 3 127 ваемых также следами) процессов разделяется коммуникацией через каналы. В случае, когда процессы синхронизированы на канале, через него могут быть переданы данные, что является простейшей формой взаимодействия. CSP подход является очень мощным и обеспечивает механизм для формального построения и проверки больших парал- лельных программных систем. Однако механизм синхронизации процессов через CSP канал весьма ограничен в своей семантике. На- пример, CSP каналы не учитывают параметры времени, хотя позже это было исправлено в так называемом Timed CSP [5]. Концентратор (hub) OpenComRTOS обобщает функциональные возможности канала CSP. Так же, как и в CSP, основной функцио- нальной возможностью экземпляров hub (т.е. port, event, semaphore, FIFO и др.) является осуществление синхронизации задач. Однако hub осуществляет взаимодействие задач, основываясь на результате проверки условия синхронизации, что позволяет реализовать намного более сложную семантику взаимодействий. Hub также может быть промежуточным звеном для взаимодей- ствия большего, чем два, числа задач, тогда как канал CSP предна- значен для синхронизации только двух процессов. Однако заметим, что поведение, аналогичное hub, может быть достигнуто в CSP путем введения специального промежуточного процесса между задачами. Таким образом, объекты синхронизации OpenComRTOS — со- бытие (event), семафор (semaphore), ресурс (resource), FIFO и т.д., определяют надмножество семантики CSP. Важное преимущество предложенного подхода состоит в том, что объекты синхронизации OpenComRTOS могут быть специализированными, т.е. определяе- мыми пользователем. Это позволяет порождать семантики взаимо- действий задач, обладающие заданными свойствами. В частности, отметим возможность реализации семантик ожида- ния, не ожидания, ожидания период времени, а также полностью асинхронных взаимодействий задач. Такой подход позволяет при- кладному программисту выражать свойства ПрО способом, который наиболее соответствует ее (требуемому) поведению. Специфичные для ПрО объекты синхронизации могут быть порождены из hub пу- тем указания условия синхронизации и действия, которое происходит в случае его истинности. В этом и состоит основное отличие нашего от традиционных подходов, которые требует полной перестройки ядра операционной системы для поддержки специфики ПрО. Т.о. hub состоит из логического суждения (условия синхрониза- ции) и действия синхронизации. Действие синхронизации осуществля- ется в случае истинности условия синхронизации. Проверка условия перед выполнением действия делает также возможным формальное Математичне та комп’ютерне моделювання 128 моделирование и проверку параллельных программных систем. Инте- рес представляет также декомпозиция условия синхронизации на пре- и постусловия. В этом случаем мы проводим аналогию между объек- тами синхронизации OpenComRTOS и тройками Хоара {P}C{Q} [6]. Раздел 2 данной статьи посвящен расширению подхода CSP пу- тем введения модели взаимодействия задач через промежуточные объекты синхронизации. Раздел 3 исследует возможные временные семантики предложенной модели взаимодействия задач. Раздел 4 посвящен расширению семантики взаимодействий задач путем ана- лиза связи модели со спецификациями языка TLA (Temporal Logic of Actions) [7] и тройками Хоара [6]. Завершают статью выводы и спи- сок использованных источников. 2. Моделирование семантики взаимодействия задач Декомпозиция любой ПрО на объекты и их взаимодействия яв- ляется естественным путем человеческого познания. Соответственно, все существующие методики моделирования ПрО подчеркивают ис- пользование объектов и их отношений. Естественным математиче- ским средством для построения моделей подобного рода ПрО являет- ся теория графов. Разрабатываемый нами подход находится в рамках идей пред- метно-ориентированного моделирования — DSM (Domain Specific Modelling). В этом контексте теория графов является основанием для метамодели, определяющей грамматику для построения моделей ПрО. Иными словами, теория графов предоставляет совокупность понятий (модельных объектов) и правил их объединения для по- строения моделей ПрО, обладающих требуемыми свойствами. Как мы уже отмечали выше, задачи и взаимодействия Open- ComRTOS типизируются нами соответственно как узлы и ребра гра- фа. Построение обладающих требуемыми свойствами моделей требу- ет более детального рассмотрения понятия взаимодействия задач. Под взаимодействием мы понимаем, что задачи осуществляют действия взаимным способом, что часто считается побочным эффек- том их коммуникации. Однако заметим, что взаимность действий не означает, что задачи выполняют их в сотрудничестве к достижению некоторой предопределенной цели. Взаимодействие имеет место, когда два или более объектов дей- ствуют друг на друга. Таким образом, основная идея взаимодействия состоит в двухстороннем эффекте, в противоположность односто- роннему причинному эффекту. Рис. 1 отражает такую схему взаимо- действия двух задач (именованных здесь Задача1 и Задача2). Серія: Технічні науки. Випуск 3 129 Из этой простой графической модели следует, что взаимодействие задач должно включать по крайней мере два взаимно противополож- ных действия, именованных здесь Действие1 и Действие2. Для гарантирования безопасности и реализации других требуе- мых принципов семантики взаимодействий задач мы помещаем между задачами объект синхронизации (обобщением которого является hub). Рис. 2. Взаимодействие через промежуточный объект синхронизации В этой модели взаимодействие между задачами состоит из двух симметричных действий между каждой задачей и объектом синхро- низации. Эти действия будем называть посылкой (put) и получением (get), что является отражением имен сервисов, используемых в реали- зации для обработки пакетов. Таким образом, процесс взаимодействия задач декомпозируется нами в пару Put (в дальнейшем для краткости будем использовать P) и Get (в дальнейшем будем использовать G) действий, приводящих к эффекту S, то есть синхронизации между задачами. Сущность следующего утверждения состоит в том, что взаимные P и G действия двух задач есть необходимое условие их синхронизации (мы не говорим здесь ничего относительно временных свойств действий, порядка их следования и условий, определяющих каждое действие):     ,P G G P S    (1) где логическое «И» символизирует, что для синхронизации S долж- ны иметь место оба действия. Мы используем здесь понятие действия в толковании, аналогич- но данному Лесли Лампортом для TLA [7, с. 16]: «действие — обыч- ная математическая формула …, действие является истинным или ложным на шаге». Уравнение (1) можно также рассмотреть как следствие одного из принципов дизайна OpenComRTOS — симметрии механизма син- Взаимодействие Задача1 Задача2 Действие1 Действие2 Рис. 1. Схема взаимодействия задач Задача1 Объект синх- ронизации Задача2 Математичне та комп’ютерне моделювання 130 хронизации, для реализации которого между взаимодействующими задачами помещается объект синхронизации. Заметим, что задачи в параллельной системе имеют равные пра- ва для взаимодействия. Таким образом, по умолчанию, нет никакой главной задачи, которая служит причиной действий других задач. Задача, посылая пакет в объект синхронизации, не знает ничего о другой задаче, также взаимодействующей с данным объектом син- хронизации. Иными словами, между взаимодействующими задачами не существует причинно-следственной связи. Уравнение (1) определяет свойство, что только взаимные дейст- вия двух задач приводят к их синхронизации, и именно поэтому мы классифицируем этот процесс как взаимодействие. Важный случай имеет место, когда осуществляется только одно действие — Put или Get. Если внешний наблюдатель обнаруживает толь- ко одно действие, то процесс синхронизации начинается, но не заканчи- вается. При использовании ждущего сервиса, задача, начавшая действие, перестает выполняться (или же, другими словами, блокируется). Уравнения (2) и (3) отражают сценарий, когда задача1 выполни- ла ждущее действие 1P , но задача2 еще не осуществила действие 2G . Это приводит к тому, что задача1 блокируется. Точно так же задача2 блокируется после выполнения ждущего действия 2G , когда задача1 еще не осуществила 1P . 1 2 1 ,P G Task blocked  (2) 1 2 2 .P G Task blocked  (3) Заметим, что уравнения (2) и (3) также отражают семантику взаимодействия процессов на ждущем (блокирующем) CSP канале. Блокированная задача снова становится активной, если проис- ходит соответствующее действие. Соответствующее означает, что тип действий задач должен быть противоположным: если первое дей- ствие имеет Put тип, то второе действие должно иметь Get тип. Син- хронизация есть единственный способ продолжить выполнение бло- кированных задач. 3. Временные свойства взаимодействий задач Уравнение (1) означает, что только взаимные действия (взаимо- действие) задач приводят к синхронизации. В этом разделе мы обсу- ждаем значение понятия взаимодействие в контексте времени. OpenComRTOS позволяет осуществить следующие временные семантики действий задач: ожидание (W), не ожидание (NW) и ожи- дание период времени (WT). Рассмотрим условия возникновения эф- Серія: Технічні науки. Випуск 3 131 фекта синхронизации в случае, когда действия задач имеют различ- ную временную семантику. Вообще говоря, временная семантика взаимодействий задач за- висит от типа объекта синхронизации и граничных условий (напри- мер, граничного размера списка элементов FIFO). В этом разделе ста- тьи будем использовать понятие синхронизации в CSP смысле, то есть как синхронную передачу данных по каналу связи между двумя задачами. Самым близким к функциональности канала CSP в OpenComRTOS является порт (port). Исходя из трех вариантов действий задач, OpenComRTOS имеет 9 возможных случаев временной семантики взаимодействий двух задач. Таблица 1 Варианты временной семантики взаимодействий задач в OpenComRTOS Временная семан- тика W (ожидание) WT (ожидание период времени) NW (не ожидание) W (ожидание) Симметрия <W, WT> <W, NW> WT (ожидание период времени) <WT, W> симметрия <WT, NW> NW (не ожидание) <NW, W> <NW, WT> симметрия В случае, когда взаимодействия принадлежат к первому квад- ранту Таблицы 1 (т.е. оба действия используют ждущую семантику W), синхронизация не зависит от времени. Случаи симметрии, представленные как диагональ Таблицы 1, имеют место, когда обе задачи используют один и тот же тип серви- сов (то есть NW и NW, WT и WT, W и W). Свойство такой симмет- рии взаимодействий во времени состоит в том, что синхронизация задач не зависит от относительного порядка их действий. В случае возникновения 1) <W, WT>, 2) <W, NW>, 3) <WT, NW> последовательностей синхронизация зависит от порядка дейст- вий задач. Для выражения временной семантики механизма синхро- низации задач в таком случае должны использоваться операторы темпоральной логики (например, [7]). 1) Если W-действие произошло ранее WT-действия, синхрониза- ция происходит в любом случае. Если сначала произошло WT-действие, то для синхронизации W- действие должно быть осуществлено во временном интервале T. 2) Если W-действие произошло прежде NW-действия, синхрониза- ция происходит в любом случае. Математичне та комп’ютерне моделювання 132 Если NW-действие произошло до осуществления W-действия, синхронизация не произойдет. 3) Если WT-действие произошло до NW-действия, то для синхро- низации NW-действие должно быть осуществлено во временном интервале T. Если NW-действие произошло до осуществления WT-действия, синхронизация не произойдет. Заметим, что в формулировке всех этих утверждений, мы игно- рируем способность объекта синхронизации к буферизации. Такие элементарные последовательности действий посредством композиции могут быть применены для построения и анализа времен- ных семантик сложных взаимодействий. Для этого элементарные после- довательности взаимодействий должны быть сформулированы как вре- менные формулы в синтаксисе TLA. Следующее состояние программ- ной системы будет зависеть от результата предыдущих взаимодействий (приводящий к синхронизации или же блокирующий приложение). Формализуем и рассмотрим свойства симметричных случаев синхронизации задач в OpenComRTOS. NW-взаимодействие задач имеет следующую семантику:    1 1 22 .t t t t P G t t S      (4) Уравнение (4) определяет, что, в случае использования NW- сервисов, синхронизация S имеет место, если обе задачи осуществля- ют соответствующие действия P и G в один и тот же момент времени. Поэтому, строго говоря, при возникновении <NW, NW> после- довательности действий задач их синхронизация не является возмож- ной, что является следствием их последовательного выполнения на машине архитектуры Фон Неймана. Иными словами, вычислительное устройство, на котором расположен объект синхронизации, преобра- зовывает доступ к нему в строго последовательную форму. Именно поэтому обработка двух NW-пакетов в одном и том же объекте син- хронизации в один и тот же момент времени является невозможной, что и приводит к невозможности NW-синхронизации в hub. Уравнение (4) может быть истинным только тогда, когда одно из действий (типа Put или Get) было буферизировано в списке ожидания hub. Например, используя NW-сервис можно получить пакет из FIFO, если он уже был помещен в него при помощи NW-сервиса ранее. (Заметим, что задача также может получить из FIFO собственный пакет, который был помещен ею в FIFO прежде.) Таким образом, NW-семантика синхронизации задач возможна в случае осуществле- ния hub буферизации пакетов. Это является следствием того факта, что синхронизация задач является вторичным эффектом от успешно- Серія: Технічні науки. Випуск 3 133 го завершения действий между hub и задачами, однако не непосред- ственно между задачами. Вообще говоря, единственная безопасная семантика осуществ- ления взаимодействий задач является блокирующей (ждущей) семан- тикой. Именно поэтому использование семантики ожидания — обычный путь для осуществления синхронизации задач, как это и практикуется в CSP. Использование NW-сервисов можно рассмот- реть как способ проверки, является ли в данный момент синхрониза- ция возможной (или же способом синхронизации, когда hub имеет поддержку буферизации). WT синхронизация задач имеет следующую семантику:    1 2 12 ,t t t t P G t t T S       (5) где T является интервалом времени. Уравнение (5) определяет, что в случае использования WT- сервисов, синхронизация задач имеет место, когда промежуток вре- мени между действиями P и G менее, чем интервал .T Заметим, что формула (5) переходит в (4) в случае 0.T  В слу- чае T   мы переходим к ждущей (W) семантике. Приводящие к синхронизации S , W -действия задач имеют сле- дующую семантику:    1 2 12t t t t P G t t S        (6). Т.о. в случае использования W сервисов, промежуток времени, в течение которого может быть осуществлена синхронизация задач, является бесконечным. Уравнение (6) сводится к уравнению (1), то есть синхронизация происходит в случае взаимных действий задач вне зависимости от времени. Заметим, что этот тип аналогичен син- хронизации на канале CSP. Асинхронная семантика взаимодействий в OpenComRTOS также возможна, хотя такие взаимодействия в действительности являются отложенными синхронными взаимодействиями. Семантика асин- хронных во времени действий задач может быть определена как «вы- стрелил и забыл». Заметим, что асинхронные взаимодействия требу- ют неограниченного числа ресурсов, однако ресурсы реальной сис- темы всегда ограничены. Это налагает серьезные ограничения на возможность применений асинхронных взаимодействий. Функциональные возможности hub обеспечивают иной способ осуществления асинхронного поведения задач. Например, для FIFO семантика ожидания будет иметь место, только если FIFO полон (достигнут предел буфера FIFO — Size), и мы имеем задачу посылки Математичне та комп’ютерне моделювання 134 (Put); или же если FIFO пуст (счетчик буфера FIFO равен нулю), и мы имеем задачу получения (Get).      0P Count FIFO Size G Count FIFO Wait      (7). Следовательно, нормальное поведение осуществляющих буфери- зацию сервисов всегда является асинхронным, и сводится к синхрон- ному только тогда, когда буфер полон или пуст. Осуществление такой семантики поведения задач в реальной системе является предпочти- тельным, так как она осуществляется при ограниченных ресурсах. Таким образом, для FIFO для всех временных семантик дейст- вий (W, NW, WT) синхронизация имеет место независимо от време- ни, если формула (7) ложна. Подобные свойства могут быть сформулированы для функцио- нальных возможностей таких сущностей синхронизации как событие (event) и семафор (semaphore), которые также осуществляют асин- хронное поведение. Заметим, что в случае синхронизации задачи на событии или на семафоре важен порядок осуществления действий. Синхронизация на событии имеет место, если первым во времени действием являет- ся Put (применительно к событию, сервис именуется RaiseEvent), с последующим Get (TestEvent), с условием, что изначально событие не было взведено. Обе задачи могут продолжить выполнение немедлен- но после осуществления их синхронизации через событие, независи- мо от временной семантики действий. Описывая семантику механизма синхронизации задач, мы неяв- но используем предположение, что она может иметь место только на том же самом объекте синхронизации:    .Hub P Hub G (8) Уравнение (8) отражает пространственную семантику меха- низма синхронизации задач в распределенной параллельной системе. 4. Модель объекта синхронизации Как было отмечено нами выше, пользователь может определить собственный объект синхронизации в рамках его модели, получив- шей название концентратора (hub). В отвлечении от технических деталей, hub включает предикат синхронизации и действие синхронизации. . def Hub Predicate Action  (9) Исходя из определения (9) модель параллельной программы в OpenComRTOS может быть определена как машина состояний, выпол- няющая действия только тогда, когда условия синхронизации задач яв- Серія: Технічні науки. Випуск 3 135 ляются истинными. Необходимыми слагаемыми условий синхронизации есть временные свойства, рассмотренные нами в разделе 3 статьи. Язык TLA [7] является основой формальной спецификации OpenComRTOS [1; 2]. Заметим, что определение (9) соответствует формулировке спецификации системы в TLA, которая также включа- ет условия и действия [7]. 0 0 0 1 1 1j j j A Guard Action A Guard Action        (10) Следующее состояние системы определяется как результат ло- гической операции «или» между всеми возможными защищенными действиями задач. 0 1 1... .jNext A A A     (11) Таким образом, мы можем определить протокол взаимодействия задач OpenComRTOS как последовательность защищенных действий, имеющих место во всех hub системы. Данный подход описывает по- ведение программной системы в терминах изменения ее внутреннего состояния. Состояние программной системы мы рассматриваем как объединение множеств состояний задач и объектов синхронизации. Последовательность действий 1 2, ,..., nA A A  задач, вызывает об- новление состояний 1 2, ,..., mH H H  объектов синхронизации. Отвечающая (1) пара действий приводит к синхронизации задач и, таким образом, взаимодействие является механизмом, который вы- зывает переход состояний вовлеченных задач. Только синхронизация позволяет задачам выполняться далее, поэтому последовательность взаимодействий 1 2, ,..., kI I I  задач приводит к обновлению со- стояний 1 2, ,..., lP P P  программы. Заметим, что первой логической системой, разработанной для проверки компьютерных программ, была логика Флойда и Хоара [6; 8]. Идея логики Хоара состоит в помещении предикатов в начало и конец блока программы. Аксиомы логики Хоара определяют входные преди- каты как достаточные условия, гарантирующие, что успешное выпол- нение блока программы приводит к указанным выходным условиям. Такие предикаты входа/выхода описывают поведение программы в альтернативной форме. Отношения между предикатами устанавли- ваются аксиомами языка программирования. Такая аксиоматическая проверка является методом доказательства правильности программы. Математичне та комп’ютерне моделювання 136 Например, предикаты для данных помещаются в различные точки про- граммы и остаются инвариантами в процессе ее выполнения. В этом подходе аксиоматическая семантика языка программиро- вания определяется тройками Хоара (12). Операторы программы пре- образуются в предикаты, а валидность графа программы сводится к валидности лемм, не содержащих операторы программы. Поэтому следующим шагом в разработке модели hub является его рассмотрение в терминах троек Хоара [6]. Эти тройки выражают- ся следующим отношением:    P C Q , (12) где P является предусловием, Q — постусловием и C — командой языка программирования. Это требует расширения модели hub путем декомпозиции пре- диката синхронизации в пред- и пост-условия. Предусловие синхро- низации в hub разрешает действие, приводя к постусловию. P recondition Action Postcondition  (13) В качестве примера рассмотрим синхронизацию задач посредст- вом семафора. Предусловия:  существует, по крайней мере, одна задача, ожидающая сигнала семафора;  семафор установлен (т.е. его счетчик более единицы). Действие (синхронизация):  состояние ждущей задачи сделать активным;  декрементировать счетчик семафора. Постусловия:  задача активна (выполняется снова);  счетчик семафора уменьшен на единицу и его значение больше нуля. Выводы. В работе предложены способы расширения семантики моделей программных систем, порождаемых из основанной на тео- рии графов метамодели. Выделены необходимые свойства семантик взаимодействия задач в распределенной параллельной системе и предложен подход для построения моделей, которые обладают за- данными свойствами. Основным средством для этого является введе- ние модели объекта синхронизации (hub). Пользователь может опре- делить собственный объект синхронизации путем указания условия синхронизации и действия, которое происходит в случае его истин- ности. Такой подход позволяет прикладному программисту выражать свойства ПрО способом, который наиболее соответствует ее (требуе- Серія: Технічні науки. Випуск 3 137 мому) поведению. Построение hub на формальной основе связывает программирование с математическими методами и является шагом к проектированию формально доказанных программ. Список использованной литературы: 1. Verhulst E. An Industrial Case: Pitfalls and Benefits of Applying Formal Methods to the Development of a Network-Centric RTOS / E. Verhulst, G. Jong, V. Mezhuyev // Lecture Notes in Computer Science. FM 2008 : For- mal Methods. — Heidelberg : Springer Berlin, 2008. — P. 411—418. 2. Verhulst E. OpenComRTOS : A Runtime Environment for Interacting Entities / E. Verhulst, V. Mezhuyev, Bernhard H. C. Sputh [et al.]; P. Welch, H. Roebbers, T. Announced (eds.) // Communicating Process Architectures 2009. — IOS Press, 2009. — P. 173 — 184. 3. Межуев В. И. Предметно-ориентированное моделирование распределен- ных параллельных приложений реального времени / В. И. Межуев // Сис- теми обробки інформації. — 2010. — Вип. 5 (86). — С. 98—103. 4. Hoare C. A. R. Communicating Sequential Processes. Published by Prentice Hall / C. A. R. Hoare // International Series in Computer Science. — 1985. — 276 p. 5. Timed CSP : A Retrospective / J. Ouaknine, S. Schneider // Electronic Notes in Theoretical Computer Science. — 2006. — 162 (1). — P. 273—276. 6. Hoare C. A. R. An Axiomatic Basis for Computer Programming / C. A. R. Hoare // Communications of the ACM. — Vol. 12, N 10. — Р. 576—583. 7. Lamport L. Specifying systems : the TLA+ language and tools for hardware and software engineers / L. Lamport // Addison-Wesley, Boston. — 2002. — 364 p. 8. Floyd R. W. Assigning meanings to programs / R. W. Floyd, J. T. Schwartz (еd.) // Proc. of Symposium on Applied Mathematics. — 1967. — Vol. 19. — Р. 19—32. 9. Rosenband D. Modular Scheduling of Guarded Atomic Actions / D. Rosen- band // Proc. of the 41st Design Automation Conference (DAC'04) (San Diego, June 7—11, 2004). — San Diego, California, USA, 2004. — P. 8. The models of tasks interactions in the OpenComRTOS real time op- eration system are developed and investigated in the paper. The main fea- ture of the proposed approach is the use of a metamodel for development of models of the interactions, which having the needed properties. In par- ticular, occurrence of a synchronization effect in the case when actions of tasks have different time semantics is considered. Key words: model, metamodel, tasks interaction, real time operation system. Отримано 22.05.10

Схожі ресурси