Адаптация формальных методов

В связи с разработкой технологии создания порталов проведены исследования в области адаптации формальных математических методов построения программных систем к условиям использования экстремального программирования [46]. Здесь пользовательские требования характеризуют конкретные компоненты и элементы данных, поэтому они формализуются бескванторными предложениями языка первого порядка. Доказано, что класс $K$ формальных моделей, удовлетворяющих таким требованиям, замкнут относительно взятия изоморфных образов, подсистем и расширений. Также доказано, что все такие классы образуют атомную булеву алгебру $B_\sigma$, причем каждый атом $A$ состоит из всех алгебраических систем, в которые единственным образом изоморфно вкладывается некоторая система из $A$, не имеющая собственных подсистем.

Таким образом, выбор алгебраической спецификации в экстремальном программировании следует проводить в два этапа. Сначала нужно выбрать подходящий атом алгебры $B_\sigma$, причем из-за слабости набора исходных требований нельзя предложить естественных критериев, позволяющих сделать такой выбор однозначным. Зато далее имеется единственная (с точностью до изоморфизма) алгебраическая система, которая является одновременно инициальной и изоинициальной моделью в выбранном классе, т.е. наиболее адекватной алгебраической спецификацией.

Выполнен сравнительный анализ возможностей различных формальных методов по обеспечению качества сервиса информационно-вычислительных систем [50]. С этой целью ключевые характеристики эффективности вычислительных систем идентифицированы на базе стандарта ISO/IEC-9126. Построена абстрактная формальная модель качества таких систем с использованием декларативного языка NoFun. Представлена и обоснована классификация основных математических методов разработки программных систем по критерию способности реализовать различные составляющие этой модели.

Отправным пунктом для применения формальных методов служит представление вычислительной задачи в виде совокупности операций, выполняемых над числовыми данными различной природы (натуральными, вещественными числами и т.д.). Действие каждой операции задается как функция на множестве возможных значений данных. Множества значений вместе с правилами выполнения операций образуют абстрактные типы данных (АТД), описываемые на математическом языке (в общем случае многосортными) алгебрами. Различным фрагментам задачи сопоставляются компоненты вычислительной системы, отвечающие за выполнение определенных наборов операций. В ходе функционирования системы данные передаются для обработки между экземплярами компонентов, выбор которых при решении сложных задач приходится осуществлять динамически, исходя из текущих профилей их загрузки. Крупномасштабные распределенные вычислительные системы с динамическим развертыванием задач известны под общим названием Grid. На математическом языке динамика функционирования многокомпонентных систем описывается с привлечением аппарата мутирующих (эволюционных) алгебр, известных также как машины абстрактных состояний (МАС). В рамках этого аппарата подходящая алгебра сопоставляется каждому состоянию каждого компонента, и вводится специальный метаязык для описания правил перехода между состояниями.

Программная реализация вычислительной системы заключается в переводе алгебраической спецификации на язык программирования, поддерживаемый целевой аппаратной платформой. При этом возникает ряд сложностей, связанных с невозможностью точного воспроизведения свойств математических объектов средствами современных компьютеров. Так, любой элемент данных может иметь лишь конечное количество различных значений, определяемое объемом доступных ресурсов памяти. Поэтому стандартные модели арифметики, обладающие бесконечными основными множествами, остаются сугубо абстрактными типами данных, не реализуемыми на практике. Существуют различные способы построения моделей вычислений -- (односортных) конечных алгебр, в той или иной степени ``аппроксимирующих'' поведение требуемых АТД и реализуемых в программно-аппаратных средствах. Различные модели вычислений оптимизируются по различным критериям эффективности, поэтому они часто плохо совмещаются друг с другом, и при организации обмена данными приходится реализовывать сложные процедуры согласования значений. Систематический подход к построению и анализу моделей вычислений основан на понятии частичной интерпретации -- специальной модификации стандартного теоретико-модельного подхода, позволяющего строить конечные модели, верифицирующие подмножества теорем арифметики, отбираемые согласно различным явно заданным критериям. При помощи этой конструкции показано, что наиболее широко распространенным моделям вычислений отвечают алгебраические представления конечнозначной логики Лукасевича.

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

Естественным критерием практической полезности модели вычислений, определяющим границы класса рассматриваемых конечных алгебр, является возможность управления потоком вычислений путем проверки равенства значения элемента данных любому из поддерживаемых чисел. Доказывается, что этот критерий выделяет так называемые $s$-примальные (semi-primal) алгебры, клоны операций которых содержат все функции, сохраняющие все их подалгебры. Также доказывается, что он эквивалентен наличию (достаточно большого объема) адресуемой памяти, в которой можно хранить массивы данных. Любой из этих признаков является характерным для РАМ-машины -- классической модели вычислительного устройства общего назначения, исходя из возможностей которого специфицируются и анализируются вычислительные алгоритмы. Для проектирования многокомпонентных вычислительных систем, (динамически) развертываемых на разнородных реализациях РАМ-машины, применяется формализация подхода на основе контрактов, данная при помощи аппарата МАС. Получен ряд технических результатов о свойствах $s$-примальных алгебр. Доказано, что для всякого $n > 0$ они образуют интервал в решетке всех клонов операций алгебр с $n$-элементным основным множеством. Описано правило построения штриха Шеффера для любой $s$-примальной алгебры. Сформулирован критерий возможности применения $s$-примальной алгебры для представления некоторой конечнозначной логики. Дано формальное доказательство пригодности $s$-примальных алгебр в качестве моделей архитектуры распределенных вычислительных систем, основанное на аппарате теории категорий.

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

Для решения этой задачи в конце 1990-х годов была предложена новая методология -- аспектно-ориентированный подход к разработке программного обеспечения (АОП). Согласно АОП, выполнение автоматизируемых процессов разбивается на аспекты -- логически замкнутые сквозные потоки функциональности, подлежащие раздельной реализации и последующей композиции (weaving) в явно заданных точках. Каждый аспект отвечает за обеспечение отдельной системной характеристики качества, а все вместе они предоставляют достаточный объем функциональных возможностей для решения целевых задач. Многие технологии разработки программного обеспечения специально ориентированы на реализацию отдельных аспектов, поэтому аспектная декомпозиция облегчает организацию деятельности коллектива разработчиков, являющихся узкими специалистами. В частности, для вычислительных аспектов удается провести глубокий анализ эффективности с применением предложенных выше алгебраических методов.