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

При выполнении ответственных инженерных расчетов численными методами для обоснования корректности расчетных моделей рекомендуется применять процедуру верификации и валидации модели, разработанную и предложенную ведущими мировыми организациями в области инженерных расчетов — NAFEMS (International Association for the Engineering Modelling, Analysis and Simulation Community) и ASME (American Society of Mechanical Engineers).

Исследователь-расчетчик последовательно создает расчетную схему и два вида моделей – математическую и численную. Математическая модель — математическое представление реального объекта или системы. Численная модель — программный код, реализующий представление объекта или системы в форме, приближенной к алгоритмическому описанию, включающей набор данных, характеризующих свойства системы и динамику их изменения со временем.

Применительно к данным видам моделей для проверки их адекватности используются подход верификации и валидации. Верификация проводится в области математики, а валидация – в области физики.

Лекция 1 | Программный анализ и формальные методы верификации | Наталья Шарыгина | Лекториум

Верификация

Верификация – процесс установления соответствия между численной моделью и математической моделью.

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

— Верификация программного кода для подтверждения того, что математические модели и алгоритмы численного решения систем уравнений работают корректно;

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

Верификация программного кода

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

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

Верификация вычислений

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

Занятие 20 (2022-23): Верификация цифровых устройств. История методов верификации.

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

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

Валидация

Валидация – процесс определения степени соответствия расчетной модели реальному физическому объекту в рамках области планируемого использования данной модели.

Ни один из этапов верификации не позволяет определить, насколько выбранные модели адекватны объекту исследования. Оценка соответствия численной модели реальному миру относится к задачам валидации, которая позволяет определить, насколько физические явления и законы, включенные исследователем в расчетную модель, соответствуют постановке исходной задачи и достаточны для получения требуемых решений.

Способ взаимодействия физической и математической дисциплин в процессе верификации и валидации схематически представлен на рисунке.

После выбора расчетной схемы процесс верификации и валидации расходится на две ветви. Левая ветвь относится к области математического моделирования, а правая – к области физического эксперимента.

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

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

Также крайне важно, чтобы результаты эксперимента не были бы известны расчетчикам заранее, до получения численного решения. Основная причина этого – убедиться в «предсказательных возможностях» численной модели. Если результаты эксперимента известны расчетчику заранее, что естественным будет желание «настроить» модель на конкретный результат. Это снижает уровень доверия к численной модели.

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

Источник: multiphysics.ru

Формальная спецификация и верификация. Задача о спящем парикмахере

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

Содержимое работы — 1 файл

Министерство образования и науки Российской Федерации

Магнитогорский Государственный Технический Университет им. Г.И.Носова

Кафедра вычислительной техники и прикладной математики

На тему: «Формальная спецификация и верификация.

Задача о спящем парикмахере»

Дисциплина: «Теория вычислительных процессов»

Выполнил: ст.гр. АВБ-08

Проверил: Калитаев А.Н.

Введение

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

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

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

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

Спецификация и верификация программ

Общие сведения о спецификации программы

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

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

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

Рис. 1.1. Категории языков спецификации

Универсальные языки спецификации (VDM, Z, RAISE и др.) имеют общематематическую основу и следующие виды средств:

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

В VDM и RAISE нет средств описания графовых структур, управления и параллелизма, однако имеется механизм конструирования новых структур данных.

Языки спецификации областей включают в себя следующие языки:

• спецификации доменов;
• описания взаимодействий;
• спецификации ЯП и трансляторов;
• спецификации БД и знаний;
• спецификации пакетов прикладных программ и др.

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

Язык спецификации доменов DSL (Domain Specific Language) представляет некоторое подмножество языка программирования и специально средства для описания специальных проблем домена [6.14]. Он подразделяется на внешние и внутренние языки. Внешние языки (типа Unix, XML и др.) по уровню выше языка описания приложения. Описание в нем сводится к языку DSL специальными генераторами или текстовыми редакторами, трансформирующими абстрактные понятия домена к понятиям языка DSL. Внутренние языки (С, С++), а также языки Java, Smalltalk ограничены синтаксисом и семантикой основного базового языка программирования приложений.

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

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

Языки описания средств программирования включают в себя языки, основанные на равенствах и подстановках с операционной семантикой (Лисп, Рефал); логические языки; языки операций (АPL) над последовательностями и матрицами; табличные языки; сети, графы [6.5, 6.11]. Язык логики предикатов с набором базисных функций используется для записи пред- и постусловий, инвариантов.

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

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

Продукция или правила подстановки общего вида – это λ → ρ где λ и ρ — произвольные слова в фиксированном алфавите. Нормальный алгоритм Маркова представляет собой упорядоченный набор правил, некоторые из них отмечены как завершающие. Применение правила λ → ρ к слову φ состоит в подстановке слова ρ вместо самого левого слова λ в φ. Вычисление заканчивается, когда применяется завершающее правило, состоящее в порождении одного слова.

Языки спецификации программ или универсальные языки (Z, VDM, RAISE) базируются на аппарате математической логики и теории множеств и требуют от пользователей математической подготовки при применении их в трудно формализуемых областях — описание трансляторов с ЯП, системы реального времени, где правильность и точность программ основополагающие. На формальную спецификацию, разработку аксиом и теорем требуется несоизмеримо больше времени, чем в обычных языках программирования. Кроме того, формальные спецификации программ более громоздкие и требуют много времени при прокручивании таких программ за столом и интерпретации их на редких инструментальных средствах математического доказательства.

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

Верификация программ

Верификация — это метод анализа, проверки спецификаций и правильности выполнения программ в соответствии с заданными требованиями и формальным описанием программы

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

• тесты, тестовые процедуры и входные наборы данных.
• компоненты системы и их интерфейсы (программные, технические и информационные) и взаимодействия объектов (протоколы, сообщения) в распределенных средах;
• описание доступа к БД, средства защиты от несанкционированного доступа к данным разных пользователей;
• документация на систему.

Подходы к верификации моделей

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

Верификация объектных моделей основывается на спецификации следующих элементов:

1. Базовых (простых) объектов ОМ, атрибутами которых являются данные и операции объект функции над этими данными.
2. Проверенных объектов с помощью операций (функции), используемых в качестве теорем, а все операции, которые применяются над их подобъектами, не выводят их из множества состояний объектов.
3. Верифицированных интерфейсов объектов путем доказательства правильности передачи типов и количества данных в параметрах сообщений, заданных в языке IDL. Интерфейс состоит из операций обращения к объекту, который посылает данные другому объекту через сообщение.

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

Доказательство правильности построения ОМ для некоторой ПрО состоит в следующем:

• вводятся дополнительные и/или удаляются лишние атрибуты объекта и его интерфейсов в ОМ, доказывается правильность объекта ОМ после изменений спецификации интерфейсов и взаимодействий с другими объектами;
• доказывается правильность задания типов для атрибутов объекта, т.е. подтверждения того, что выбранный тип реализует операцию, а множество его значений определено на множестве состояний этого объекта;
• доказывается правильность спецификации объектов ОМ и параметров интерфейсов, которые передаются другим объектам. Этим заканчивается заключительное доказательство проверки правильности ОМ.

Верификация модели распределенного приложения — это спецификация процессов SDL (Spesification Description Language), задание модели проверки (model-checking) и индуктивных утверждений. В нем проверки состоит в редукции системы с бесконечным числом состояний к системе с конечным числом состояний, а также в доказательстве распределенных приложений с помощью индуктивных рассуждений и системы переходов конечного автомата.

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

Источник: www.turboreferat.ru

Верификация и аттестация ПО

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

Верификация и аттестация не одно и то же, хотя их легко перепутать. Кратко различие между ними можно определить следующим образом:

— верификация отвечает на вопрос, правильно ли создана система;

— аттестация отвечает на вопрос, правильно ли работает система.

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

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

В процессах верификации и аттестации используются две основные методики проверки и анализа систем.

1. Инспектирование ПО. Анализ и проверка различных представлений системы, например документации спецификации требований, архитектурных схем или исходного кода программ. Инспектирование выполняется на всех этапах процесса разработки программной системы. Параллельно с инспектированием может выполняться автоматический анализ исходного кода программ и соответствующих документов. Инспектирование и автоматический анализ — это статические методы верификации и аттестации, поскольку им не требуется исполняемая система.
2. Тестирование ПО. Запуск исполняемого кода с тестовыми данными и исследование выходных данных и рабочих характеристик программного продукта для проверки правильности работы системы. Тестирование — это динамический метод верификации и аттестации, так как применяется к исполняемой системе.

На рис. 19.1 показано место инспектирования и тестирования в процессе разработки ПО. Стрелки указывают на те этапы процесса разработки, на которых можно применять данные методы. Согласно этой схеме, инспектирование можно выполнять на всех этапах процесса разработки системы, а тестирование — в тех случаях, когда создан прототип или исполняемая программа.

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

Рис. 19.1. Статическая и динамическая верификация и аттестация

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

На разных этапах процесса разработки ПО применяют различные виды тестирования.

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

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

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

1. Назначение ПО. Уровень достоверности соответствия зависит от того, насколько критическим является разрабатываемое программное обеспечение по тем или иным критериям. Например, уровень достоверности для систем, критическим по обеспечению безопасности, должен быть значительно выше аналогичного уровня достоверности для опытных образцов программных систем, разрабатываемых для демонстрации некоторых новых идей.
2. Ожидания пользователей. Следует с грустью отметить, что в настоящее время у большинства пользователей невысокие требования к программному обеспечению. Пользователи настолько привыкли к отказам, происходящим во время работы программ, что не удивляются этому. Они согласны терпеть сбои в работе системы, если преимущества ее использования компенсируют недостатки. Вместе с тем с начала 1990-х годов терпимость пользователей к отказам в работе программных систем постепенно снижается. В последнее время создание ненадежных систем стало практически неприемлемым, поэтому компаниям, занимающимся разработкой программных продуктов, необходимо все больше внимания уделять верификации и аттестации программного обеспечения.
3. Условия рынка программных продуктов. При оценке программной системы продавец должен знать конкурирующие системы, цену, которую покупатель согласен заплатить за систему, и назначенный срок выхода этой системы на рынок. Если у компании-разработчика несколько конкурентов, необходимо определить дату выхода системы на рынок до окончания полного тестирования и отладки, иначе первыми на рынке могут оказаться конкуренты. Если покупатели не желают приобретать ПО по высокой цене, возможно, они согласны терпеть большее количество отказов в работе системы. При определении расходов на процесс верификации и аттестации необходимо учитывать все эти факторы.

Как правило, в ходе верификации и аттестации в системе обнаруживаются ошибки. Для исправления ошибок в систему вносятся изменения. Этот процесс отладки обычно интегрирован с другими процессами верификации и аттестации. Вместе с тем тестирование (или более обобщенно — верификация и аттестация) и отладка являются разными процессами, которые имеют различные цели.

1. Верификация и аттестация — процесс обнаружения дефектов в программной системе.
2. Отладка — процесс локализации дефектов (ошибок) и их исправления.

Источник: studopedia.info