RUS  ENG ЖУРНАЛЫ   ПЕРСОНАЛИИ   ОРГАНИЗАЦИИ   КОНФЕРЕНЦИИ   СЕМИНАРЫ   ВИДЕОТЕКА   ПАКЕТ AMSBIB
Общая информация
Последний выпуск
Архив
Импакт-фактор

Поиск публикаций
Поиск ссылок

RSS
Последний выпуск
Текущие выпуски
Архивные выпуски
Что такое RSS



Модел. и анализ информ. систем:
Год:
Том:
Выпуск:
Страница:
Найти






Персональный вход:
Логин:
Пароль:
Запомнить пароль
Войти
Забыли пароль?
Регистрация


Модел. и анализ информ. систем, 2018, том 25, номер 2, страницы 174–192 (Mi mais620)  

Сети Петри и временные автоматы

О корректности моделирования модульных вычислительных систем реального времени с помощью сетей временных автоматов

А. Б. Глонина, В. В. Балашов

Московский государственный университет им. М.В. Ломоносова, Ленинские горы, д. 1, г. Москва, 119991 Россия

Аннотация: Рассматривается задача проверки допустимости конфигураций модульных вычислительных систем реального времени (МВС РВ). Конфигурация считается допустимой, если все работы успевают выполниться на МВС РВ в рамках своих директивных интервалов. Предложена обобщенная модель функционирования МВС РВ и метод построения на её основе модели для конкретной конфигурации. Модель представляет собой сеть временных автоматов с остановкой таймеров. По вычислению сети автоматов предлагается строить временную диаграмму (ВД) функционирования МВС РВ, необходимую для проверки допустимости. В работе обосновывается корректность предложенного подхода. Из спецификаций на МВС РВ был выделен ряд требований, применимых к моделям МВС РВ и их компонентов на выбранном уровне абстракции. Модели считаются корректными, если удовлетворяют этим требованиям. Доказано, что если все модели компонентов системы удовлетворяют соответствующим требованиям, то модель МВС РВ, построенная согласно предложенному подходу, удовлетворяет требованиям к модели системы в целом (то есть корректна), а также является детерминированной. Под детерминированностью понимается однозначность построения ВД сети автоматов, соответствующей заданной конфигурации. Это позволяет использовать для проверки допустимости конфигурации любое вычисление соответствующей сети автоматов, что крайне важно для эффективности предложенного подхода, так как число возможных вычислений сети автоматов растет экспоненциально с числом работ в системе. Выполнение требований корректности к моделям компонентов системы может быть проверено автоматически с использованием верификатора и подхода автоматов-наблюдателей. Все разработанные нами модели компонентов системы удовлетворяют соответствующим требованиям, что было доказано с помощью верификатора UPPAAL. Если пользовательские модели компонентов системы удовлетворяют требованиям корректности, то они могут быть включены в модель МВС РВ, которая при этом останется корректной и детерминированной.

Ключевые слова: моделирование, верификация, интегрированная модульная авионика, планирование вычислений.

Финансовая поддержка Номер гранта
Российский фонд фундаментальных исследований 17-07-01566_а
Работа выполнена при финансовой поддержке РФФИ (грант № 17-07-01566).


DOI: https://doi.org/10.18255/1818-1015-2018-2-174-192

Полный текст: PDF файл (662 kB)
Список литературы: PDF файл   HTML файл

Реферативные базы данных:

Тип публикации: Статья
УДК: 519.7
Поступила в редакцию: 02.11.2017

Образец цитирования: А. Б. Глонина, В. В. Балашов, “О корректности моделирования модульных вычислительных систем реального времени с помощью сетей временных автоматов”, Модел. и анализ информ. систем, 25:2 (2018), 174–192

Цитирование в формате AMSBIB
\RBibitem{GloBal18}
\by А.~Б.~Глонина, В.~В.~Балашов
\paper О корректности моделирования модульных вычислительных систем реального времени с помощью сетей временных автоматов
\jour Модел. и анализ информ. систем
\yr 2018
\vol 25
\issue 2
\pages 174--192
\mathnet{http://mi.mathnet.ru/mais620}
\crossref{https://doi.org/10.18255/1818-1015-2018-2-174-192}
\elib{http://elibrary.ru/item.asp?id=34992610}


Образцы ссылок на эту страницу:
  • http://mi.mathnet.ru/mais620
  • http://mi.mathnet.ru/rus/mais/v25/i2/p174

    ОТПРАВИТЬ: VKontakte.ru FaceBook Twitter Mail.ru Livejournal Memori.ru


    Citing articles on Google Scholar: Russian citations, English citations
    Related articles on Google Scholar: Russian articles, English articles
  • Моделирование и анализ информационных систем
    Просмотров:
    Эта страница:52
    Полный текст:22
    Литература:6
     
    Обратная связь:
     Пользовательское соглашение  Регистрация  Логотипы © Математический институт им. В. А. Стеклова РАН, 2019