ISSN 0236-235X (P)
ISSN 2311-2735 (E)

Публикационная активность

(сведения по итогам 2016 г.)
2-летний импакт-фактор РИНЦ: 0,493
2-летний импакт-фактор РИНЦ без самоцитирования: 0,389
Двухлетний импакт-фактор РИНЦ с учетом цитирования из всех
источников: 0,732
5-летний импакт-фактор РИНЦ: 0,364
5-летний импакт-фактор РИНЦ без самоцитирования: 0,303
Суммарное число цитирований журнала в РИНЦ: 5022
Пятилетний индекс Херфиндаля по цитирующим журналам: 355
Индекс Херфиндаля по организациям авторов: 499
Десятилетний индекс Хирша: 11
Место в общем рейтинге SCIENCE INDEX за 2016 год: 304
Место в рейтинге SCIENCE INDEX за 2016 год по тематике "Автоматика. Вычислительная техника": 11

Больше данных по публикационной активности нашего журнале за 2008-2016 гг. на сайте РИНЦ

Вход


Забыли пароль? / Регистрация

Добавить в закладки

Следующий номер на сайте

4
Ожидается:
16 Декабря 2017

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

Статья опубликована в выпуске журнала № 1 за 2005 год.[ 22.02.2005 ]
Аннотация:
Abstract:
Авторы: Баранов С.Н. () - , , , Летичевский А.А. () - , , , Дробинцев П.Д. () - , , , Котляров В.П. () - , ,
Ключевое слово:
Ключевое слово:
Количество просмотров: 6185
Версия для печати
Выпуск в формате PDF (1.17Мб)

Размер шрифта:       Шрифт:

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

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

Формализация спецификаций на языках MSC/SDL/UML [1-3] позволяет при определенных условиях формально проверить корректность требований и соответствие им кода.

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

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

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

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

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

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

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

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

Эта сложная производственная задача решается путем дополнения тестирования верификацией (рис. 3) – доказательством корректности (качества) продукта. В процессе формализации разработчик и тестировщик создают модели продукта – модель приложения и модель окружения, – используя языки спецификаций MSC/SDL/UML.

Подпись:  
Рис. 3. Подход с применением верификации
Разработка формальных описаний сложных систем – непростая работа. Она требует точного представления структурных и поведенческих свойств создаваемых моделей на этапе проектирования. В традиционной технологии на этом этапе, как правило, ограничиваются приближенными описаниями свойств создаваемых объектов, в полной мере используя гибкость и “уклончивость” естественного языка. Их уточнение происходит позднее на этапе программирования, в результате фазы формализации и программирования перекрываются.

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

Ручная работа над сложными моделями требует особой экспертизы в проблемной области и в детальном понимании структурных и поведенческих характеристик проектируемого объекта.

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

Каждый БП (рис. 4) соответствует некоторому пункту спецификации и тем самым заменяет формализацию сложных сценариев простой формализацией поведенческих протоколов сценариев элементарных действий, из которых строится сложный сценарий. Из множества БП автоматически генерируются сложные поведенческие сценарии или, наоборот, сложные сценарии декомпозицируются в простые.

Подпись:  
Рис. 4. Базовый протокол
Переход к постепенной формализации по пунктам спецификаций упрощает сложности формализации, связанные с человеческим фактором. Каждый проектировщик работает над формализацией “своего” хорошо знакомого модуля. Автоматическое объединение БП в корректные сценарии позволяет автоматически генерировать сложные поведенческие сценарии и проверять корректность разработанных вручную сценариев.

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

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

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

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

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

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

·    множество БП;

·    описание некорректностей, найденных в результате верификации;

·    символические трассы – сценарии, порождающие некорректные ситуации;

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

По верификационным трассам можно автоматически сгенерировать тесты, настроенные на специфическую работу с тестируемым объектом и его окружением.

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

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

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

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

3.        Удаление избыточных символических трасс: трассы разбиваются на классы эквивалентности, и из каждого класса берется только по одному представителю, что приводит к сокращению объема тестирования до 1:100.

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

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

Список литературы

1.  ITU-T z.100 (08/2002)// Telecommunication standardization sector of UTI, 202 с. – http://www.itu.int/rec/recommenda tion.asp?type=items&lang=e&parent=T-REC-Z.100-200208-I

2.  Recommendation z.120, 78 с. – http://www.itu.int/rec/re commendation.asp?type=items&lang=e&parent=T-REC-Z.120-200404-P.

3.  Telelogic TAU 2.3 UML tutorial// Telelogic, 60 с. –  https://support.telelogic.com/en/tau/download/product/product.cfm?vid=97  (the document is included in the product box of TAU 2.3).

4.  VRS User manual // Motorola, 82 с. - http://www.stc.corp. mot.com/twiki/bin/view/GSGSE/VrsDocumentation


Постоянный адрес статьи:
http://swsys.ru/index.php?page=article&id=550
Версия для печати
Выпуск в формате PDF (1.17Мб)
Статья опубликована в выпуске журнала № 1 за 2005 год.

Возможно, Вас заинтересуют следующие статьи схожих тематик: