· Неопределенное поведение - неинициализированные переменные, обращение к NULL-указателям. О простейших случаях сигнализируют и компиляторы.
· Типичные сценарии, приводящие к недокументированному поведению. Стандартная библиотека Си известна большим количеством неудачных технических решений. Некоторые функции, например, gets, в принципе небезопасны.
· Переполнение буфера - когда компьютерная программа записывает данные за пределами выделенного в памяти буфера.
· Ошибки в повторяющемся коде. Многие программы исполняют несколько раз одно и то же с разными аргументами. Обычно повторяющиеся фрагменты не пишут с нуля, а размножают и исправляют.
· Ошибки форматных строк - в функциях наподобие printf могут быть ошибки с несоответствием форматной строки реальному типу параметров.
· Прочие ошибки - многие функции из стандартных библиотек не имеют побочного эффекта, и вызов их как процедур не имеет смысла.
Статический анализ состоит из нескольких этапов.
. Анализ потока управления. Идентификация и выделение циклов, их точек входа и выхода, выявление неиспользуемого кода.
. Анализ использования данных. Проверка переменных в программе. На этом этапе также можно выявить условные операторы с избыточными условиями.
. Анализ интерфейса. Проверка согласованности различных частей программы, правильности объявления процедур и их использования. Данный этап является лишним, если используется язык со строгим контролем типов.
. Анализ потоков данных. Определяются зависимости между входными и выходными переменными. Такой анализ не позволяет выявить конкретных ошибок, он дает полный список значений, используемых в программе. Следовательно, легко обнаруживается ошибочный вывод данных.
. Анализ ветвей программы. На этом этапе семантического анализа определяются все ветви программы и выделяются операторы, исполняемые в каждой ветви. Такой анализ помогает разобраться в управлении программой и позволяет проанализировать каждую ветвь отдельно.
Следует отметить, что анализ потока данных и анализ ветвей программы генерируют огромное количество информации, которая не выявляет конкретных ошибок, а представляет программу в разных аспектах. Из-за большого объема генерируемой информации эти этапы зачастую исключают из процесса анализа и используют только на ранних стадиях для обнаружения аномалий в разрабатываемой программе. Статические анализаторы полезны в тех случаях, когда используются языки программирования, подобные С, так как в них нет строгого контроля типов, и потому проверка, осуществляемая компилятором языка С, ограничена. В этом случае средствами статического анализа выявляется широкий спектр ошибок, что особенно важно при разработке критических систем.
Анализ с помощью инструментальных средств не может заменить
инспектирования, так как существуют такие типы ошибок, которые не выявляются с
помощью статического анализа. В частности, анализаторы могут обнаружить
необъявленные переменные, но неправильное присвоение они обнаружить не смогут.
В итоге статический анализ является наиболее эффективным при обнаружении ошибок
в языках, подобных С.
Software Engineering (методология «чистой комнаты») - процесс разработки программного обеспечения, предназначенный для создания программного обеспечения с сертифицируемым уровнем надёжности. Основной принцип cleanroom состоит в том, что предупреждение дефектов лучше, чем их устранение. Название Cleanroom («чистая комната») взято из электронной промышленности - так называются помещения с высокой степенью защиты от загрязнений, позволяющие предотвратить появление дефектов в процессе производства полупроводников. Впервые процесс был применён в середине-конце 80-х годов.
Основные принципы метода.
· Разработка программного обеспечения основывается на формальных методах
· Инкрементальная реализации в рамках статистического контроля качества
· Статистическое тестирование
· Формальная верификация
Наиболее важные для заказчика системные функции проверяются наибольшее
количество раз. Метод «чистой комнаты» позволяет выявить дефекты еще до
исполнения программы. Эти дефекты исправляются в процессе разработки ПО. Такой
метод наиболее эффективен при разработке систем с наивысшим уровнем надежности.
. Верификация и аттестация критических систем
Верификация и аттестация систем, критических по обеспечению безопасности, имеет много общего с тестированием любых систем с высокими требованиями надежности. Чтобы обнаружить наибольшее количество ошибок, следует применять всестороннее тестирование, а при оценке безопасности использовать статические методы тестирования. Однако вследствие чрезвычайно низкой частоты отказов, присущих многим КС, с помощью статического тестирования не всегда удается количественно оценить безотказность, так как для этого требуется очень большое число тестов. Эти тесты лишь дают основание считать ту или иную КС безопасной.
При создании КС, важен всесторонний анализ разрабатываемой системы. Имеется пять типов анализа системы, обязательных для КС:
. Анализ правильности функционирования системы
. Анализ возможности изменения и понятности системной архитектуры
. Анализ соответствия алгоритма обработки и структуры данных определенному в спецификации поведению системы
. Анализ согласованности программного кода, алгоритмов и структур данных.
. Анализ адекватности тестовых сценариев системным требованиям.
Все доказательства безопасности системы строятся на следующем
предположении: количество ошибок в системе, которые приводят к аварийным
ситуациям, намного меньше общего числа ошибок в системе. Обеспечение безопасности
должно сосредоточиться на выявлении потенциально опасных ошибок. Если
оказывается, что эти ошибки не проявляются или проявляются, но не приводят к
серьезным последствиям, то система считается надежной. Доказательства
правильности программ были предложены в качестве методов верификации ПО более
25 лет назад. Однако эти методы в основном используются только в лабораториях.
Практические проблемы построения доказательства правильности ПО настолько
сложны, что некоторые организации считают использование данных методов в
процессе разработки обычных систем неоправданно дорогим. Но, как отмечалось
ранее, для ряда КС экономически выгодно использовать доказательства
правильности системы, чем ликвидировать последствия отказов. Несмотря на то,
что для большинства систем разрабатывать доказательства правильности
нерентабельно, иногда возникает необходимость разработать доказательства
безопасности, демонстрирующие соответствие данной программы требованиям по
обеспечению безопасности. При доказательстве безопасности необязательно
доказывать соответствие программы спецификации. Необходимо только показать, что
выполнение программы не приводит к сбоям с опасными последствиями.
Заключение
В этой работе были рассмотрены вопросы верификации и аттестации ПО. Было выявлено, что это очень сложные шаги в разработке любого продукта, требующие от инженеров внимания, высочайшей квалификации, терпения, а от организации - больших вложений средств. Однако какими бы дорогостоящими не были эти процессы, экономическая выгода от их использования очевидна, ведь система без сбоев не наносит убытков. Следует помнить, что аварийные ситуации - редкие события (особенно в КС), поэтому практически невозможно смоделировать их во время тестирования системы. Было установлено, что требования безопасности никогда не исключают ненадежного поведения системы. Посредством тестирования и других процессов аттестации невозможно полностью доказать соответствие системы требованиям безопасности. Верификация и аттестация должны стать обязательными шагами в разработке ПО, пусть даже самого простого. Каждая компания, производящая ПО, должна создать штат сотрудников, которые будут заниматься только верификацией и аттестацией: это инженеры-тестеры, инженеры-испекторы и др. Организации должны учитывать экономическую обстановку на рынке ПО, желания пользователей (уже было отмечено, что требовательность пользователей к ПО растет). Если соблюдать все эти требования, то, скорее всего, наступит день, когда нас будут окружать системы, работающие без сбоев.
верификация аттестация программный
Литература
1. Соммервилл И. Инженерия программного обеспечения, 6-е издание.:
Пер. с англ. - М.: Издат. Дом. «Вильямс», 2002. - 624 с.: ил.
. МЕТОДЫ ВЕРИФИКАЦИИ ПРОГРАММНОГО ОБЕСПЕЧЕНИЯ,
В. В. Кулямин, Институт системного программирования Российской академии наук.
. Синицын С.В., Налютин Н.Ю. Верификация программного обеспечения: Курс лекций.
4. Роберт Капбертсон, Крис Браун, Гэри Кобб. БЫСТРОЕ ТЕСТИРОВАНИЕ, Издательский дом «Вильямс»
5. Компьютерные технологии в мащиностроении. <http://www.arctic-cooler.com/>
. Материалы с сайта ru.wikipedia.org