Классификация частично формализованных и формальных моделей и методов верификации программного обеспечения
жүктеу/скачать 69.65 Kb.
|
| Классификация частично формализованных и формальных моделей и методов верификации программного обеспечения
Н.А. Бурякова, А.В. Чернов РГСУ, Ростов-на-Дону Методы верификации программного обеспечения (ПО) предназначены для подтверждения фактов соответствия свойств ПО заявленным требованиям. Такие методы разнообразны и разнородны, как по своему назначению, так и по способам достижения конечного результата и включают как эмпирические, так и формальные доказательства подтверждения наличия у ПО предопределенных свойств. Понятие о верификации ПО понимается в достаточно широком смысле и на отдельных этапах жизненного цикла ПО формальные математические модели, служащие основой верификации существенно различаются. В процессе верификации ПО может достигаться и еще одна цель, состоящая в поиске некорректно реализованных свойств, невыполненных требований и сопутствующем обнаружении ошибок в ПО. В связи с этим, современные методы верификации ПО могут включать в себя методы тестирования ПО. Методы верификации ПО в целом можно разделить на структурные и функциональные, а также имеющие в своей основе формальную математическую модель, либо зависящие от квалификации лиц, принимающих решение о корректности ПО. В данной статье рассматриваются методы верификации ПО, в основном нацеленные на оценку технического состояния и работоспособности. Такие методы разделяются на группы, которые выделены на рис.1 следующим образом:
Рис.1. Общая схема классификации методов верификации ПО Частично формализованные методы верификации ПО Методы первой группы в основном, представляют собой тестирование и экспертный анализ свойств ПО и его соответствие некоторому образцу. Экспертиза (review, переводится как рецензирование, просмотр, обзор, оценка, анализ). Отличительной особенностью экспертизы при верификации ПО является наличие ряда международных стандартов [ISOISIS], причем заметим, что в нашей стране стандартов аналогичного назначения пока нет. В целом, при таком подходе к верификации ПО, наблюдается ориентированность на экспертные оценки, которые при рассмотрении различных парадигм программирования изменяются. Таким образом, их нельзя отнести к универсальным и строго формализованным. Кроме того, экспертиза применима только непосредственно к самому ПО, а не к формальным моделям, или результатам работы. В качестве видов экспертиз выделяются организационные экспертизы (management review), технические экспертизы (technical review), сквозной контроль (walkthrough), инспекции (inspection) и аудиты (audit). Различные виды экспертиз применяются к различным свойствам ПО на различных этапах проектирования. Своевременное обнаружение дефектов позволяет снизить до минимума риск некорректной работы ПО в дальнейшем. Особое место среди экспертиз занимают систематические методы анализа архитектуры ПО. Такие как: SAAM (Software Architecture Analysis Method) [3]; ATAM (Architecture Tradeoff Analysis Method) [4,5]. Методы статического анализа проводят сравнение некоторого ПО с заранее определенным шаблоном.
Динамические методы анализируют уже готовый, работающий продукт и выявляют проблемы с работоспособностью. Динамические методы верификации применяются для анализа и оценки уже результатов работы ПО, либо некоторых ее прототипов и моделей. Примерами таких методов являются тестирование ПО или имитационное тестирование, мониторинг и профилирование. Динамические методы применяются на этапе эксплуатации ПО поэтому необходимо иметь уже работающую систему или хотя бы некоторые ее работающие компоненты. Такие методы нельзя использовать на стадиях разработки и проектирования ПО, зато с их помощью можно контролировать характеристики работы системы в ее реальном окружении, которые иногда невозможно точно определить с помощью других подходов. Динамические методы позволяют обнаруживать в ПО только ошибки, проявляющиеся при его функционировании. Это обстоятельство ограничивает область их применения, например, с их помощью невозможно найти ошибки ПО, связанные с удобством сопровождения программы. Классификация видов тестирования достаточно сложна, потому что может проводиться по нескольким разным классификационным признакам. По уровню или масштабу проверяемых элементов системы тестирование делится на следующие виды:
По источникам данных, используемых для построения тестов, тестирование относится к одному из следующих видов:
По роли команды, выполняющей тестирование, оно может относиться к следующим видам:
Формальные модели верификации ПО Методы формального анализа работают с математическими моделями и абстрактными представлениями, интересующего нас ПО. Формальные методы верификации. Их отличительной особенностью является возможность проведения поиска ошибок на математической модели, без обращения к физической реализации, что в некоторых случаях довольно удобно и экономично. Для проведения анализа формальных моделей применяются специфические техники, такие как дедуктивный анализ (theorem proving), проверка моделей (model checking), абстрактная интерпретация (abstract interpretation). К сожалению, для построения таких моделей всегда необходимо исходить так же из корректности и адекватности модели ПО. Лишь после правильного построения этой модели можно автоматически проанализировать некоторые из ее свойств. Тем не менее, в большинстве случаев для эффективного анализа от специалистов потребуются глубокие знания математической логики и алгебры и некоторого набора навыков работы с этим аппаратом. Понятия логических и алгебраических исчислений довольно близки. Но для некоторой ясности и определенности можно сказать, что логика применима к утверждениям, записанным на каком либо языке, а алгебра работает с равенствами и неравенствами, записанными на языке выражений. На нынешнее время логические исчисления могут быть классифицированы следующим образом:
Другим направлением построения моделей верификации являются алгебраические модели:
В последнее время, привлекают внимание исследователей и другие изучаемые модели: 1. Исполнимые модели (или операционные, executable models) это модели, реализуя которые изучаются свойства моделируемого ПО. Каждая исполнимая модель является, по сути, программой для некоторой виртуальной машины. Примерами исполнимых моделей являются:
2. Модели промежуточного типа имеют черты как одних - логико-алгебраических, так и других - исполнимых. Стоит отметить, что часть перечисленных выше примеров может быть отнесена к обоим этим классам. Есть, однако, виды моделей, в которых логико-алгебраические и исполнимые элементы сочетаются более глубоко. Основные их виды следующие:
Чаще всего для проверки этих моделей используются методы дедуктивного анализа (theorem proving), проверки моделей (model checking) [1], согласованности, (conformance). Синтетические методы .Синтетические методы верификации сочетают техники нескольких типов - статический анализ, формальный анализ свойств ПО, тестирование. К таким методам относятся:
Представленная в статье классификация частично формализованных и формальных методов верификации отражает современное состояние исследований в данной области. Литература
жүктеу/скачать 69.65 Kb. Достарыңызбен бөлісу:
|