Программные продукты и системы

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

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

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

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

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

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

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

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

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

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