научная статья по теме CONTROLLED EXECUTION WITH EXPLICIT MODEL Математика

Текст научной статьи на тему «CONTROLLED EXECUTION WITH EXPLICIT MODEL»

- ВЫЧИСЛИТЕЛЬНЫЕ СИСТЕМЫ РЕАЛЬНОГО ВРЕМЕНИ ~

УДК 681.3.06

КОНТРОЛИРУЕМОЕ ВЫПОЛНЕНИЕ С ЯВНОЙ МОДЕЛЬЮ

© 2014 г. В.Б. Бетелин, В.А. Галатенко, К.А. Костюхин

Научно-исследовательский институт системных исследований 117218 Москва, Нахимовский просп., 36, к. 1 E-mail: {betelin,galat,kost} @niisi. msk.ru Поступила в редакцию 10.08.2013

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

1. ПОНЯТИЕ КОНТРОЛИРУЕМОГО ВЫПОЛНЕНИЯ

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

• интеграция средств информационной безопасности, отладки и управления;

нения на все этапы жизненного цикла аппаратно-программных комплексов;

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

Частными случаями контролируемого выполнения являются:

ционными системами;

ты систем;

пых характеристик функционирования систем.

Средства управления информационными системами ориентированы на такие крупные сущности, как сети, узлы сетей, хосты, устройства, приложения. Эти средства применяются на этапе эксплуатации систем.

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

В данной статье основное внимание будет уделено применению концепции контролируемого выполнения для моделирования различных аспектов поведения целевых аппаратно-программных комплексов.

2. МОДЕЛИРОВАНИЕ СИСТЕМ И

КОЛИЧЕСТВЕННЫХ ХАРАКТЕРИСТИК ИХ ФУНКЦИОНИРОВАНИЯ

2.1. Модель распределенных вычислений

Описание сложной системы вычислений с различными разносторонними требованиями требует наличия формализма, позволяющего описать

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

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

мизации;

рон и с различной степенью детализации;

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

Некоторые из вышеперечисленных аспектов уже изучались в контексте формальных моделей. В частности в работе [3] строится формальное описание системы моделирования и преобразования моделей МОК [14]. В работе [5] была предложена количественная модель формальных вычислений, позволяющая оценить степень оптимизации преобразований приложения.

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

Сбои моделируются с помощью множества "сбойных" действий F, которые изменяют

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

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

Приведем несколько определений:

Определение 1. Состояние - отображение

набора переменных Var на, набор значений Val.

s : Var ^ Val.

Определение 2. Действие - это некоторый предикат над переменными, их значениям,и, а также их измененными значениям,и, которые обозначаются штрихом:

X + 1 ^ y.

Над бесконечными последовательностями действий а = а\,а2,... можно рассматривать временные формулы, которые составлены из булевых операторов и операторов линейной временной логики. Например, рф](а) - предикат ф выполняется для любого суффикса а [оф](а) - предикат ф выполняется хотя бы однажды.

Определение 3. Программа - набор, состоящий из следующих компонент:

1. Конечное непустое множество v состояний;

2. Подмножество внутренних состояний x множества v;

3. Предикат первоначального состояния Q, включающий, в себя только переменные из v;

4- Конечный набор A действий над переменными из v.

Определение 4. Вычисление программы Р = (V, X, в, А) - это последовательность состояний а, такая что выполняются два условия:

1. а0 удовлетворяет в,

2. аг+1 = аг или найдется такое т € А, что аг+1, аг удовлетворяет т.

Р=

(V, X, в, А) рассмотрим

Мр = у т.

т еА

Тогда точная спецификация, определяется как

П(Р) = в V П[Мр]„

и описывает набор всех разрешенных состояний программы.

Определение 6. Внешняя спецификация, программы задается как

Ф(Р) = ЗХ.П(Р)

и описывает все возможные последовательности внешних состояний системы.

И, наконец, введем определение уточнения программ, позволяющее ввести понятие верификации.

Определение 7. Отношение уточнения Р Ц Ри означает, что программа Р корректно реализует Р^, то есть отношение

Ф(Р1) ^ Ф(Ри)

выполнено для внешних спецификаций.

В работах [11] и [12] описываются дальнейшие расширения предложенных определений и возможности вывода теорем. Например, для того, чтобы описать сбои, вводится множество действий ^ и понятие внешних и внутренних спецификаций, сбойного вычисления ^(Р, ^) = (V, х, в, А и ^), устойчивого к сбоям уточнения и т.д.

Мы же перейдем к вариантам расширения описания для учета необходимых нам свойств.

2.2. Моделирование разных аспектов вычисления,

Естественно описывать вычисление несколькими моделями, отражающими различные аспекты приложения, например, модель памяти и модель занимаемой пропускной способности сети могут быть различными, дополняя основную модель вычислений. Кроме того, набор ограничений и утверждений о приложении может быть достаточно разнородным и задаваться:

1. результатами тестирования;

2. выведенными в процессе анализа приложения утверждениями;

3. проверками во время выполнения;

Таким образом кроме понятия уточнения необходимо задать более сложное соотношение между различными моделями выполнения, описывающее совместное дополнение программ, сводимое к нужному нам выполнению.

Определим операцию комбинации программ:

Определение 8. Введем, внутреннюю и внеш-

Рг

П(Р1, . . . , Рп) = (лвг) V (лп[Мр.ы, Ф(Р1,...,Рга) = Зж.П(Р1,...,Рп).

Определение 9. Будем говорить, что Р

Р1,..., Рн, если

Ф(Р) ^ Ф(Р1,...,Рп).

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

Можно определить и другие операции над моделями программ [5].

Р1

Р2 определяется набором со стояний 7и1 х Щ, начальным состоянием в1 х в2 и набором действий А1 и А2.

Другой операцией, позволяющей абстрагироваться от внешней переменной является операция сокрытия переменной.

Определение 11. Для программы, P и переменной Var f x определим, программу Hidex(P) с помощью набора состояний v и набора внутренних состояний х' = x U Var.

2.3. Моделирование ресурсов

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

Например, время моделируется с помощью временных меток действий. Каждое действие т связывается с нижней временной границей L(t) и верхней временной границей U (т). Для того, чтобы считаться успешным, действие должно выполняться по крайней мере L(t) временных интервалов. Действие не должно выполняться реже, чем U(т). Модель может включать в себя более сложных механизмов планирования, например, планирования с временным освобождением ресурсов.

Определим набор ресурсов zi е Z и для каждого из них и для каждого действия определим верхнюю и нижнюю границу потребления ресурсов для каждого действия Щ(т) и Li(T).

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

now = 0 е в, (1)

U[now' е (now, ro))]now, (2)

Vt е R+, o(now>t). (3)

Для механизма простейшего выделения памяти формулируются более простые условия Dmem(a) > 0,mem' > mem — Um(T),mem' < mem — Lm(T), хотя, для сложных механизмов выделения можно учитывать и более точные характеристики, такие как фрагментацию памяти.

В случае работы с ресурсом нам необходимо расширить определение внутренней и внешней спецификации соответственно:

Ер = V Ег(т),

т еА

П(Р) = в V □ [Ыр]„ V □ [Ер]„,

где Ег - ограничения, накладываемые на использование ресурса.

Более сложные модели использования ресурсов требуют дополнительных построений, поэтому некоторые аспекты, не так часто применяемые в системах реального времени остались не описанными. Например, представляет интерес описание задачи планирования не только времени, но и совместного планирования ресурсов.

2.4. Оптимизация

Возможность учета понятия оптимизации является естественным требованием к формальной модели приложения. Необходимо ра

Для дальнейшего прочтения статьи необходимо приобрести полный текст. Статьи высылаются в формате PDF на указанную при оплате почту. Время доставки составляет менее 10 минут. Стоимость одной статьи — 150 рублей.

Показать целиком