Главная страница
Навигация по странице:

  • 6.2 Проверка адекватности модели

  • Верификация имитационной модели Верификация

  • 6.4 Валидация данных имитационной модели

  • Методы доказательства правильности программ

  • Особенности тестирования различных приложений. Лекция Особенности тестирования различных приложений. Автоматиз. Тестирование Вебприложений


    Скачать 0.61 Mb.
    НазваниеТестирование Вебприложений
    АнкорОсобенности тестирования различных приложений
    Дата14.04.2023
    Размер0.61 Mb.
    Формат файлаpdf
    Имя файлаЛекция Особенности тестирования различных приложений. Автоматиз.pdf
    ТипДокументы
    #1061756
    страница5 из 5
    1   2   3   4   5
    (testing) - планируемый итеративный процесс, направленный главным
    образом на поддержку процедур верификации и валидации
    имитационных моделей и данных.
    Некоторые полезные процедуры тестирования рассмотрим ниже. Более широкое изложение методов тестирования имитационных моделей можно найти в специальной литературе [20, 33, 56].
    6.2 Проверка адекватности модели
    При моделировании исследователя прежде всего интересует, насколько хорошо модель представляет моделируемую систему (объект моделирования).
    Модель, поведение которой слишком отличается от поведения моделируемой системы, практически бесполезна.

    Различают модели существующих и проектируемых систем.
    Если реальная система (или ее прототип) существует, дело обстоит достаточно просто. Поэтому для моделей существующих систем исследователь должен выполнить проверку адекватности имитационной модели объекту моделирования, т.е. проверить соответствие между поведением реальной системы и поведением модели.
    На реальную систему воздействуют переменные G*, которые можно измерять, но нельзя управлять, параметры Х*, которые исследователь может изменять в ходе натурных экспериментов. На выходе системы возможно измерение выходных характеристикY*.
    При этом существует некоторая неизвестная исследователю зависимость между ними Y*=f*(Х*, G*).
    Имитационную модель можно рассматривать как преобразователь входных переменных в выходные. В любой имитационной модели различают составляющие: компоненты, переменные, параметры, функциональные зависимости, ограничения, целевые функции. Модель системы определяется как совокупность компонент, объединенных для выполнения заданной функции Y = f(Х, G).Здесь Y, Х, G - векторы соответственно результата действия модели системы выходных переменных, параметров моделирования,
    входных переменных модели. Параметры модели Х исследователь выбирает произвольно, G -принимают только те значения, которые характерны для данных объекта моделирования.
    Очевидный подход в оценке адекватности состоит в сравнении выходов
    модели и реальной системы при одинаковых (если возможно) значениях
    входов. И те, и другие данные (данные, полученные на выходе имитационной модели и данные, полученные в результате эксперимента с реальной системой) — статистические. Поэтому применяют методы статистической
    теории оценивания и проверки гипотез.
    Используя соответствующий статистический критерий для двух выборок, мы можем проверить статистические гипотезы (Н
    0
    ) о том, что выборки выходов системы и модели являются выборками из различных совокупностей или (Н
    1
    ), что они "практически" принадлежат одной совокупности.
    Могут быть рекомендованы два основных подхода к оценке адекватности:
    1 способ: по средним значениям откликов модели и системы.
    2 способ: по дисперсиям отклонений откликов модели от среднего
    значения откликов систем.
    А если не существует реальной системы (что характерно для задач проектирования, прогнозирования)? Проверку адекватности выполнить в этом случае не удается, поскольку нет реального объекта. Для целей исследования модели иногда проводят специальные испытания (например, так поступают при военных исследованиях). Это позволяет убедиться в точности модели, полезности ее на практике, несмотря на сложность и дороговизну проводимых испытаний.

    Могут использоваться и другие подходы к проведению валидации имитационной модели [56], кроме статистических сравнений между откликами реальной системы и модели. В отдельных случаях полезна валидация внешнего представления, когда проверяется насколько модель выглядит адекватной с точки зрения специалистов, которые с ней будут работать, так называемый тест Тьюринга (установление экспертами различий между поведением модели и реальной системы). В процессе валидации требуется постоянный контакт с заказчиком модели, дискуссии с экспертами по системе. Рекомендуется также проводить эмпирическое тестирование допущений модели, в ходе которого может осуществляться графическое представление данных, проверка гипотез о распределениях, анализ чувствительности и др. Важным инструментом валидации имитационной модели является графическое представление промежуточных результатов и выходных данных, а также анимация процесса моделирования.
    Наиболее эффективными являются такие представления данных, как гистограммы, временные графики отдельных переменных за весь период моделирования, графики взаимозависимости, круговые и линейчатые диаграммы. Методика применения статистических технологий зависит от доступности данных по реальной системе.
    Верификация имитационной модели
    Верификация модели — есть доказательство утверждений соответствия алгоритма ее функционирования замыслу моделирования и своему назначению. На этапе верификации устанавливается верность логической
    структуры модели, реализуется комплексная отладка с использованием средств трассировки, ручной имитации, в ходе которой проверяется правильность реализации моделирующего алгоритма.
    Комплексные процедуры верификации включают неформальные и формальные исследования программы-имитатора. Неформальные процедуры могут состоять из серии проверок следующего типа: проверка преобразования информации от входа к выходу; трассировка модели на реальном потоке данных (при заданных G и X):
    X изменяется по всему диапазону значений контролируется Y; o можно посмотреть, не будет ли модель давать абсурдные ответы, если ее параметры будут принимать предельные значения; o
    "проверка на ожидаемость", когда в модели заменяют стохастические элементы на детерминированные и др.
    Полезным при решении указанных задач могут быть также следующие приёмы [56]: обязательное масштабирование временных параметров в зависимости от выбранного шага моделирования (валидация данных); валидация по наступлению "событий" в модели и сравнение (если возможно) с реальной системой; тестирование модели для критических значении и при наступлении редких событий;
    фиксирование значений для некоторых входных параметров с последующим сравнением выходных результатов с заранее известными данными; вариация значениями входных и внутренних параметров модели с последующим сравнительным анализом поведения исследуемой системы; реализация повторных прогонов модели с неизменными значениями всех входных параметров; оценка фактически полученных в результате моделирования распределений случайных величин и оценок их параметров (математическое ожидание и дисперсия) с априорно заданными значениями; сравнение исследователями поведения и результатов валидируемой модели с результатами уже существующих моделей, для которых доказана достоверность; для существующей реальной исследуемой системы предсказание её будущего поведения и сравнение прогноза с реальными наблюдениями.
    Формальные процедуры связаны с проверкой исходных предположений
    (выдвинутых на основе опыта, теоретических знаний, интуитивных
    представлений, на основе имеющейся информации). Общая процедура включает: построение ряда гипотез о поведении системы и взаимодействии ее элементов; проверка гипотез с помощью статистических тестов: используют методы статистической теории оценивания и проверки гипотез (методы проверки с помощью критериев согласия (
    2
    , Колмогорова-Смирнова, Кокрена и др.), непараметрические проверки и т.д., а также дисперсионный, регрессионный, факторный, спектральный анализы).
    6.4 Валидация данных имитационной модели
    Валидация данных имитационной модели предполагает исследование
    свойств имитационной модели, в ходе которого оценивается точность,
    устойчивость, чувствительность результатов моделирования и другие свойства имитационной модели.
    Наиболее существенные процедуры исследования свойств модели: оценка точности результатов моделирования; оценка устойчивости
    результатов моделирования;
    оценка чувствительности имитационной модели.
    Получить эти оценки в ряде случаев бывает весьма сложно. Однако без успешных результатов этой работы, доверия к модели не будет, невозможно будет провести корректный проблемный анализ и сформулировать статистически значимые выводы на основе данных, полученных в результате имитации.

    Методы доказательства правильности программ
    Как известно, универсальные вычислительные машины могут быть запрограммированы для решения самых разнородных задач - в этом заключается одна из основных их особенностей, имеющая огромную практическую ценность. Один и тот же компьютер, в зависимости от того, какая программа находится у него в памяти, способен осуществлять арифметические вычисления, доказывать теоремы и редактировать тексты, управлять ходом эксперимента и создавать проект автомобиля будущего, играть в шахматы и обучать иностранному языку. Однако успешное решение всех этих и многих других задач возможно лишь при том условии, что компьютерные программы не содержат ошибок, которые способны привести к неверным результатам.
    Можно сказать, что требование отсутствия ошибок в программном обеспечении совершенно естественно и не нуждается в обосновании. Но как убедиться в том, что ошибки, в самом деле, отсутствуют? Вопрос не так прост, как может показаться на первый взгляд.
    К неформальным методам доказательства правильности программ относят отладку и тестирование, которые являются необходимой составляющей на всех этапах процесса программирования, хотя и не решают полностью проблемы правильности. Существенные ошибки легко найти, если использовать соответствующие приемы отладки (контрольные распечатки, трассировки).
    Тестирование – процесс выполнения программы с намерением найти ошибку, а не подтвердить правильность программы. Суть его сводится к следующему. Подлежащую проверке программу неоднократно запускают с теми входными данными, относительно которых результат известен заранее.
    Затем сравнивают полученный машиной результат с ожидаемым. Если во всех случаях тестирования налицо совпадение этих результатов, появляется некоторая уверенность в том, что и последующие вычисления не приведут к ошибочному итогу, т.е. что исходная программа работает правильно.
    Мы уже обсуждали понятие правильности программы с точки зрения отсутствия в ней ошибок. С интуитивной точки зрения программа будет правильной, если в результате ее выполнения будет достигнут результат, с целью получения которого и была написана программа. Сам по себе факт безаварийного завершения программы еще ни о чем не говорит: вполне возможно, что программа в действительности делает совсем не то, что было задумано. Ошибки такого рода могут возникать по различным причинам.
    В дальнейшем мы будем предполагать, что обсуждаемые программы не содержат синтаксических ошибок, поэтому при обосновании их правильности внимание будет обращаться только на содержательную сторону дела, связанную с вопросом о том, достигается ли при помощи данной программы данная конкретная цель. Целью можно считать поиск решения поставленной задачи, а программу рассматривать как способ ее решения. Программа будет правильной, если она решит сформулированную задачу.

    Метод установления правильности программ при помощи строгих средств известен как верификация программ.
    В отличие от тестирования программ, где анализируются свойства отдельных процессов выполнения программы, верификация имеет дело со свойствами программ.
    В основе метода верификации лежит предположение о том, что существует программная документация, соответствие которой требуется доказать. Документация должна содержать:
    спецификацию ввода-вывода (описание данных, не зависящих от процесса обработки);
    свойства отношений между элементами векторов состояний в выбранных точках программы;
    спецификации и свойства структурных подкомпонентов программы;
    спецификацию структур данных, зависящих от процесса обработки.
    К такому методу доказательства правильности программ относится метод индуктивных высказываний, независимо сформулированный К. Флойдом и П.
    Науром.
    Суть этого метода состоит в следующем:
    1) формулируются входное и выходное высказывания: входное высказывание описывает все необходимые входные условия для программы
    (или программного фрагмента), выходное высказывание описывает ожидаемый результат;
    2) предполагая истинным входное высказывание, строится промежуточное высказывание, которое выводится на основании семантики операторов, расположенных между входом и выходом (входным и выходным высказываниями); такое высказывание называется выведенным высказыванием;
    3) формулируется теорема (условия верификации): из выведенного высказывания следует выходное высказывание;
    4) доказывается теорема; доказательство свидетельствует о правильности программы (программного фрагмента).
    Доказательство проводится при помощи хорошо разработанных математических методов, использующих исчисление предикатов первого порядка.
    Условия верификации можно построить и в обратном направлении, т.е., считая истинным выходное высказывание, получить входное высказывание и доказывать теорему: из входного высказывания следует выведенное высказывание.
    Такой метод построения условий верификации моделирует выполнение программы в обратном направлении. Другими словами, условия верификации должны отвечать на такой вопрос: если некоторое высказывание истинно после выполнения оператора программы, то, какое высказывание должно быть истинным перед оператором?

    Построение индуктивных высказываний помогает формализовать интуитивные представления о логике программы. Оно и является самым сложным в процессе доказательства правильности программы. Это объясняется, во-первых, тем, что необходимо описать все содержательные условия, и, во-вторых, тем, что необходимо аксиоматическое описание семантики языка программирования.
    Важным шагом в процессе доказательства является доказательство завершения выполнения программы, для чего бывает достаточно неформальных рассуждений.
    Таким образом, алгоритм доказательства правильности программы методом индуктивных высказываний представляется в следующем виде:
    1) Построить структуру программы.
    2) Выписать входное и выходное высказывания.
    3) Сформулировать для всех циклов индуктивные высказывания.
    4) Составить список выделенных путей.
    5) Построить условия верификации.
    6) Доказать условие верификации.
    7) Доказать, что выполнение программы закончится.
    Этот метод сравним с обычным процессом чтения текста программы
    (метод сквозного контроля). Различие заключается в степени формализации.
    Преимущество верификации состоит в том, что процесс доказательства настолько формализуем, что он может выполняться на вычислительной машине. В этом направлении в восьмидесятые годы проводились исследования, даже создавались автоматизированные диалоговые системы, но они не нашли практического применения.
    Для автоматизированной диалоговой системы программист должен задать индуктивные высказывания на языке исчисления предикатов.
    Синтаксис и семантика языка программирования должны храниться в системе в виде аксиом на языке исчисления предикатов. Система должна определять пути в программе и строить условия верификации.
    Основной компонент доказывающей системы - это построитель условий верификации, содержащий операции манипулирования предикатами, алгоритмы интерпретации операторов программы. Вторым компонентом системы является подсистема доказательства теорем.
    Отметим трудности, связанные с методом индуктивных высказываний.
    Повторим, что трудно построить «множество основных аксиом, достаточно ограниченное для того, чтобы избежать противоречий, но достаточно богатое для того, чтобы служить отправной точкой для доказательства высказываний о программах». Вторая трудность - семантическая, заключающаяся в формировании самих высказываний, подлежащих доказательству. Если задача, для которой пишется программа, не имеет строгого математического описания, то для нее сложнее сформулировать условия верификации.
    Перечисленные методы имеют одно общее свойство: они рассматривают программу как уже существующий объект и затем доказывают ее правильность.

    Метод, который сформулировали К. Хоар и Э. Дейкстра основан на формальном выводе программ из математической постановки задачи.
    1   2   3   4   5


    написать администратору сайта