Верификация - это процесс проверки программного продукта. Место верификации среди процессов разработки программного обеспечения В методы верификации программного

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1. Верификация и аттестация – процесс обнаружения дефектов в программной системе.

2. Отладка – процесс локализации дефектов (ошибок) и их исправления (рис. 20.2).

Рис. 20.2. Процесс отладки

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

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

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

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

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

Планирование верификации и аттестации

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

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

Рис. 20.3. Планирование испытаний в процессе разработки и тестирования

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

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

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

Санкт-Петербургский

Государственный Электротехнический Университет

Кафедра МОЭВМ

по дисциплине

“Процесс разработки программных изделий”

“Верификация ПО”

Санкт-Петербург

    Цель верификации………………………………………………………………… стр. 3

    Вводные замечания……………………………………………………………….. стр. 3

    Специальные и общие целевые задачи………………………………………….. стр. 4

    Ожидаемая практика по целевым задачам……………………………………… стр. 4

SG1 Подготовка к верификации………………………………………………..... стр. 4

SG2 Проведение экспертиз (экспертного оценивания)………………………… стр. 7

SG3 Осуществление верификации……………………………………………..... стр. 9

    Приложение 1. Обзор средств автоматизации процесса верификации……….. стр. 11

    Приложение 2. Основные современные подходы к верификации…………….. стр. 12

    Список использованной литературы…………………………………………….. стр. 14

Интегрированнаяя модель совершенства и зрелости

Верификация (Уровень зрелости 3)

    Цель

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

  1. Водные замечания

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

Цель верификации программных систем - это определение и выдача отчетов об ошибках, которые могут быть допущены на этапах жизненного цикла. Основные задачи верификации:

    определение соответствия высокоуровневых требований требованиям к системе;

    учет высокоуровневых требований в архитектуре системы;

    соблюдение архитектуры и требований к ней в исходном коде;

    определение соответствия исполняемого кода требованиям к системе;

    определение средств, используемых для решения вышеперечисленных задач, которые технически корректны и достаточно полны.

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

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

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

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

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

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

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

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

Основными методами экспертного оценивания являются:

    осмотр

    сквозной структурный контроль

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

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

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

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

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

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

Метод установления правильности программ при помощи строгих средств известен как верификация программ.

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

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

спецификацию ввода-вывода (описание данных, не зависящих от процесса обработки);

свойства отношений между элементами векторов состояний в выбранных точках программы;

спецификации и свойства структурных подкомпонентов программы;

спецификацию структур данных, зависящих от процесса обработки.

К такому методу доказательства правильности программ относится метод индуктивных утверждений , независимо сформулированный К. Флойдом и П. Науром.

Суть этого метода состоит в следующем:

1) формулируются входное и выходное утверждения: входное утверждение описывает все необходимые входные условия для программы (или программного фрагмента), выходное утверждение описывает ожидаемый результат;

2) предполагая истинным входное утверждение, строится промежуточное утверждение, которое выводится на основании семантики операторов, расположенных между входом и выходом (входным и выходным утверждениями); такое утверждение называется выведенным утверждением;

3) формулируется теорема (условия верификации):

из выведенного утверждения следует выходное утверждение;

4) доказывается теорема; доказательство свидетельствует о правильности программы (программного фрагмента).

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

Условия верификации можно построить и в обратном направлении, т.е., считая истинным выходное утверждение, получить входное утверждение и доказывать теорему:

из входного утверждения следует выведенное утверждение.

Такой метод построения условий верификации моделирует выполнение программы в обратном направлении. Другими словами, условия верификации должны отвечать на такой вопрос: если некоторое утверждение истинно после выполнения оператора программы, то, какое утверждение должно быть истинным перед оператором?

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

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

Таким образом, алгоритм доказательства правильности программы методом индуктивных утверждений представляется в следующем виде:

1) Построить структуру программы.

2) Выписать входное и выходное утверждения.

3) Сформулировать для всех циклов индуктивные утверждения.

4) Составить список выделенных путей.

5) Построить условия верификации.

6) Доказать условие верификации.

7) Доказать, что выполнение программы закончится.

Этот метод сравним с обычным процессом чтения текста программы (метод сквозного контроля). Различие заключается в степени формализации.

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

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

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

Отметим трудности, связанные с методом индуктивных утверждений. Трудно построить «множество основных аксиом, достаточно ограниченное для того, чтобы избежать противоречий, но достаточно богатое для того, чтобы служить отправной точкой для доказательства утверждений о программах» (Э. Дейкстра). Вторая трудность - семантическая, заключающаяся в формировании самих утверждений, подлежащих доказательству. Если задача, для которой пишется программа, не имеет строгого математического описания, то для нее сложнее сформулировать условия верификации.

Перечисленные методы имеют одно общее свойство: они рассматривают программу как уже существующий объект и затем доказывают ее правильность.

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

Верификация и валидация (verification and validation - V& V) предназначены для анализа, проверки правильности выполнения и соответствия ПО спецификациям и требованиям заказчика. Данные методы проверки правильности программ и систем соответственно означают:

  • верификация - это проверка правильности создания системы в соответствии с ее спецификацией;
  • валидация - это проверка правильности выполнения заданных требований к системе.

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

  • планирование процедур проверки и контроля проектных решений и требований;
  • обеспечение уровня автоматизации проектирования программ CASE- средствами;
  • проверка правильности функционирования программ методами тестирования на наборах целевых тестов;
  • адаптация продукта к операционной среде и др.

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

Верификации и валидации подвергаются:

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

Иными словами, основными систематическими методами правильности программ являются:

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

Стандарты ISO/IEC 3918-99 и 12207 включают в себя процессы верификации и валидации. Для них определены цели, задачи и действия по проверке правильности создаваемого продукта (включая рабочие, промежуточные продукты) на этапах ЖЦ и соответствия его требованиям.

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

Эти процессы взаимосвязанные и определяются одним термином - «верификация и валидация» (V&V 7).

При верификации осуществляется:

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

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

Идея создания международного проекта по формальной верификации была предложена Т. Хоаром, она обсуждалась на симпозиуме по верифицированному ПО в феврале 2005 г. в Калифорнии. Затем в октябре этого же года на конференции IFIP в Цюрихе был принят международный проект сроком на 15 лег но разработке «целостного автоматизированного набора инструментов для проверки корректности ПС».

В нем сформулированы следующие основные задачи:

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

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

Многие формальные методы доказательства и верификации специфицированных программ прошли практическую апробацию. Проделана большая работа международного комитета ISO/IEC в рамках стандарта ISO/ IEC 12207:2002 по стандартизации процессов верификации и валидации ПО. Проверка корректности формальными методами разных объектов программирования является перспективной.

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

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

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

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

  • 2.1. Интеграционные свойства систем
  • 2.2. Система и ее окружение
  • 2.3. Моделирование систем
  • 2.4. Процесс создания систем
  • 2.5. Приобретение систем
  • 3. Процесс создания программного обеспечения
  • 3.1. Модели процесса создания программного обеспечения
  • 3.2. Итерационные модели разработки программного обеспечения
  • 3.3. Спецификация программного обеспечения
  • 3.4. Проектирование и реализация программного обеспечения
  • 3.5. Эволюция программных систем
  • 3.6. Автоматизированные средства разработки программного обеспечения
  • 4. Технологии производства программного обеспечения
  • Часть II. Требования к программному обеспечению
  • 5. Требования к программному обеспечению
  • 5.1. Функциональные и нефункциональные требования
  • 5.2. Пользовательские требования
  • 5.3. Системные требования
  • 5.4. Документирование системных требований
  • 6. Разработка требований
  • 6.1. Анализ осуществимости
  • 6.2. Формирование и анализ требований
  • 6.3. Аттестация требований
  • 6.4. Управление требованиям
  • 7. Матрица требований. Разработка матрицы требований
  • Часть III. Моделирование программного обеспечения
  • 8. Архитектурное проектирование
  • 8.1. Структурирование системы
  • 8.2. Модели управления
  • 8.3. Модульная декомпозиция
  • 8.4. Проблемно-зависимые архитектуры
  • 9. Архитектура распределенных систем
  • 9.1. Многопроцессорная архитектура
  • 9.2. Архитектура клиент/сервер
  • 9.3. Архитектура распределенных объектов
  • 9.4. Corba
  • 10. Объектно-ориентированное проектирование
  • 10.1. Объекты и классы объектов
  • 10.2. Процесс объектно-ориентированного проектирования
  • 10.2.1. Окружение системы и модели ее использования
  • 10.2.2. Проектирование архитектуры
  • 10.2.3. Определение объектов
  • 10.2.4. Модели архитектуры
  • 10.2.5. Специфицирование интерфейсов объектов
  • 10.3. Модификация системной архитектуры
  • 11. Проектирование систем реального времени
  • 11.1. Проектирование систем реального времени
  • 11.2. Управляющие программы
  • 11.3. Системы наблюдения и управления
  • 11.4. Системы сбора данных
  • 12. Проектирование с повторным использованием компонентов
  • 12.1. Покомпонентная разработка
  • 12.2. Семейства приложений
  • 12.3. Проектные паттерны
  • 13. Проектирование интерфейса пользователя
  • 13.1. Принципы проектирования интерфейсов пользователя
  • 13.2. Взаимодействие с пользователем
  • 13.3. Представление информации
  • 13.4. Средства поддержки пользователя
  • 13.5. Оценивание интерфейса
  • Часть IV. Технологии разработки программного обеспечения
  • 14. Жизненный цикл программного обеспечения: модели и их особенности
  • 14.1. Каскадная модель жизненного цикла
  • 14.2. Эволюционная модель жизненного цикла
  • 14.2.1. Формальная разработка систем
  • 14.2.2. Разработка программного обеспечения на основе ранее созданных компонентов
  • 14.3. Итерационные модели жизненного цикла
  • 14.3.1 Модель пошаговой разработки
  • 14.3.2 Спиральная модель разработки
  • 15. Методологические основы технологий разработки программного обеспечения
  • 16. Методы структурного анализа и проектирования программного обеспечения
  • 17. Методы объектно-ориентированного анализа и проектирования программного обеспечения. Язык моделирования uml
  • Часть V. Письменная коммуникация. Документирование проекта Программного обеспечения
  • 18. Документирование этапов разработки программного обеспечения
  • 19. Планирование проекта
  • 19.1 Уточнение содержания и состава работ
  • 19.2 Планирование управления содержанием
  • 19.3 Планирование организационной структуры
  • 19.4 Планирование управления конфигурациями
  • 19.5 Планирование управления качеством
  • 19.6 Базовое расписание проекта
  • 20. Верификация и аттестация программного обеспечения
  • 20.1. Планирование верификации и аттестации
  • 20.2. Инспектирование программных систем
  • 20.3. Автоматический статический анализ программ
  • 20.4. Метод "чистая комната"
  • 21. Тестирование программного обеспечения
  • 21.1. Тестирование дефектов
  • 21.1.1. Тестирование методом черного ящика
  • 21.1.2. Области эквивалентности
  • 21.1.3. Структурное тестирование
  • 21.1.4. Тестирование ветвей
  • 21.2. Тестирование сборки
  • 21.2.1. Нисходящее и восходящее тестирование
  • 21.2.2. Тестирование интерфейсов
  • 21.2.3. Тестирование с нагрузкой
  • 21.3. Тестирование объектно-ориентированных систем
  • 21.3.1. Тестирование классов объектов
  • 21.3.2. Интеграция объектов
  • 21.4. Инструментальные средства тестирования
  • Часть VI. Управление проектом программного обеспечения
  • 22. Управление проектами
  • 22.1. Процессы управления
  • 22.2. Планирование проекта
  • 22.3. График работ
  • 22.4. Управление рисками
  • 23. Управление персоналом
  • 23.1. Пределы мышления
  • 23.1.1. Организация человеческой памяти
  • 23.1.2. Решение задач
  • 23.1.3. Мотивация
  • 23.2. Групповая работа
  • 23.2.1. Создание команды
  • 23.2.2. Сплоченность команды
  • 23.2.3. Общение в группе
  • 23.2.4. Организация группы
  • 23.3. Подбор и сохранение персонала
  • 23.3.1. Рабочая среда
  • 23.4. Модель оценки уровня развития персонала
  • 24. Оценка стоимости программного продукта
  • 24.1. Производительность
  • 24.2. Методы оценивания
  • 24.3. Алгоритмическое моделирование стоимости
  • 24.3.1. Модель сосомо
  • 24.3.2. Алгоритмические модели стоимости в планировании проекта
  • 24.4. Продолжительность проекта и наем персонала
  • 25. Управление качеством
  • 25.1. Обеспечение качества и стандарты
  • 25.1.1. Стандарты на техническую документацию
  • 25.1.2. Качество процесса создания программного обеспечения и качество программного продукта
  • 25.2. Планирование качества
  • 25.3. Контроль качества
  • 25.3.1. Проверки качества
  • 25.4. Измерение показателей программного обеспечения
  • 25.4.1. Процесс измерения
  • 25.4.2. Показатели программного продукта
  • 26. Надежность программного обеспечения
  • 26.1. Обеспечение надежности программного обеспечения
  • 26.1.1 Критические системы
  • 26.1.2. Работоспособность и безотказность
  • 26.1.3. Безопасность
  • 26.1.4. Защищенность
  • 26.2. Аттестация безотказности
  • 26.3. Гарантии безопасности
  • 26.4. Оценивание защищенности программного обеспечения
  • 27. Совершенствование производства программного обеспечения
  • 27.1. Качество продукта и производства
  • 27.2. Анализ и моделирование производства
  • 27.2.1. Исключения в процессе создания по
  • 27.3. Измерение производственного процесса
  • 27.4. Модель оценки уровня развития
  • 27.4.1. Оценивание уровня развития
  • 27.5. Классификация процессов совершенствования
  • 20. Верификация и аттестация программного обеспечения

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    1. Верификация и аттестация – процесс обнаружения дефектов в программной системе.

    2. Отладка – процесс локализации дефектов (ошибок) и их исправления (рис. 20.2).

    Рис. 20.2. Процесс отладки

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

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

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

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

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