Microsoft Word petrenko rus doc

2.5 Интеграция обратной и прямой инженерии ПО

В 1999 году KVEST начинает применяться для совместной работы проектировщиков и верификаторов. Группа разработчиков в Оттаве будет разрабатывать проектную документацию и реализацию, в то время как другая группа в Москве параллельно будет разрабатывать формальные спецификации и тестовые наборы. Такая схема позволяет улучшить

качество проектной документации и создать тестовые наборы еще до того, как будет готова реализация. Это один из способов использования KVEST в процессе прямой инженерии ПО.

В 1998 году ИСП начал исследовательские работы по генерации документации на естественном языке.

Результатом этой работы стал прототип,

который демонстрировался на конференции

ZUM’98 (Берлин, сентябрь 1998)

Этот прототип на основе формальных и неформальных компонентов спецификации

синтезирует документацию в стиле UNIX

программы man. Результаты демонстрируют реальную возможность генерации документации. Актуальность документации проверяется тестами, которые генерируются из того же источника информации – спецификаций на языке RSL. Работа по расширению генерируемых форм документации и улучшению качества языка продолжается.

3. Современное состояние методов генерации тестов из формальных спецификаций

предлагается	достаточно	общая
технологическая	схема,	поскольку

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

реализация теоретического решения отдельных задач сталкивается со значительными трудностями при практическом их применении в процессе верификации индустриального ПО.

3.1 Система ITEX (Interactive TTCN Editor and eXecutor)

ITEX [29] – это система для разработки тестов для систем коммуникации. Она включает инструменты TTCN и ASN.1 для анализа и проектирования, тестовый эмулятор и поддержку для генерации полных выполнимых тестовых наборов (ВТН). Основные возможности ITEX:

^{• Тестовый набор состоит из наборов}

тестовых параметров, заданных в форме

таблиц;

^{• ITEX предоставляет набор хорошо}

интегрированных инструментов для

создания и поддержки Абстрактных Тестовых Наборов (АТН), написанных в TTCN;

^{• IETX поддерживает такие фазы}

разработки тестовых наборов как

генерацию наборов тестовых

параметров, редактирование,

верификацию и выполнение.

Этот набор инструментов хорошо интегрирован с SDT – системой проектирования SDL спецификаций.

Тестовые наборы, описанные с помощью

TTCN, могут быть преобразованы в форму, которая позволяет тестировать и реализацию на языке программирования и SDL спецификации.

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

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

Это значит, что довольно легко построить

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

3.2 ADL/ADL2

Этот подход [27] наиболее похож на работу нашей группы. Из формальных спецификаций ADL генерирует тестовые оракулы и скелетоны для построения тестовых драйверов и документации. Не очень большое, но интересное отличие состоит в том, что ADL использует не распространенный универсальный язык спецификации, а расширение языков C и C++. В рамках KV проекта на этапе создания прототипа был разработан язык SPP – аналогичное расширение целевого языка. Он документирован в KV Project Report [20]. Аналогичный способ расширения был предложен Барбарой Лисков (B.Liskov) [6]. Существуют идеи расширения Java и других объектно- ориентированных языков, направленные на разработку ПО по принципу «дизайн по контракту» (design-by-contract) [5, 27, 31]. Однако, несмотря на очевидные преимущества лучшего приема таких языков сообществом разработчиков ПО, до общей концепции еще далеко, общая нотация не выработана.

Разницу в результатах KVEST и ADL можно объяснить разницей в классах API, для которых та и другая методологии могут предоставить средства спецификации и генерации тестов. ADL предоставляет инструменты для автоматизации генерации тестов только для процедур, которые могут тестироваться независимо, с параметрами,



допускающими независимый перебор. По KVEST классификации это процедуры первого и второго классов. Это значит, что процедуры с зависимыми параметрами, процедуры, которые требуют совместного тестирования, например open/close, или процедуры, которые необходимо тестировать параллельно, например, lock/unlock, или send/receive, отбрасываются. Кроме того, ADL не распознает API класса 1, для которых возможна автоматическая генерация всего тестового набора, включая наборы тестовых параметров и тестовые оракулы.

Интересным моментом ADL является возможность генерации документации на естественном языке. Важно, что один и тот же механизм используется для документирования как целевой системы, так и тестовых наборов. Похоже, что авторы ADL сознательно не использовали технологий из области NLG (Natural Language Generation). Это понятно из практических соображений, но не значит, что современные методы генерации текста на естественном языке не могут помочь в генерации программной документации. Возможности KVEST по генерации документации реализованы в прототипной форме. Однако, в противоположность ADL KVEST использует компьютерную грамматику и словарь английского языка для анализа и генерации фрагментов на естественном языке. Это способствует уменьшению числа ошибок в тексте на естественном языке и делает текст более читабельным без дополнительной ручной правки.

Значительным преимуществом ADL2 в сравнении с KVEST является возможность спецификации и тестирования классов объектно-ориентированных языков программирования. Этот недостаток KVEST объясняется ограничениями языка спецификации RSL. Расширение KVEST для верификации объектно- ориентированного программного обеспечения планируется в 1999 году.

3.3 Использование тестовых оракулов, сгенерированных из программной документации

Работа [8] является исследовательской и не может рассматриваться как технология, пригодная для промышленного использования. Основной интерес в этом исследовании представляет анализ факторов, которые, по мнению авторов, препятствуют широкому распространению формальных спецификаций для индустриального тестирования

программного обеспечения. Авторы формулируют пять основных проблем, общее решение которых, по их мнению, при существующем положении дел невозможно. Эти пять проблем имеют много общего с набором характеристик, на которых базировалась классификация API в KVEST. Таким образом, Д.Петерс (D. Peters) и Д.Парнас (D.Parnas) и мы пришли к общему пониманию, что это ключевые проблемы в задаче автоматизации тестирования, использующего формальные спецификации. KVEST продолжает исследования в этом направлении и предлагает технологическую схему для частичной автоматизации разработки тестовых наборов для всех классов API.

3.4 Формальный вывод конечного автомата для тестирования класса

Эта работа [7] также является исследовательской. В то же время, она представляет интерес, поскольку предлагает схему тестирования группы процедур, аналогично схеме, использующейся в KVEST. В качестве языка спецификации используется Object-Z, а в качестве целевого языка программирования – C++. Задача формулируется следующим образом: построить тестовые наборы для проверки соответствия реализации и спецификации, используя формальные спецификации методов класса. Как критерий тестового покрытия используется объединение двух критериев: покрытие всех классов эквивалентности, которые представляют собой области, полученные в результате анализа разбиений и, затем, проверка результатов на границах и рядом с границами.

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

Анализ разбиений и границ производится вручную в соответствии с

предложенной авторами методологией.

Аналогичным образом строятся спецификации оракулов. Оракул, скомпилированный в C++, вызывает целевую процедуру и проверяет соответствие результатов ее работы спецификации.

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

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

спецификации переходов. Очевидно, что

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

Основное отличие KVEST от этой работы состоит в том, что KVEST не требует полного описания конечного автомата, который моделирует состояние целевой системы. Вместо этого KVEST предлагает универсальный алгоритм, который динамически поддерживает доступные состояния и переходы между парами состояний.
4. Заключение и направления дальнейшей работы
Опыт KVEST показал, что формальные методы могут использоваться в промышленной разработке ПО. Уровень сложности и размеры приложений KVEST поддерживают этот тезис.

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

^{• Пользователи языков программирования}

не владеют языками спецификаций и

главным	фактором,	сдерживающим
более	широкое	использование

формальными методами, это является

формальных методов;

^{• Методологии, технологии, CASE}

системы, поддерживающие разработку

ПО, как правило, нацелены на разработку и анализ структур (архитектур) реализаций. Этот подход

затрудняет рассмотрение собственно

функциональности ПО. Методологий, которые удачно сочетают преимущества обоих подходов: структурного и функционального, – пока нет;

^{• Статические (чисто формальные)}

методы анализа программ

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

^{• Сближение языков спецификации и}

языков программирования.

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

него язык спецификации, но и просто

новый язык программирования невозможно, легко прийти к выводу, что надо сделать переход от языка программирования к языку спецификации более незаметным. Попытки сблизить эти языки делались уже давно. Примерами таких языков служат расширение CLU [18], Alphard [19], Eiffel[27, 31], iContract [5], SDL [16], SPP [20].

Некоторые языки, например, Larch [23], предлагают делать это сближение за счет упрощения собственно спецификационной части при одновременном расширении средств для отображения формальной модели в язык реализации. Другие языки, например SDL, пользуясь спецификой проблемной области, заимствуют возможности языков программирования и за счет этого позволяют генерировать исполнимый код прямо из спецификаций.

Имеется и вполне удачный опыт встречного движения. Например, авторы ADL путем небольших добавлений расширяют C, C++, Java, и IDL. В результате для пользователя языка программирования нет никаких проблем, по крайней мере, в чтении спецификаций.

KVEST в своем перспективном развитии рассматривает как основной последний из перечисленных подходов. В настоящее

время разрабатывается версия системы,

которая в качестве инструмента специфицирования предлагает средства С++, возможно, пополненные несложным в



реализации и в понимании

“синтаксическим сахаром”.

Заметим, что концепция такого пополнения нуждается в глубокой проработке. Последствия “простых

решений” легко видеть на примере ADL.

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

^{• Синтез методов анализа и разработки}

программ, направленных на описание

функциональности и на описание структуры реализации.

Некоторые аспекты поведения ПО

плохо укладываются в рамки рассмотрения API. В качестве примера можно привести стеки телекоммуникационных протоколов и распределенные системы. Такого рода ПО хорошо описывается в форме исполнимых моделей, построенных на основе конечных автоматов, сетей Петри, специальных видов автоматов, например, типа CCS [14]. Общим недостатком таких подходов являются трудности с заданием инвариантов, охватывающие распределенные события. В частности, эта проблема проявилась при попытке обнаружения потенциальных нежелательных взаимовлияний (Feature Interaction). Одним из путей интеграции структурных и функциональных методов являются КА, расширенные описанием ограничений на переходы [4]. Этот подход близок к технике описания и тестирования групп процедур, предложенный в KVEST. Тем самым, KVEST может быть расширен соответствующими средствами для описания протоколов, распределенных систем и других видов ПО, требующих сочетания структурных и функциональных спецификаций.

^{• Интеграция статических и}

динамических методов в форвард- и

реверс-инженерии.

Из потенциально возможных приложений синтеза статических и

динамических методов разработки/анализа

выделим средства для управления уровнем абстракции и генераторы моделей для статического и/или динамического анализа поведения программ.

В качестве средств управления уровнем абстракции в KVEST разрабатывается методическая и инструментальная поддержка для “подъема” и “спуска” (“upwarding” and “downwarding”) и средства

трансформации эксплицитных спецификаций в имплицитные (в форме пост-условий). Вплоть до последнего времени эти работы выполнялись полностью вручную. Сейчас разрабатываются некоторые из запроектированных “транформаторов”.

Модели, о которых идет речь, являются обобщенным описанием сценариев использования целевой системы. Такие сценарии могут использоваться как для статического анализа (в этом и состоит идея “model checking”), так и для генерации тестовых последовательностей. В KVEST роль таких моделей играли KA в 5-ом виде тестовых драйверов. То, что такой КА разрабатывается вручную, помимо проблем связанных со стоимостью, сроками его разработки, ставит вопрос о соответствии между КА и спецификациями процедур, об отношении критериев тестового покрытия, определенных на основе спецификаций и на основе собственно КА. В настоящее время имеются работы по частичной автоматизации построения такого КА. К сожалению, в них не рассматриваются вопросы, связанные с извлечением КА из спецификаций функций с побочным эффектом. В KVEST делается попытка решить эту задачу на основе использования спецификаций скрытых (абстрактных) состояний целевых систем.

Литература

1. B.Algayres, Y.Lejeune, G.Hugonnet, and F.Hantz. The AVALON project: A VALidation Environment For SDL/ MSC Descriptions. // In: 6th SDL Forum, Darmstadt, 1993.

2. I.Burdonov, V.Ivannikov, A.Kossatchev, G.Kopytov, S.Kuznetsov. The CLOS Project:

Towards an Object-Oriented Environment for Application Development. – In Next Generation Information System Technology,

Lecture Notes in Computer Science, volume

504, Springer Verlag, 1991, pp. 422-427.

3. I.Burdonov, A.Kossatchev, A.Petrenko, S.Cheng, H.Wong. Formal Specification and

Verification of SOS Kernel. // BNR/NORTEL

Design Forum, June 1996.

4. Pansy Au and Joanne M. Atlee. Evaluation of a State-Based Model of Feature Interactions. // Proceedings of the Fourth International Workshop on Feature Interactions in Telecommunications Software Systems, June

1997, pp. 153-167.

5. R.Kramer. iContract – The Java Design by Contract Tool. // 4th conference on OO technology and systems (COOTS), 1998.

6. B.Liskov, J.Guttag. Abstraction and

Specification in Program Development. – The

MIT Press, McGraw-Hill Book Company,

1986.

7. L.Murray, D.Carrington, I.MacColl, J.McDonald, P.Strooper. Formal Derivation of

Finite State Machines for Class Testing. // Lecture Notes in Computer Science, volume

1493, pp. 42-59.

8. D.Peters, D.Parnas. Using Test Oracles

Generated from Program Documentation. // IEEE Transactions on Software Engineering,

1998, Vol. 24, N. 3, pp.161-173.

9. A.K.Petrenko. Test specification based on trace description. // Software and

Programming, New York (translated from

Programmirovanie), No. 1, Jan-Feb. 1992, pp.

26-31.

10. A.K.Petrenko. Methods of debugging and monitoring of parallel programs. // Software

and Programming, N. 3, 1994.

11. The RAISE Language Group. The RAISE Specification Language. – Prentice Hall

Europe, 1992.

12. The RAISE Language Group. The RAISE Development Method. – Prentice Hall Europe,

1995.

13. A.R.Hoare. Communicating Sequential

Processes. – Prentice Hall, 1985.

14. R.Milner. Communication and Concurrency. – Prentice Hall, 1989.

15. D. Bjorner et al eds. The Vienna Development Method: The Meta-Language. – Lecture Notes in Computer Science, volume 61, Springer

Verlag, 1978.

16. Specification and Design Language. ITU-T

recommendation Z100.

17. P.H.J. van Eijk et al eds. The Formal

Description Technique LOTOS. – North

Holland, 1989.

18. Barbara Liskov et al. CLU Reference Manual.

– Lecture Notes in Computer Science, volume

114, Springer Verlag, 1981.

19. Mary Shaw. Abstraction and Verification in

Alphard: Defining and Specifying Iteration and

Generators. // Communications of the ACM, Vol. 20, N. 8 (August 1977), pp. 553-563.

20. SPP – specification language description. –

KV project report, Nortel (Northern Telecom), May 1995.

21. C.A.R.Hoare. An axiomatic basis for

programming. // Communications of the ACM, Vol. 12, N. 10 (October 1969), pp. 576-583.

22. C.A.R.Hoare. Proof of correctness of data representations. // Acta Informatica, 1(4): 271-

281, 1972.

23. J. Guttag et al. The Larch Family of Specification Languages. // IEEE Software, Vol. 2, N. 5, pp. 24-36 (September 1985).

24. А.А.Марков. Теория алгорифмов. // Москва,

Изд-во АН СССР, 1954.

25. А.А.Ляпунов. О Логических схемах программ. Проблемы кибернетики, Москва, вып. 1, 1958.

26. Ю.И.Янов. О логических схемах алгоритмов. Проблемы кибернетики, вып. 1,

Москва, 1958.

Ресурсы сети Internet

27. http://www.eiffel.com/doc/manuals/language/i ntro/

28. http://www.fme-nl.org/fmadb088.html

29. http://www.kvatro.no/products/itex/itex.htm

30. http://www.sun.com/960201/cover/language.ht ml

31. http://www.elj.com/eiffel/intro/