РАЗДЕЛ 1 ТЕОРЕТИЧЕСКИЕ АСПЕКТЫ ВЕРИФИКАЦИИ МНОГОПОТОЧНЫХ ПРИЛОЖЕНИЙ
1.1 Общие сведения о верификации и аттестации программного
обеспечения
Верификация и аттестация это некий процесс контроля и анализирован-ные, в процессе которого происходит проверка на соответствие программы указанному и заявленному регламенту, а также требованию заказчика. Процесс верификации и аттестации занимает весь процесс жизнедеятельности и функционирования программного обеспечения, появляющийся в ходе анализированною требований заказчика и заканчивающийся сверкой кода программы на этапе контроля программного обеспечения [3].
Определения верификации и аттестации совершенно различны по своей структуре, но, тем не менее, их нередко путают. Для того чтобы научиться различать их, будет определено основное отличие среди этих двух терминов. Верификация даёт ответ на вопрос, верно ли спроектирована программа, а аттестация определяет, правильно ли функционирует программное обеспечение [11].
В процессах верификации и аттестации используются две основные ме-тодики проверки и анализа систем: инспектирование ПО и тестирование ПО. Инспектирование ПО подразумевает анализ и проверку различных представлений системы, например, документации. Инспектирование происходит на всех этапах разработки программной системы. Параллельно с инспектированием может проводиться автоматический анализ исходного кода программ и соответствующих документов. Инспектирование и автоматический анализ – это статические методы верификации и аттестации, поскольку им не требуется исполняемая система. Тестирование ПО есть анализ выходных данных и рабочих характеристик программного продукта для проверки правильности работы системы. Тестирование – динамический метод верификации и аттестации, так как применяется к исполняемой системе.
Одной из важнейших проблем при проектировании и разработке про-граммного обеспечения является его верификация. Методы верификации про-граммного обеспечения предназначены для подтверждения фактов соответ-ствия конечного программного продукта заявленным требованиям, целью ве-рификации программного обеспечения является обнаружение ошибок, уязви-мостей, некорректно реализованных свойств и требований [3]. Проблема создания новой классификации методов верификации ПО является актуальной, так как позволяет рассмотреть существующие на данные момент методы верификации программного обеспечение и их программную реализацию, выявить их преимущества и недостатки.
Поэтому, в процессе верификации происходит контроль соответствия программного обеспечения заявленным системным требованиям, а в частности, исправно ли функционирует либо не функционирует программное обеспечение согласно заявленным требованиям.
Существует множество методов верификации ПО, в данной статье рас-сматривается лишь несколько методов, приведенных на Рис 1. Это, прежде всего, символьное выполнение, проверка моделей, динамические и статические методы верификации ПО. Данные методы являются наиболее эффективными на данный момент. Изучение алгоритмов и принципов работы существующих методов верификации, послужит основой для создания синтетического метода верификации на основе SMT-решателей.
Рис. 1 - Методы верификации ПО
Процесс аттестации – это наиболее обширный процесс. В ходе аттестации основная задача – показать клиенту, что программное обеспечение оправдывает ожидания заказчика. Аттестацию всегда проводят после процесса верификации.
На раннем этапе проектирования программного обеспечения весьма зна-чим процесс аттестации системного требования. В требованиях нередко попа-даются определённые погрешности, ошибки, неточности, которые могут по-служить причиной несоответствия итоговой версии требованию клиента. Про-ектировщик обязан решить данную проблему. Тем не менее, общеизвестно, что весьма трудно исправить все неточности в требованиях. Некоторые погрешности могут выявиться лишь тогда, когда программное обеспечение уже реализовано [2].
В ходе верификации и аттестации применяются пару главных методик контроля и анализирование системы: инспектирование программного обеспе-чения и дальнейшая его проверка. Инспектирование программного обеспечения является неким анализом и контролем разных элементов программы, к примеру, документов. Процесс инспектирования протекает на всех стадиях проектирования программного обеспечения. Одновременно с процессом инспектирования может происходить автоматическое анализирование кода-исходника программного обеспечения и его соответствующих составляющих [4].
Процесс контроля и проверки системы является динамическим способом хода верификации и аттестации, поскольку используется к применяемой системе.
На рисунке 2 представлена точка инспектировки и проверки системы в процессе проектирования программного обеспечения. Стрелки показывают на стадии хода проектирования, где используются указанные способы [9].
Рис. 2 - Инспектировка и проверка системы в процессе проектирования
Ход инспектировки и анализа является методом статистической верифи-кации и аттестации, поскольку в данном случае не предполагается применяемая система. Контроль и оценка программного обеспечения является анализом итоговых данных и рабочих параметров программного обеспечения для контроля верности жизнедеятельности системы.
Самой главной проблемой при проектировании и разработке программ-ного обеспечения считается его верификация. Методы верификации предназначаются для утверждения факта соответствия итогового продукта программы представленным требованиям, задачей считается нахождение ошибок, уязвимостей, некорректно осуществлённых свойств и требований заказчика [1].
Методы формального процесса верификации позволяют провести непо-средственно верификацию, основываясь на математической модели системы без обращения к её физической реализации. Техника символьного исполнения [5] часто применяется в последнее время для тестирования и анализа систем [6] и даёт возможность моделирования осуществления проектной деятельности, при которой доля входных переменных предстаёт в символьном варианте.
Один из важных этапов верификации – это проверка программного обеспечения на соответствие заявленным характеристикам качества. Далее будут представлены самые основные свойства программного обеспечения:
- корректность (соответствие программного обеспечения заявленному предназначению);
- защищённость программного обеспечения;
- стабильность программного обеспечения в случае недетерминированного действия общества (к примеру, неправильные входные данные);
- результативность применения ресурсов периода и памяти;
- адаптирование системы к определённым переменам окружения;
- транспортабельность и сочетаемость.
Наиболее значительные элементы верификации включают символьное осуществление, контроль модификаций, динамические и постоянные способы верификации. Исследование алгоритмов и основ службы существующих способов верификации, послужит базой для формирования искусственного способа верификации в основе SMT-решателей [11] – это некие методы, которые, принимают на входе вопрос разрешимости, т.е. ставят задачу, сформулированную в сфере определённой формальной системы, и требует ответа «да» либо «нет», и в итоге на выходе выдают соответствующий итоговый результат.
Методы верификации включают:
- проверку модификаций (model checking);
- закономерность заключения (logical inference);
- символьное осуществление;
- абстрактное интерпретирование;
- регулярное исследование алгоритмов и проектов;
- схемы неоспоримого программирования.
Основными разновидностями и характеристиками считаются: [12]:
- непосредственно устойчивость программного обеспечения при недетерминированной операции;
- эффективность использования временных ресурсов и ресурсов памяти.
Существует большое количество способов верификации, далее представ-лены некоторые наиболее широко используемые технологии (рисунок А.1). Классификация способов верификации системы включает формальные способы. Следует внедрить несколько определений, которые содержатся в ос-новании этой систематизации способов, [13]:
- типы способов – представление ключевых разновидностей рассматриваемого подхода;
- уровень автоматизации – устанавливает степень возможной автоматиза-ции методов верификации;
- степень многофункциональной годности – устанавливает степень ширины области вопросов, покрывающей способ верификации;
- достоверность – оценка свойства получаемых замеров, демонстрирует, насколько неточность способа (анализ отклонения измеренного значимости величины от её подлинного значения) устремляется к нулю;
- виды обнаруживаемых погрешностей;
- результативность – устанавливает эффективность способа;
- сфера применимости – устанавливает, в которой стадии исследования употребим тот либо другой способ верификации системы, кроме того, устанавливает к каким артефактам системы можно использовать способ верификации. Артефактом системы называется изучаемая часть программного кода проекта;
- период исполнения – устанавливает период, который необходим для проведения процесса верификации;
- метод достижения результата – устанавливает способы и методы, с по-мощью которых приборы наблюдения реализовывают верификацию программного обеспечения [21].
Экспертиза бывает двух видов: всеобщей либо специальной, при этом общую экспертизу можно поделить на соответствующие типы [27]:
- техническая экспертиза – установление годности программного продукта с целью применения его согласно предназначению, соотношение его спецификации и образцам;
- сквозное контролирование, исследование и анализ проекта посредством контроля артефакта, при поддержке группы специалистов, члены команды поочерёдно представляют все свойства программы, а специалисты исследуют её и записывают критические замечания, фиксируя вероятные погрешности и уязвимости;
- проверка – исследование, при котором отбор погрешностей и уязвимо-стей исполняется в согласовании с чётким планом;
- аудирование – исследование проекта, который производится людьми, не входящими в команду проекта.
Специальную экспертизу дифференцируют на соответствующие типы [20]:
- координационная экспертиза. Контролирование управлением состояния проекта;
- экспертиза удобства применения. Контролирование заказчиком и поль-зователем удобства применения разрабатываемого программного обеспечения;
- экспертиза безопасности. Контролирование экспертами согласно ин-формативной защищённости безопасности применения разрабатываемого про-граммного обеспечения;
- исследование качеств архитектуры. Исследование качеств архитектуры программного обеспечения, анализ и систематизация сценариев взаимодей-ствия программного обеспечения с пользователем.
Следовательно, наибольшим преимуществом представленной методики считается его применимость на различных этапах проектной деятельности и высокая степень покрытия классов погрешностей и уязвимости в программном обеспечении. Формальный метод верификации подразумевают под собой не некий процесс верификации математических моделей системы, а только её код-исходник.
Условия к программной модификации формулируются в форме процесса спецификации. Осуществляется проверка выполнимости условий хода спецификации на форме программного обеспечения [10].
Поэтому, в процессе верификации происходит контроль соответствия программного обеспечения заявленным системным требованиям, а в частности, исправно ли оно функционирует либо не функционирует.
Верификация и аттестация это некий процесс контроля и анализирования, в процессе которого происходит проверка на соответствие программы указанному и заявленному регламенту, а также требованию заказчика. Процесс верификации и аттестации занимает весь процесс жизнедеятельности и функционирования программного обеспечения, появляющийся в ходе анализирования требований заказчика и заканчивающийся сверкой кода программы на этапе контроля программного обеспечения [3].
Методы верификации предназначаются для утверждения факта соответ-ствия итогового продукта программы представленным требованиям, задачей верификации считается нахождение ошибок, уязвимостей, некорректно осу-ществлённых свойств и требований.
1.2 Верификация и аттестация программного обеспечения
Одной из важнейших проблем при создании разработки ПО и проектировании является его верификация. Методы верификации программного обеспечения предназначены для подтверждения фактов соответствия конечного программного продукта требованиям заказчика, основной целью верификации является обнаружение ошибок, уязвимостей, некорректно выполнение реализованных свойств и требований [3]. Проблема создания новой классификации методов верификации является актуальной темой, так как позволяет рассмотреть существующие на данные момент методы верификации программного обеспечение и их программную реализацию, выявить их преимущества и недостатки. Классификация и исследование существующих методов позволяет составить список требований и рекомендаций для дальнейшей разработки и исследования синтетического метода верификации программного обеспечение, на основе SMT – решателя. Существует методы верификации[4] программного обеспечение эмпирические (использующие экспертизу) и формальные (использующие математический аппарат для верификации программного обеспечения)динамические (проверяющие работу программной реализации с помощью непосредственного запуска), а с точки зрения уровня автоматизации на ручные, автоматизированные и автоматические.
Самым популярным способом верификации системы, считается экспертиза [20]. Экспертиза подразумевает изучение программного обеспечения, проводимое персоной (специалистом), сведущей в этой предметной сфере, специалист представляет собой, не всегда единственного творца программного продукта, но также может быть привлечена и группа лиц, со стороны, с целью объективной оценки данных программного продукта.
Экспертиза исполняется командой грамотных экспертов, при этом дан-ный способ нереально осуществить механически, таким образом, все этапы экспертизы исполняются специалистами [17]. Данный способ имеет высочайшую многофункциональную пригодность и способен разрешать неограниченный круг вопросов в области верификации системы, он также употребим к различным свойствам программного обеспечения и на каждой стадии верификации [28].
Точность экспертизы находится в зависимости от квалификации и навыка экспертов, проводящих её. Исследования свидетельствуют, что от 50 до 90% погрешностей и уязвимостей обнаруживается с помощью метода экспертизы [16]. Способ даёт возможность обнаружить почти все возможные типы погрешностей и более результативен, в том случае если экспертизу выполняют максимально опытные и грамотные эксперты.
Бесспорным превосходством, считается пригодность данного способа в каждой стадии исследования проекта. Период исполнения контроля находится в зависимости от трудности программного обеспечения и квалифицированно-сти команды экспертов.
Формальные способы можно поделить по следующим соответствующим свойствам [19]:
- дедуктивное исследование;
- контроль модификаций;
- контроль согласованности;
- теоретическое толкование.
В сравнении с экспертизой, очевидным превосходством формальных способов считается вероятность автоматизации хода верификации и возведения модификаций проектов. С целью возведения точной модификации постоянно нужен грамотный эксперт. Внешние способы отличаются значительной многофункциональной пригодностью, и значительной правильностью в том случае, когда создана соответственная внешняя форма [5].
При поддержке внешних способов обнаруживается соответствующие классы погрешностей [8]:
- неопределённые действия программы;
- неинициализированное неустойчивое отношение к NULL указателям;
- несоблюдение законов и алгоритмов пользования библиотекой;
- сценарии, приводящие к не задокументированному действию програм-мы;
- переполнение буфера;
- сценарии, препятствующие кроссплатформенности;
- погрешности, образующиеся в циклическом коде;
- погрешности форматных строчек;
- погрешности при применении обычных библиотек.
Недостатками способов внешней верификации считается, небольшая об-ласть разрешаемых вопросов верификации, а кроме того, далеко не каждый раз можно создать более совершенную и адекватную математическую модификацию, однако при этом данные методы способны результативно функционировать в промышленных планах. Этот способ используется только лишь к тем испытываемым участкам, какие возможно учитывать в формальной модификации [14].
Для возведения точных модификаций, как правило, применяется кон-струкция Крипке [9], а с целью спецификации программного обеспечения применяют темпоральную логику [10], механическое обоснование теорем, применение мультимножеств и графов, модельные комбинации (конечные автоматы, сети Петри, кратковременные автоматы, логичное определение).
Главным плюсом способа проверки модификаций, считается вероятность автоматизации течения верификации и построения модификации. Создание внешней модификации даёт возможность показать, кодировку проекта в виде рядов закономерных формулировок, что тем самым даёт возможность проконтролировать характеристики программы, выявленные в разновидности спецификации [15].
Статическое изучение программы – это исследование, производимое без практического исполнения программы (исследование, выполненное при исполнении программного обеспечения, более известное как динамичное исследование). В большинстве ситуаций разбирается определённая модификация начального программного кода. Определённая разница от динамического наблюдения данного метода в том, что статичное исследование даёт возможность рассмотреть все без исключения вероятные пути исполнения программы. Данный термин, как правило, применяется в случае, если исследование выполняется с поддержкой автоматизированных приборов [3].
