Авторитетность издания
Добавить в закладки
Следующий номер на сайте
Механизм контроля качества программного обеспечения оптико-электронных систем контроля
Аннотация:
Abstract:
Авторы: Балыков Е.А. () - , Царев В.А. () - | |
Ключевое слово: |
|
Ключевое слово: |
|
Количество просмотров: 13895 |
Версия для печати Выпуск в формате PDF (1.30Мб) |
Автоматизированные оптико-электронные системы контроля (ОЭСК) [1], позволяющие повысить эффективность управления технологическими процессами, чрезвычайно востребованы в промышленном производстве, транспортных перевозках, охранном наблюдении и т.п. Одной из составных частей ОЭСК является нетривиальное программное обеспечение (ПО), к которому предъявляются жесткие функциональные требования. Основной задачей, решаемой в процессе разработки ПО ОЭСК, является подтверждение и улучшение качества изготовляемых программных модулей (ПМ). Данная задача эффективно разрешается с помощью механизма контроля качества ПО ОЭСК, включающего процедуры ручного контроля, методы аналитической верификации и дисциплину тестирования [2,3]. При создании ПО ОЭСК приходится сталкиваться со значительными трудностями. Это обусловлено рядом факторов, специфичных для программных систем класса ОЭСК: - недостаточное развитие теоретических основ процесса верификации, тестирования и отладки ПМ ОЭСК, использующих разнообразные циклические структуры, массивы, подпрограммы, и операторы, которые могут потенциально привести к исключительным или аварийным ситуациям; - математическое обеспечение ОЭСК представлено в большей части эвристическими алгоритмами обработки и анализа изображений, которые не всегда обеспечивают получение правильного или оптимального решения, что обусловливает неприменимость методов верификации для доказательства корректности и затрудняет выявление источника ошибки, найденной в ПМ ОЭСК, реализующем эвристический алгоритм. Следовательно, необходимо развитие и адаптация существующих методов, а также построение новых способов контроля качества, которые бы учитывали специфику ОЭСК и позволяли создавать ПМ ОЭСК, обладающие высокими заданными характеристиками качества. Принятые в классических методах верификации программ (методах Флойда и Хоара) [4] допущения позволяют применять их к небольшому числу достаточно тривиальных программ. Реальные программные системы намного сложнее. К ним относятся ПМ ОЭСК, которые содержат такие программные структуры, как подпрограммы; массивы видеоизображений; особые операторы, которые при определенных значениях входных переменных могут не завершиться, привести к исключительной ситуации или аварийному сбою. Следовательно, необходимо развить и доработать классические методы верификации, чтобы они учитывали особенности рассмотренных программных элементов. Предложения по развитию метода Флойда, включают следующие этапы. 1. К существующим операторам, используемым при построении блок-схемы алгоритма программы 2. Для доказательства частичной корректности программы 3. Доказательство частичной корректности программы P, содержащей массив M, заключается в доказательстве истинности условий вида 4. Для доказательства завершаемости программы Предложения по развитию метода Хоара включают следующие этапы. 1. Для доказательства частичной корректности программы
2. Доказательство частичной корректности программы Для доказательства завершаемости программы При проектировании эвристических алгоритмов принимаются определенные допущения, не имеющие строгого математического обоснования, а основанные исключительно на опыте и интуиции разработчика, вследствие чего ПМ ОЭСК, реализующие подобные алгоритмы, не всегда вырабатывают правильное решение. Следовательно, известные методы верификации неприменимы для доказательства правильности функционирования ПМ ОЭСК вида В [5] отмечено, что корректность программы определяется двумя свойствами: корректностью функционирования и корректностью построения, или так называемой конструктивной правильностью. Поэтому в статье предлагается использование методов верификации для доказательства конструктивной правильности Методика доказательства конструктивной правильности включает следующие шаги. 1. Верификация завершаемости ПМ ОЭСК вида 2. Верификация правильности построения ПМ ОЭСК вида 2.1. Декомпозиция программы 2.2. Доказательство с помощью известных методов аналитической верификации частичной корректности всех этапов 2.3. Вывод о конструктивной правильности Верификация ПМ ОЭСК вида Основное отличие эвристических алгоритмов от точных заключается в том, что они не всегда дают правильное решение. Следовательно, если с помощью некоторого механизма контроля качества (например тестирования) выявлена ошибка в ПМ ОЭСК вида Часть модели ЖЦ ПО ОЭСК, связанная с проектированием и реализацией алгоритмического обеспечения, представлена на рисунке. Как правило, алгоритмическое обеспечение ОЭСК разрабатывается математиком с использованием вспомогательного языка, предоставляемого специализированными математическими пакетами (Mathlab, Mathcad), позволяющими проводить проверку эффективности и осуществлять предварительную верификацию синтезированных алгоритмов. Затем спецификация алгоритма вида Для разрешения проблемы поиска источника ошибки, выявленной в ПМ ОЭСК вида · Определение исходных данных. Пусть исходный эвристический алгоритм задан спецификацией · Проверка корректности трансляции. Источником выявленной ошибки является неправильная трансляция алгоритма в основную реализацию, если выявлено несоответствие между спецификациями или между описанием и реализацией · Следует отметить, что этап проверки корректности трансляции алгоритма в реализацию достаточно сложен и нетривиален. Поэтому способ поиска источника ошибки дополнен методикой проверки корректности трансляции алгоритма в реализацию, которая включает следующие шаги. 1. Определение семантического соответствия между спецификацией эвристического алгоритма и спецификацией основной реализации 1.1. Построение эквивалентной спецификации вида: 1.2. Проверка семантического равенства всех термов и утверждений, входящих в спецификацию алгоритма и эквивалентную спецификацию: 1.3. Фиксация всех выявленных несоответствий и различий между 1.4. Семантическое равенство термов, входящих в исходную спецификацию алгоритма и спецификацию реализации 2. Определение семантического соответствия между описанием эвристического алгоритма и его основной программной реализацией 2.1. Построение эквивалентного описания 2.2. Проверка того, учитывает ли 2.3. Проверка семантического равенства эквивалентного и исходного описания Если Реализация алгоритма на нескольких языках программирования приводит к значительному удорожанию процесса разработки и увеличению сроков выпуска ПС. Однако ЖЦ ПО ОЭСК предусматривает две стадии разработки: фаза синтеза алгоритма с одновременной его реализацией на вспомогательном языке и фаза реализации алгоритма на основном языке программирования. Следовательно, в рамках ЖЦ ПО ОЭСК реализация алгоритмов всегда осуществляется в двух языках программирования, что обусловливает минимальные затраты, связанные с поиском источника ошибки в ПМ ОЭСК вида Среди широко используемых в рамках ПМ ОЭСК программных конструкций можно выделить циклические структуры. К наиболее распространенным дефектам циклических структур относятся ошибки некорректного изменения итераторов, которые могут привести к зацикливанию соответствующего ПМ и зависанию работы ОЭСК. Анализ существующих методов тестирования показал отсутствие каких-либо методик тестирования завершаемости циклических структур. В статье представлена новая методика, позволяющая осуществлять целенаправленное тестирование завершаемости циклов ПМ ОЭСК. Методика разработана с учетом специфики циклов, применяемых в ПМ ОЭСК для обработки массивов видеоданных, заключающаяся в изменении значений итераторов цикла в соответствии, как правило, с монотонными функциями. Предложенная методика базируется на принципах верификации и включает следующий ряд шагов. 1. Проверка на входе в цикл возможности достижения итератором значения выхода из цикла 2. Проверка внутри тела цикла изменения итератора на некоторую необязательно постоянную величину 3. Исполнение второго шага в соответствии с одним из структурных критериев для покрытия тех команд, ветвей или маршрутов внутри тела цикла, которые приводят к модификации значения итератора цикла. Представленная методика позволяет повысить качество ПМ ОЭСК, широко использующих циклические структуры, повысить эффективность процедур контроля качества и снизить трудоемкость тестирования циклов. Список литературы 1. Еремин С.Н., Малыгин Л.Л., Рачинский Е.В. Оптико-электронные системы контроля. Алгоритмы обработки // Тез. доклад. и сообщ. XIII межвуз. воен.-науч. конф.– Череповец: ЧВИИР. - 1999. - Ч. 2. - С. 21-22. 2. Маейрс Г. Искусство тестирования программ/Пер. с англ. – М.: Финансы и статистика, 1982. – 176 с. 3. Макгрегор Джон, Сайкс Дэвид. Тестирование объектно-ориентированного программного обеспечения. / Пер. с англ. – К.: ООО “ТИД ДС”, 2002. - 432 с. 4. Непомнящий В.А., Рякин О.М. Прикладные методы верификации программ / Под ред. А.П. Ершова. – М.: Радио и связь, 1988. – 256 с. 5. Брауде Э. Технология разработки программного обеспечения. – СПб.: Питер, 2004. - 655 с. |
Постоянный адрес статьи: http://swsys.ru/index.php?page=article&id=440 |
Версия для печати Выпуск в формате PDF (1.30Мб) |
Статья опубликована в выпуске журнала № 4 за 2006 год. |
Возможно, Вас заинтересуют следующие статьи схожих тематик:
- Реализация теней с помощью библиотеки OpenGL
- Метод интегрированного описания топологических отношений в геоинформационных системах
- ДИНАМИКА-2 - программа для решения осесимметричных и плоских задач
- Информационные модели на основе CASE–средств промышленных объектов для информационной поддержки принятия решений
- Интеллектуальная поддержка реинжиниринга конфигураций производственных систем
Назад, к списку статей