Software & Systems

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

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

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

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

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

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

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

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

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

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

Определение 1. Состояние – это отображение набора переменных Var на набор значений Val:

s : Var ® Val.

Определение 2. Действие – это некоторый предикат над переменными, их значениями, а также их измененными значениями, которые обозначаются штрихом: x'+1≤y.

В качестве бесконечных последовательностей действий s=s1, s2,… можно рассматривать временные формулы, которые составлены из булевых операторов и операторов линейной временной логики.

Например: [ÿj](s) – предикат j выполняется для любого суффикса s, [àj](s) – предикат j выполняется хотя бы однажды.

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

-    конечное непустое множество  состояний;

-    подмножество внутренних состояний  множества ;

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

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

Определение 4. Вычисление программы P=(, , Q, A) – это последовательность состояний s, такая, что выполняются два условия:

1)  s0 удовлетворяет Q;

2)  si+1=si или найдется такое tÎA, что si+1, si удовлетворяет t.

Определение 5. Для программы P=(, , Q, A) рассмотрим NP=t.

Тогда точная спецификация определяется как P(P)=QÚÿ[NP]  и описывает набор всех разрешенных состояний программы.

Определение 6. Внешняя спецификация программы задается как F(P)=$P(P) и описывает все возможные последовательности внешних состояний системы.

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

Определение 7. Отношение уточнения PlÍPh означает, что программа Pl корректно реализует Ph, то есть отношение F(Pl)®F(Ph) выполнено для внешних спецификаций.

В работах [1] и [4] описываются дальнейшие расширения предложенных определений и возможности вывода теорем. Например, для описания сбоев вводятся множество действий F и понятия внешних и внутренних спецификаций, сбойного вычисления F(P,F)=(, , Q, AÈF), устойчивого к сбоям уточнения, и т.д.

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

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

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

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

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

Определение 8. Введем внутреннюю и внешнюю спецификации набора программ Pi:

P(P1, …, Pn)=(ÙQi)Ú(Ùÿ[NPi]),

F(P1, …, Pn)=$P(P1, …, Pn).

Определение 9. Будем говорить, что программа P является уточнением набора P1, …, Pn, если F(P)®F(P1,…,Pn).

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

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

Определение 10. Композиция программ P1 и P2 определяется набором состояний ´, начальным состоянием Q1´Q2 и набором действий A1ÈA2.

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

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

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

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

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

Определив набор ресурсов ziÎZ, для каждого ресурса и каждого действия отыщем верхнюю и нижнюю границы потребления ресурсов Ui(t) и Li(t). Для каждого из ресурсов нужно ввести и специальные ограничения, которые описывают их расходование (например для времени):

now=0ÎQ,                                                             (1)

ÿ[now'Î(now,µ))]now,                                         (2)

"tÎR+, à(now>t).                                                 (3)

Для механизма простейшего выделения памяти формулируются более простые условия: ÿmem(s)>0, mem'>mem-Um(t), mem'

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

RP=Ri(t), P(P)=QÚÿ[NP]Úÿ[RP],

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

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

Оптимизация

Возможность учета понятия оптимизации является естественным требованием к формальной модели приложения. Необходимо рассмотреть две проблемы, возникающие при этом: проверка корректности оптимизирующего преобразования и количественное определение результатов оптимизации. Первая проблема может быть решена с помощью введения эталонной модели вычисления Pe, таким образом, корректность оптимизации можно определить как соответствие эталонной модели вычисления P1ÍPeÙP2ÍPe. То есть для оценки корректности оптимизации необходимо зафиксировать эталонную модель вычисления.

Чтобы ввести количественные оценки эффективности для последующей оптимизации, необходимо ввести внутренние переменные для оптимизации и задать соотношения, описывающие затраты на каждый переход из состояния s в состояние si и действия t–C(t, s, s'). Соответственно изменяется внутренняя спецификация:

CP=C(t, s, s'),

P(P)=Q Ú ÿ[NP]Úÿ[RP]Úÿ[CP].

Полная модель приложения

Расширяя описание приложения, получим следующую формальную модель.

Определение. Программа описывается такими сущностями:

-    программа без времени P(,, Q, A);

-    набор сбоев F и соответствующая программа со сбоями с условием F(P,F)ÍP;

-    счетчик часов now со свойствами време- ни (1);

-    внутренние состояния, описывающие наличие ресурсов, таких как доступная память;

-    функции расхода ресурсов Li(t) и Ui(t), задающие границы потребления ресурсов для каждого действия из P;

-    ценовые функции C(t, s, s'), используемые для оптимизации;

-    внутренние и внешние спецификации P(P) и F(P).

Для подобного описания можно сформулировать свойства в терминах временных выражений F и доказать их: F(P)®j, в том числе и для набора спецификаций P1, …, Pn, оценить корректность оптимизации с помощью эталонной модели Pe и вычислить результат оптимизации с помощью ценовой функции.

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

Литература

1.   Liu Z., Joseph M. Real-Time and Fault-Tolerant Systems. Specification, verification, refinement and scheduling, UUNU/IIST, 2005.

2.   Pnueli A. The temporal logic of programs // 18th Annual Symposium on Foundations of Computer Science, 1977.

3.   Lamport L. The temporal logic of actions // ACM Transactions on Programming Languages and Systems, 1994. Vol. 16 (3).

4.   Manna Z., Pnueli A. The Temporal Logic of Reactive and Concurrent Systems: Specification, Springer-Verlag, 1991.

5.   Организация отладочного комплекса для целевых систем со сложной архитектурой / Н.И. Вьюкова [и др.] // Информационная безопасность. Микропроцессоры. Отладка сложных систем; под ред. В.Б. Бетелина. М.: НИИСИ РАН, 2004.