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

В статье проводится классификация методов верификации программного обеспечения (ПО), которые разнообразны по своему назначению, по способам достижения результата, по способу проверки и подтверждения у ПО предопределенных свойств.В целом производится деление на структурные и функциональные, и имеющие в своей основе формальные математические модели. Методы первой группы представляют собой тестирование и экспертный анализ свойств ПО, второй – работают с моделями и абстрактными представлениями проверяемого ПО. Отличительной особенностью экспертизы является ориентированность на экспертные оценки, поэтому их нельзя отнести к универсальным и строго формализованным. Различные виды экспертиз применяются к различным свойствам ПО на различных этапах проектирования, что позволяет своевременно определять и устранять неполадки и дефекты в работе ПО. Отличительная особенность формальных методов – удобство и экономичность, так как они проводятся без обращения к физической реализации. Для работы с формальными методами применяются специфические техники, такие как дедуктивный анализ (theorem proving), проверка моделей (model checking), абстрактная интерпретация (abstract interpretation).Так же в статье перечисляются логические и алгебраические исчисления применимые для работы с формальными моделями.Представленная в статье классификация частично формализованных и формальных методов верификации отражает современное состояние исследований в данной области.Ключевые слова:верификация, частично формализованные методы верификации ПО, формальные модели верификации ПО, экспертиза, статический анализ, динамические методы, формальные методы, синтетические методы.

05.13.18 - Математическое моделирование, численные методы и комплексы программ

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

Экспертиза (1);
Статический анализ (2);
Динамические методы (3);
Формальные методы (4);
Синтетические методы (5).

Рис.1. Общая схема классификации методов верификации ПО

Частично формализованные методы верификации ПО Методы первой группы в основном, представляют собой тестирование и экспертный анализ свойств ПО и его соответствие некоторому образцу. Экспертиза ( review , переводится как рецензирование, просмотр, обзор, оценка, анализ). Отличительной особенностью экспертизы при верификации ПО является наличие ряда международных стандартов [ISO 12207, IEEE 1074, ISO 15288, ISO 15504], причем заметим, что в нашей стране стандартов аналогичного назначения пока нет. В целом, при таком подходе к верификации ПО, наблюдается ориентированность на экспертные оценки, которые при рассмотрении различных парадигм программирования изменяются. Таким образом, их нельзя отнести к универсальным и строго формализованным. Кроме того, экспертиза применима только непосредственно к самому ПО, а не к формальным моделям, или результатам работы. В качестве видов экспертиз выделяются организационные экспертизы ( management review ), технические экспертизы ( technical review ), сквозной контроль ( walkthrough ), инспекции ( inspection ) и аудиты ( audit ). Различные виды экспертиз применяются к различным свойствам ПО на различных этапах проектирования. Своевременное обнаружение дефектов позволяет снизить до минимума риск некорректной работы ПО в дальнейшем. Особое место среди экспертиз занимают систематические методы анализа архитектуры ПО. Такие как: SAAM (Software Architecture Analysis Method) [3]; ATAM (Architecture Tradeoff Analysis Method) [4,5].Методы статического анализа проводят сравнение некоторого ПО с заранее определенным шаблоном. Статический анализ корректного построения исходного кода или поиск часто встречающихся дефектов по некоторым шаблонам хорошо автоматизирован и практически не нуждается в процедурах принятия решений человеком. Однако, круг ошибок, выявляемых статическим анализом, достаточно узок. Одним из применений шаблонов типичных ошибок является их включение в семантические правила компиляторов языков программирования.Динамические методы анализируют уже готовый, работающий продукт и выявляют проблемы с работоспособностью. Динамические методы верификации применяются для анализа и оценки уже результатов работы ПО, либо некоторых ее прототипов и моделей. Примерами таких методов являются тестирование ПО или имитационное тестирование, мониторинг и профилирование. Динамические методы применяются на этапе эксплуатации ПО поэтому необходимо иметь уже работающую систему или хотя бы некоторые ее работающие компоненты. Такие методы нельзя использовать на стадиях разработки и проектирования ПО, зато с их помощью можно контролировать характеристики работы системы в ее реальном окружении, которые иногда невозможно точно определить с помощью других подходов. Динамические методы позволяют обнаруживать в ПО только ошибки, проявляющиеся при его функционировании. Это обстоятельство ограничивает область их применения, например, с их помощью невозможно найти ошибки ПО, связанные с удобством сопровождения программы. Классификация видов тестирования достаточно сложна, потому что может проводиться по нескольким разным классификационным признакам.По уровню или масштабу проверяемых элементов системы тестирование делится на следующие виды:

Модульное или компонентное ( unit testing, component testing );
Интеграционное ( integration testing );
Системное ( system testing );
Регрессионное тестирование( regression testing ).

По источникам данных, используемых для построения тестов, тестирование относится к одному из следующих видов:

Тестирование черного ящика ( black-box testing , часто также называется тестированием соответствия, conformance testing , или функциональным тестированием, functional testing );
Тестирование белого ящика ( white-box testing , glass-box testing , также структурное тестирование, structural testing );
Тестирование серого ящика ( grey-box testing );
Тестирование, нацеленное на ошибки.

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

Внутреннее тестирование;
Независимое тестирование;
Аттестационное тестирование (приемочные испытания);
Пользовательское тестирование.

Формальные модели верификации ПО Методы формального анализа работают с математическими моделями и абстрактными представлениями, интересующего нас ПО. Формальные методы верификации. Их отличительной особенностью является возможность проведения поиска ошибок на математической модели, без обращения к физической реализации, что в некоторых случаях довольно удобно и экономично. Для проведения анализа формальных моделей применяются специфические техники, такие как дедуктивный анализ ( theorem proving ), проверка моделей ( model checking ), абстрактная интерпретация ( abstract interpretation ). К сожалению, для построения таких моделей всегда необходимо исходить так же из корректности и адекватности модели ПО. Лишь после правильного построения этой модели можно автоматически проанализировать некоторые из ее свойств. Тем не менее, в большинстве случаев для эффективного анализа от специалистов потребуются глубокие знания математической логики и алгебры и некоторого набора навыков работы с этим аппаратом.Понятия логических и алгебраических исчислений довольно близки. Но для некоторой ясности и определенности можно сказать, что логика применима к утверждениям, записанным на каком либо языке, а алгебра работает с равенствами и неравенствами, записанными на языке выражений.На нынешнее время логические исчисления могут быть классифицированы следующим образом:

Исчисление высказываний (пропозициональное исчисление, propositional calculus );
Исчисление предикатов ( predicate calculus );
Исчисления предикатов более высоких порядков( higher-order calculi );
l- исчисление ( lambda calculus );
Модальные логики;
Специальным случаем модальных логик являются временные логики ( temporal logics );
Логика дерева вычислений( Computation Tree Logic, CTL* );
m-исчисление (или исчисление неподвижных точек);
Логики явного времени ( timed temporal logics ).

Другим направлением построения моделей верификации являются алгебраические модели:

Реляционные алгебры;
Алгебраические модели абстрактных типов данных;
Алгебры процессов (исчисления процессов, process calculi ).

В последнее время, привлекают внимание исследователей и другие изучаемые модели:1. Исполнимые модели (или операционные, executable models ) это модели, реализуя которые изучаются свойства моделируемого ПО. Каждая исполнимая модель является, по сути, программой для некоторой виртуальной машины. Примерами исполнимых моделей являются:

Конечный автомат ( finite state machine, FSM );
Конечные системы помеченных переходов (или просто системы переходов, labeled transition systems, LTS );
Расширенные конечные автоматы ( extended finite state machines, EFSM );
Взаимодействующие автоматы ( communicating finite state machines, CFSM );
Иерархические автоматы ( hierarchical state machines );
Временные автоматы ( timed automata ) [2];
Гибридные автоматы ( hybrid automata );
Сети Петри ( Petri nets );
Обычный конечный автомат, его принято называть ω -автоматом;
Машины абстрактных состояний ( abstract state machines ).

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

Логики Хоара ( Hoare logics );
Динамические или программные логики ( dynamic logics, program logics );
Программные контракты ( software contracts ).

Чаще всего для проверки этих моделей используются методы дедуктивного анализа ( theorem proving ), проверки моделей ( model checking ) [1], согласованности, ( conformance ). Синтетические методы . Синтетические методы верификации сочетают техники нескольких типов - статический анализ, формальный анализ свойств ПО, тестирование. К таким методам относятся:

Тестирование на основе моделей ( model based testing );
Мониторинг формальных свойств ПО (для этой области используется два английских термина — runtime verification и passive testing );
Метод статического анализа формальных свойств;
Синтетические методы генерации структурных тестов.

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

📎📎📎📎📎📎📎📎📎📎