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

Автоматизированные оптико-электронные системы контроля (ОЭСК) [1], позволяющие повысить эффективность управления технологическими процессами, чрезвычайно востребованы в промышленном производстве, транспортных перевозках, охранном наблюдении и т.п.

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

При создании ПО ОЭСК приходится сталкиваться со значительными трудностями. Это обусловлено рядом факторов, специфичных для программных систем класса ОЭСК:

-    недостаточное развитие теоретических основ процесса верификации, тестирования и отладки ПМ ОЭСК, использующих разнообразные циклические структуры, массивы, подпрограммы, и операторы, которые могут потенциально привести к исключительным или аварийным ситуациям;

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

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

Принятые в классических методах верификации программ (методах Флойда и Хоара) [4] допущения позволяют применять их к небольшому числу достаточно тривиальных программ. Реальные программные системы намного сложнее. К ним относятся ПМ ОЭСК, которые содержат такие программные структуры, как подпрограммы; массивы видеоизображений; особые операторы, которые при определенных значениях входных переменных могут не завершиться, привести к исключительной ситуации или аварийному сбою.

Следовательно, необходимо развить и доработать классические методы верификации, чтобы они учитывали особенности рассмотренных программных элементов.

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

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

2.        Для доказательства частичной корректности программы , содержащей подпрограммы, необходимо предварительно доказать частичную корректность всех подпрограмм: , где  – предусловия и постусловия соответствующих подпрограмм. Доказательство корректности подпрограмм, как и основной программы, следует проводить относительно расширенной спецификации вида . Доказательство истинности всех условий верификации, следующих за подпрограммой , необходимо проводить с использованием предиката . Истинность постусловия  обеспечивается истинностью  и . А для вывода истинности  используется стандартное условие верификации Флойда вида  , где  – базовый путь, ведущий в подпрограмму ;  – вектор переменных пути;  – точка начала пути;  – индуктивное утверждение для начальной точки пути;  – предикат пути;  – функция отображения состояния памяти.

3.        Доказательство частичной корректности программы P, содержащей массив M, заключается в доказательстве истинности условий вида , где  – утверждение, задающее принадлежность индексов массиву ;  – оператор в котором осуществляется доступ к элементам массива ;  – вектор индексов или указателей.

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

Предложения по развитию метода Хоара включают следующие этапы.

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

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

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

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

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

В [5] отмечено, что корректность программы определяется двумя свойствами: корректностью функционирования и корректностью построения, или так называемой конструктивной правильностью. Поэтому в статье предлагается использование методов верификации для доказательства конструктивной правильности  ПМ ОЭСК вида , что позволит повысить их качество.

Методика доказательства конструктивной правильности включает следующие шаги.

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

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

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

2.2. Доказательство с помощью известных методов аналитической верификации частичной корректности всех этапов  относительно своих спецификаций , .

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

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

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

Часть модели ЖЦ ПО ОЭСК, связанная с проектированием и реализацией алгоритмического обеспечения, представлена на рисунке.

Как правило, алгоритмическое обеспечение ОЭСК разрабатывается математиком с использованием вспомогательного языка, предоставляемого специализированными математическими пакетами (Mathlab, Mathcad), позволяющими проводить проверку эффективности и осуществлять предварительную верификацию синтезированных алгоритмов. Затем спецификация алгоритма вида , где  – предусловие и постусловие эвристического алгоритма, а также описание алгоритма (псевдокод или блок-схема) передаются на этап реализации. На этапе реализации осуществляется кодирование алгоритма программистом с использованием основного языка программирования (С/C++, MC++, C#), предоставляемого интегрированной средой разработки (MS Visual Studio.net). Спецификация реализации  получена из исходной спецификации алгоритма  путем дополнения спецификации интерфейсной части .

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

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

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

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

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

1.        Определение семантического соответствия между спецификацией эвристического алгоритма и спецификацией основной реализации . Как правило, спецификация алгоритма записывается с помощью строгих математических обозначений и отражает суть алгоритма. Спецификация основной реализации является более детальной и записывается с учетом синтаксиса конкретного языка программирования, а также учитывает особенности аппаратного представления и хранения данных, адаптирует исходную спецификацию к конкретным типам данных и дополняет ее требованиями к интерфейсной части (так называемая интерфейсная обвязка).

1.1. Построение эквивалентной спецификации вида: .

1.2. Проверка семантического равенства всех термов и утверждений, входящих в спецификацию алгоритма и эквивалентную спецификацию: .

1.3. Фиксация всех выявленных несоответствий и различий между  и .

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

2.        Определение семантического соответствия между описанием эвристического алгоритма и его основной программной реализацией . Как правило, описание алгоритма задается в общем виде и не учитывает конкретные особенности реализации (типы данных, интерфейсной части и языка программирования). Поэтому при реализации алгоритм определенным образом модифицируется.

2.1. Построение эквивалентного описания  в виде псевдокода или блок-схемы.

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

2.3. Проверка семантического равенства эквивалентного и исходного описания  путем прямого сопоставления полученного и исходного псевдокода или блок-схем.

Если , то принимается решение о корректности трансляции алгоритма в реализацию , в противном случае констатируется несоответствие описания и реализации и принимается решение об ошибке трансляции.

Реализация алгоритма на нескольких языках программирования приводит к значительному удорожанию процесса разработки и увеличению сроков выпуска ПС. Однако ЖЦ ПО ОЭСК предусматривает две стадии разработки: фаза синтеза алгоритма с одновременной его реализацией на вспомогательном языке и фаза реализации алгоритма на основном языке программирования. Следовательно, в рамках ЖЦ ПО ОЭСК реализация алгоритмов всегда осуществляется в двух языках программирования, что обусловливает минимальные затраты, связанные с поиском источника ошибки в ПМ ОЭСК вида .

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

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

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

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

3.        Исполнение второго шага в соответствии с одним из структурных критериев для покрытия тех команд, ветвей или маршрутов внутри тела цикла, которые приводят к модификации значения итератора цикла.

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

Список литературы

1.        Еремин С.Н., Малыгин Л.Л., Рачинский Е.В. Оптико-электронные системы контроля. Алгоритмы обработки // Тез. доклад. и сообщ. XIII межвуз. воен.-науч. конф.– Череповец: ЧВИИР. - 1999. - Ч. 2. - С. 21-22.

2.        Маейрс Г. Искусство тестирования программ/Пер. с англ. – М.: Финансы и статистика, 1982. – 176 с.

3.        Макгрегор Джон, Сайкс Дэвид. Тестирование объектно-ориентированного программного обеспечения. / Пер. с англ. – К.: ООО “ТИД ДС”, 2002. - 432 с.

4.        Непомнящий В.А., Рякин О.М. Прикладные методы верификации программ / Под ред. А.П. Ершова. – М.: Радио и связь, 1988. – 256 с.

5.        Брауде Э. Технология разработки программного обеспечения. – СПб.: Питер, 2004. - 655 с.