ISSN 0236-235X (P)
ISSN 2311-2735 (E)

Публикационная активность

(сведения по итогам 2018 г.)
2-летний импакт-фактор РИНЦ: 0,678
2-летний импакт-фактор РИНЦ без самоцитирования: 0,541
Двухлетний импакт-фактор РИНЦ с учетом цитирования из всех
источников: 1,047
5-летний импакт-фактор РИНЦ: 0,460
5-летний импакт-фактор РИНЦ без самоцитирования: 0,389
Суммарное число цитирований журнала в РИНЦ: 7170
Пятилетний индекс Херфиндаля по цитирующим журналам: 310
Индекс Херфиндаля по организациям авторов: 412
Десятилетний индекс Хирша: 19
Место в общем рейтинге SCIENCE INDEX за 2018 год: 303
Место в рейтинге SCIENCE INDEX за 2018 год по тематике "Автоматика. Вычислительная техника": 10

Больше данных по публикационной активности нашего журнале за 2008-2018 гг. на сайте РИНЦ

Добавить в закладки

Следующий номер на сайте

1
Ожидается:
16 Марта 2020

В НИИ системных исследований РАН построена модель вычислений, описывающая основные аспекты контролируемого выполнения распределенных ответственных приложений реального времени

07.07.2010

Для описания сложной системы вычислений с разносторонними требованиями необходимо наличие формализма, позволяющего описывать объекты системы и их взаимодействие, унифицировать подходы к вычислениям. Построенная модель вычислений описывает основные аспекты контролируемого выполнения распределенных ответственных приложений реального времени и включает:

-    статическую и динамическую верификацию корректности;

-    оптимизацию и проверку результатов оптимизации;

-    устойчивость к сбоям;

-    представление вычисления с разных сторон и с различной степенью детализации;

-    возможность описания ресурсов.

 Предложенная автором модель построена на основе формального описания устойчивой системы реального времени, включающего восстановление системы после сбоев, временные свойства и планируемость. В качестве модели приложения используется система переходов, в качестве общей спецификации – логика действий со временем (TLA – Temporal Logic of Actions) [3].

 Сбои моделируются с помощью множества «сбойных» действий F, которые изменяют состояние так же, как и обычные вычисления. Устойчивость к сбоям обеспечивается проведением корректирующих действий. Как показано, доказательство устойчивости к сбоям в такой модели не отличается от доказательства функциональной корректности.

 Программы и спецификации описываются в модели TLA как логические формулы, позволяя таким образом устанавливать правила вывода и описывать выполнение без времени, выполнение со временем, сбои и планируемость.

 Подробное описание дается в статье «Математическая модель контролируемого выполнения», автор Шмырев Н.В. (Научно-исследовательский институт системных исследований РАН, г. Москва).