Формализация стандартов и тестовых наборов протоколов Интернета тема диссертации и автореферата по ВАК РФ 05.13.11, кандидат физико-математических наук Пакулин, Николай Витальевич

• Пакулин, Николай Витальевич
• кандидат физико-математических наук
• 2006

Оглавление диссертации кандидат физико-математических наук Пакулин, Николай Витальевич

Введение.

Глава 1. Анализ современного состояния методов формализации в тестировании телекоммуникационных протоколов.

1.1 Краткий обзор истории формализации спецификаций и тестов для телекоммуникационных протоколов.

1.2 Методы формальной спецификации тестов.

1.3 Методы формального описания протоколов и автоматической генерации тестовых последовательностей.

1.4 Введение в протоколы Интернета.

1.5 Постановка задачи.

Глава 2. Метод формализации стандартов протоколов Интернета.

2.1 Введение в контрактные спецификации.

2.2 Описание разработанного метода формализации стандартов протоколов Интернета.

2.3 Анализ спецификации протокола и извлечение требований.

2.4 Разработка и анализ концептуальной модели требований.

2.5 Определение формального интерфейса протокола.

2.6 Разработка пред- и постусловий для формального интерфейса протокола Интернета.

2.7 Разработка критериев покрытия.

2.8 Разработка функций реконструкции состояния.

Выводы по главе 2.

Глава 3. Метод формального задания тестов для тестирования соответствия контрактным спецификациям протоколов Интернета.

3.1 Тестирование соответствия контрактным спецификациям.

3.2 Обзор разработанного метода формального задания тестов.

3.3 Определение целей тестирования.

3.4 Разработка проекта тестового сценария.

3.5 Разработка итераторов тестовых воздействий и конструкторов конкретных тестовых воздействий.

3.6 Разработка функции определения текущего состояния сценария.

3.7 Разработка настроек тестового сценария.

3.8 Прогон тестового сценария и анализ результатов тестирования.

Выводы по главе 3.

Глава 4. Практические применения.

4.1 Проекты по тестированию IPv6 в ИСП РАН.

4.2 Тестирование MSR IPv6.

4.3 Сравнение с другими тестовыми наборами для IPv6.

4.4 Применение разработанных методов к другим видам систем.

Выводы по главе 4.

Введение диссертации (часть автореферата) на тему «Формализация стандартов и тестовых наборов протоколов Интернета»

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

Тестирование соответствия стандартам Интернета является одним из основных средств обеспечения совместимости реализаций протоколов Интернета. Подходы к тестированию реализаций этих протоколов, использующиеся на практике, основаны на ручной разработке тестовых наборов, состоящих из отдельных элементарных испытаний (test cases). Элементарные испытания представляют собой программы на специализированных языках спецификации тестов, таких как TTCN-2[54] и TTCN-3[55], или на обычных языках программирования - Perl, Java, Си. В каждом элементарном испытании реализуется последовательность тестовых воздействий на целевую систему и вынесение вердикта о корректности наблюдаемого поведения целевой системы. Для каждого элементарного испытания явно или неявно задаётся цель тестирования (test purpose)[38], которая неформально определяет группу функциональных требований к реализации протокола. Успешное или неуспешное завершение элементарного испытания трактуется следующим образом: реализация протокола корректно или некорректно реализует требования, соответствующие цели тестирования.

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

1. Высокая трудоёмкость разработки из-за низкого уровня автоматизации разработки тестовых наборов.

2. Низкая доля повторно используемых компонентов тестового набора, прежде всего процедур проверки корректности поведения и генераторов тестовых данных.

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

4. Элементарные испытания, как правило, реализуют только ограниченное число сценариев для проверки соответствующей цели тестирования. Нет подхода, который позволяет существенно повысить «глубину» тестирования и обеспечить всестороннюю проверку требований цели тестирования.

В последнее десятилетие определённый прогресс в решении указанных проблем достигнут в исследованиях в области тестирования с использованием моделей (model-based testing). Центральная идея этого направления заключается в том, что в процесс разработки тестовых наборов включаются формальные модели (спецификации) целевой системы и тестов, которые используются для автоматической генерации тестовых последовательностей, автоматической проверки корректности поведения реализации, оценки полноты тестирования и т.д.

Наибольшее распространение в телекоммуникациях имеют подходы к формальному моделированию протоколов посредством явного задания автоматных моделей, алгебр взаимодействующих процессов, систем размеченных переходов и темпоральных логик. При попытке их прямого применения к протоколам Интернета оказывается, что получающиеся модели либо дают слишком упрощенное представление о поведении протокола, либо сталкиваются с проблемой так называемого комбинаторного взрыва или взрыва состояний {state explosion) - число возможных состояний стека протоколов и переходов между ними настолько велико, что тестирование не может завершиться за приемлемое время. Для тестирования реализаций протоколов Интернета необходимо искать новые методы формального специфицирования сетевых протоколов.

До последнего времени в исследованиях по формализации протоколов и их тестированию незаслуженно мало внимания уделялось контрактным спецификациям, которые развивают известный метод проектирования программ Design-by-Contract (Проектирование на основе контрактов), разработанный Б.Майером.[120] По сути контрактные спецификации являются продолжением идей Т.Хора[121] о спецификации при помощи пред- и постусловий. При описании внешне наблюдаемого поведения системы контрактными спецификациями взаимодействие системы с окружением представляется как набор операций в некотором формальном интерфейсе. С каждой операцией формального интерфейса связаны предусловие и постусловие. Предусловие операции накладывает ограничения на ситуации, в которых эта операция может быть вызвана, постусловие операции накладывает ограничение на результаты операции и изменение состояния системы после выполнения операции.

Контрактные спецификации успешно использовались в проектах индустриального масштаба по тестированию программных интерфейсов компонентов ядра операционной системы [122,123]. Представляется перспективным расширить подход контрактных спецификаций на сетевые протоколы и применить их для формализации стандартов протоколов Интернета и разработать метод тестирования реализаций протоколов Интернета на основе формальных спецификаций протоколов.

Целью диссертационной работы являлась разработка комплекса методов автоматизации построения тестовых наборов для проверки соответствия реализаций протоколов Интернета стандартам Интернета.

Для достижения цели работы были поставлены следующие задачи:

• Разработать метод формализации стандартов протоколов, функционирующих в стеке протоколов Интернета.

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

• Провести апробацию и оценку эффективности предложенных методов на наборе протоколов Интернета, составляющих сетевой и транспортный уровни стека протоколов IPv6.

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

Практическая значимость работы. Разработанные методы спецификации протоколов Интернета и тестирования их соответствия требованиям стандартов расширяют область использования контрактных спецификаций на сложные сетевые протоколы с ограниченным временем реакции на внешние воздействия. С использованием разработанных методов и пакета программ CTesK[100], реализующего технологию автоматизированного тестирования UniTESK[124] для программного обеспечения на языке Си, были проведены исследовательские проекты по грантам Microsoft Research, РФФИ, Президиума РАН по тестированию реализаций современных сетевых протоколов. Были разработаны тестовые наборы для тестирования соответствия следующим базовым стандартам протоколов сетевого и транспортного уровней стека Интернет-протокола нового поколения IPv6:

• протокол IPv6, базовые функции оконечного узла (IETF RFC 2460, 2461,2462,2463, 2464,2710,3513)[74,78,79,77,116,91,125];

• протокол UDP в сетях IPv6 (IETF RFC 768,2460)[76,74]

• протоколы динамической смены подключения к сетям IPv6, Mobile IPv6 (IETF RFC 3775)[99];

• протоколы безопасности сетевого уровня IPsec (IETF RFC 1851, 2401,2402,2403,2404,2405,2406,2410)[80-87];

• программный интерфейс стека протоколов (IETF RFC 2292, 2553)[97,98].

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

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

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

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

Апробация работы и публикации. Результаты работы докладывались на международных конференциях «Интернет нового поколения» (Ярославль, 2002 г., там же, 2003 г., Москва, 2004 г.), Всероссийской научной конференции «Научный сервис в сети Интернет» (Новороссийск, 2003 г., 2004 г., 2005 г.), пятой международной конференции «Перспективы систем информатики» (Новосибирск, 2003 г.), на втором Международном симпозиуме по обеспечению готовности сервисов ISAS (Берлин, Германия, 2005 г.), девятой всемирной конференции по системике, кибернетике и информатике WMSCI2005 (Орландо, США, 2005), на рабочем совещании Европейского проекта G04IT (Sophia Antipolis, Франция, 2005 г.), на семинаре по теоретической информатике Ярославского Государственного Университета (Ярославль, 2006 г.).

По теме диссертации опубликованы 12 работ [1-12], раскрывающих все основные научные результаты диссертации.

Структура и объем работы. Диссертация состоит из введения, четырёх глав, заключения, списка литературы и четырёх приложений. Список литературы включает 126 названий. Основной текст диссертации (без приложений и списка литературы) занимает 130 страниц.

Заключение диссертации по теме «Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей», Пакулин, Николай Витальевич

Выводы по главе 4

1. С использованием представленных в диссертации методов разработан пакет прикладных программ - тестовый набор - для тестирования соответствия реализаций стека протоколов IPv6 набору базовых стандартов IPv6.

2. Проведенное в работе сравнение эффективности разработанного пакета прикладных программ с известными реализациями показало, что:

1. Использование разработанных методов позволяет сократить объём тестового набора 2—5 раз по сравнению с созданием тестовых наборов из элементарных испытаний.

2. Доля повторно используемых компонентов составляет 80% тестового набора, что в 1,5—5 раз превосходит аналогичный показатель тестовых наборов TAHI и ETSI.

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

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

Заключение

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

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

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

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

4. С использованием представленных в диссертации методов разработан пакет прикладных программ - тестовый набор - для тестирования соответствия реализаций стека протоколов IPv6 набору базовых стандартов IPv6.

5. Проведенное в работе сравнение эффективности разработанного пакета прикладных программ с известными реализациями показало, что:

• Использование разработанных методов позволяет сократить объём тестового набора 2—5 раз по сравнению с созданием тестовых наборов из элементарных испытаний.

• Доля повторно используемых компонентов составляет 80% тестового набора, что в 1,5—5 раз превосходит аналогичный показатель тестовых наборов TAHI и ETSI.

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

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

Список литературы диссертационного исследования кандидат физико-математических наук Пакулин, Николай Витальевич, 2006 год

1. Агамирзян И., Грошев С.Г., Хорошилов А.В., Ключников Г.В., Косачев

2. A.С., Омельченко В.А., Пакулин Н.В., Петренко А.К., Шнитман В.З. Применение формальных методов для тестирования MSR IPv6. // Интернет нового поколения. Сборник тезисов международной конференции. Ярославль, 2002. С. 29-33.

3. Ключников Г.В., Косачев А.С., Пакулин Н.В., Петренко А.К., Шнитман

4. B.З. Применение формальных методов для тестирования Mobile IPv6. // Интернет нового поколения. Сборник тезисов II международной конференции. Ярославль, 2003. С. 20-25.

5. Ключников Г.В., Косачев А.К., Пакулин Н.В., Петренко А.К., Шнитман В.З. Применение формальных методов для тестирования реализации IPv6. // Труды ИСП РАН, Том 4. М., 2003. С. 121-140.

6. Пакулин H.B. Формальная спецификация IPsec. // Интернет нового поколения. Сборник тезисов III международной конференции. М., 2004. С. 14-23.

7. Nickolay Pakoulin, Vitaly Omelchenko, Alexander Koptelov, Alexander Petrenko, Alexander Kossatchev, Chunyen Cheng. MPEG-2 IPMP Conformance Test Suite Development. AVS M1263, 2004. PDF. (http://www.avs.org.cn/FileList.asp?meetingid=15&filetype=proposal)

8. V. Kuliamin, A. Petrenko, N. Pakoulin. Extended Design-by-Contract Approach to Specification and Conformance Testing of Distributed Software. // Model Based Development and Testing, v. VII. Proc. of 9-th WMSCI, Orlando, USA, 2005. P. 65-70.

9. Ю.Ключников Г.В., Пакулин H.B., Шнитман В.З. Автоматизированное тестирование сетевых сервисов Интернет-протокола. // Научный сервис в сети ИНТЕРНЕТ. Труды Всероссийской научной конференции, М.: Изд-во МГУ, 2005. С. 168-170.

10. В. В. Кулямин, Н. В. Пакулин, О. JI. Петренко, А. А. Сортов, А. В. Хороши лов. Формализация требований на практике. Препринт. М.: ИСП РАН, 2006. 50 с.

11. Пакулин Н.В., Хорошилов А.В. Разработка формальных моделей и тестирование соответствия для систем с асинхронными интерфейсами и телекоммуникационных протоколов. // Программирование. 2006. В печати.

12. F. С. Hennie. Fault detecting experiments for sequential circuits. // Proc. 5th Ann. Symp. Switching Circuit Theory and Logical Design, 1964. C. 95110,.

13. M. П. Василевский. Диагностика ошибок в автоматах. // Кибернетика и системный анализ, т. 9, № 4, 1973. С. 98-108.

14. Т. S. Chow. Testing software design modeled by finite-state machines. // IEEE Trans, on Software Engineering, vol. 4, no. 3,1978. C. 178-187.

15. J. A. Bergstra, J. W. Klop. Algebra of Communicating Processes with Absraction. Theoretical Computer Science, 37(1), 1985. C. 77-121.

16. C. A. R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985; электронное издание, 2004. 260 с. PDF. (http://www.usingcsp.com/cspbook.pdf).

17. R. Milner. Communication and Concurrency. Prentice-Hall, 1989. 260 c.

18. N.A. Lynch, M.R. Tuttle, "An Introduction to Input/Output Automata" // CWI-Quaterly 3, 1989, P. 219-246. PDF. http://www.markrtuttle.com/papers/lt89-cwi.pdf.

19. F. Maraninchi. Operational and compositional semantics of synchronous automaton compositions. // CONCUR'92 Proceedings, LNCS 630. Springer-Verlag, 1992. PS. http://www-verimag.imag.fr/~maraninx/ArgosCONCUR92.ps.gz

20. ISO/IEC 7498. Information technology Open Systems Interconnection -Basic Reference Model. Geneva, Switzerland: ISO, 1994.

21. CCITT Recommendation Z.100. Specification and Description Language (SDL). Geneve, Switzerland: ITU, 1993. 245 c.

22. ISO/IEC 9074. Information Processing Systems — Open Systems Interconnection. Estelle — A Formal Description Technique based on an Extended State Transition Model. Geneve, Switzerland: ISO, 1989 1 я редакция,1997 2-я редакция. Отозван 06.05.1999.

23. ISO/IEC 8807. Information Processing Systems — Open Systems Interconnection. LOTOS — A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour. Geneve, Switzerland: ISO, 1989. 142 c.

24. Е. Brinksma. A theory for the derivation of tests. Proc. IFIP WG6.1 8th Intl. Symp. on Protocol Specification, Testing, and Verification, North-Holland, S. Aggarwal and K. Sabnani Ed. pp. 63-74,1988.

25. К. K. Sabnani and A. T. Dahbura. A protocol test generation procedure. Computer Networks and ISDN Systems, vol. 15, no. 4, pp. 285-297, 1988.

26. S. Fujiwara, G. v. Bochmann, F. Khendek, M. Amalou, and A. Ghedamsi. Test selection based on finite state models. IEEE Trans, on Software Eng., vol. 17, pp. 591-603, 1991.

27. G. Luo, A. Petrenko, and G. v. Bochmann. Selecting test sequences for partially specified nondeterministic finite state machines, Proceedings of the IFIP Seventh International Workshop on Protocol Test Systems, Japan, 1994, pp. 95-110.

28. H. В. Евтушенко, А. В. Лебедев, А. Ф. Петренко. Построение проверяющего множества для компоненты последовательной автоматной сети. Автоматика и телемеханика, № 8. стр. 145-153,1994.

29. J. Tretmans. A Formal Approach to Conformance Testing. PhD thesis, University of Twente, Enschede, The Netherlands, 1992.

30. J. C. Fernandez, C. Jard, T. Jeron, C. Viho. Using on-the-Fly Verification Techniques for the Generation of Test Suites // Proceedings of the 8th International Conference on Computer Aided Verification, LNCS 1102, Springer-Verlag, 1996, P. 348-359.

31. J. Tretmans. Test Generation with Inputs, Outputs, and Repetitive Quiescence. Software — Concepts and Tools, 17(3):103-120,1996.

32. D. P. Sidhu and T.-K. Leung. Formal methods for protocol testing: a detailed study. IEEE Trans. Soft. Eng., vol. 15, no. 4, pp. 413-426,1989.

33. D. Lee, M. Yannakakis. Principles and methods of testing finite state machines — a survey. Proc. IEEE, 84(8): 1090-1123,1996.

34. G. v. Bochmann, A. Petrenko. Protocol Testing: Review of Methods and Relevance for Software Testing. Proc. of ACM SIGSOFT ISSTA'1994, Software Engineering Notes, Special Issue, pp. 109—124.

35. G. Bernot. Testing against Formal Specifications: A Theoretical View. In Proc. of TAPSOFT'91, vol. 2. S. Abramsky and T. S. E. Maibaum, eds. LNCS 494, pp. 99-119, Springer-Verlag, 1991.

36. ISO/IEC 9646. Information technology Open Systems Interconnection - Conformance testing methodology and framework - Part 1: General concepts. Geneva: ISO, 1994. 46 c.

37. ITU-T Recommendation Z.500. Framework on formal methods in conformance testing. Geneve, Switzerland: ITU, 1997. 49 c.

38. S. Sadeghipour, H. Singh. Test strategies on the basis of extended finite state machines, 1998. Report FT3/SM-98-04, Daimler-Benz AG.

39. C. Bourhfir, R. Dssouli, El M. Aboulhamid and N. Rico. Automatic Executable Test Case Generation for Extended Finite State Machine Protocols. IFIP International Workshop on Testing Communicating Systems, IFIP IWTCS'97, Korea, 1997.

40. A. Duale, U. Uyar. Generation of Feasible Test Sequences for EFSM Models. Proc. IFIP Intl. Conf. Testing of Communicating Systems, pp. 91109, Sept. 2000.

41. M. Ben-Ari, A. Pnueli, Z. Manna: The Temporal Logic of Branching Time. // Acta Informatica, Volume 20, Springer Verlag, 1989, pp. 207-226.

42. A. Pnueli. The temporal semantics of concurrent programs. // Theoretical Computer Science, Vol. 13 № 1, Elsevier, 1981, pp. 45-60.

43. E.M. Clarke, E.A. Emerson: Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic. // Logic of Programs, LNCS 131, Springer-Verlag, 1981, pp. 52-71.

44. A. Church. A formulation of the simple theory of types. // J Symbolic Logic, vol.5,1940. C. 56-68.48.muCalc. D. Kozen. Results on the propositional mu-calculus. // Theoretical Computer Science, vol. 27. Netherlands: Elsevier, 1983. C. 333—354.

45. M. Gordon. HOL: A Machine Oriented Formulation of Higher Order Logic. Technical Report 68, University of Cambridge, Computer Laboratory, 1985.

46. S. Owre, J. M. Rushby, N. Shankar. PVS: A Prototype Verification System. // Proc. of 11th Int. Conf. on Automated Deduction (CADE), LNAI 607. Springer-Verlag, 1992. C. 748-752.

47. Кларк Э.М. (мл.), Грамберг О., Пелед Д. Верификация моделей программ: Model checking. Пер. с англ. Под ред. Р. Смелянского. М.: МЦНМО, 2002.416 с.

48. IS09646-2. ISO/IEC 9646. Information technology Open Systems Interconnection - Conformance testing methodology and framework - Part 2: Abstract Test Suite specification. Geneva: ISO, 1994. 33 c.

49. ISO/IEC 9646-3. Information technology Open systems interconnection -Conformance testing methodology and framework - Part 3: The Tree and

50. Tabular Combined Notation (TTCN). 1-е издание. Geneva, Switzerland: ISO, 1992.

51. ISO/IEC 9646-3. Information technology Open systems interconnection -Conformance testing methodology and framework - Part 3: The Tree and Tabular Combined Notation (TTCN). 2-е издание. Geneva, Switzerland: ISO, 1998.

52. ETSI ES 201 873-1 V3.1.1. Methods for Testing and Specification (MTS); The Testing and Test Control Notation version 3; Part 1: TTCN-3 Core Language. Sophia-Antipolis, France: ETSI, 2005. 210 c.

53. OMG formal/05-07-07. UML Testing Profile. Version 1.0. Needham, USA: Open Management Group, 2005. PDF, PostScript. (http://www.omg.org/cgi-bin/doc7formal/05-07-07).

54. L. Ebrecht, M. Schacher, C. Buhler. Test Specification in XML the most important Element for Test Automation. // ARTiSAN Benutzerforum D.A.CH, 2005.

55. Программный комплекс для разработки unit-тестов. URL. http://www.junit.org.

56. Проект TAHI по разработке тестового набора для стека протоколов IPv6. HTML. (http://www.tahi.org/).

57. CCITT Recommendation Z.120. Message Sequence Chart (MSC). Geneve, Switzerland: ITU-T General Secretariat, 1996. 77 c.

58. OMG formal/05-07-04. Unified Modeling Language: Superstructure. Version 2.0. Needham, USA: Open Management Group, 2005. 710 c.

59. ITU-T Rec. X.680 (2002) | ISO/IEC 8824-1:2002. Abstract Syntax Notation One (ASN.l): Specification of Basic Notation. Geneva, Switzerland: ITU-T, 2002; ISO, 2002. 133 c.

60. ITU-T Rec. X.681 (2002) | ISO/IEC 8824-2:2002. Abstract Syntax Notation One (ASN.l): Information Object Specification. Geneva, Switzerland: ITU-T, 2002; ISO, 2002.31 c.

61. ITU-T Rec. X.682 (2002) | ISO/IEC 8824-3:2002. Abstract Syntax Notation One (ASN.l): Constraint Specification. Geneva, Switzerland: ITU-T, 2002; ISO, 2002.10 c.

62. ITU-T Rec. X.683 (2002) | ISO/IEC 8824-4:2002. Abstract Syntax Notation One (ASN.l): Parameterization of ASN.l Specifications. Geneva, Switzerland: ITU-T, 2002; ISO, 2002. 14 c.

63. MIL-STD-188-220. Interoperability Standard for Digital Message Transfer Device Subsystems. 1993.

64. C. Jard, T. Jeron. TGV: Theory, principles and algorithms. // International Journal on Software Tools for Technology Transfer (STTT), vol. 7(4). Berlin: Springer, 2005. C. 297 315. PDF. (http://www.irisa.fr/triskell/publis/2002/Jard02c.pdf).

65. IETF RFC 2462. S. Thomson, T. Narten. IPv6 Stateless Address Autoconfiguration. December 1998. 25 c. TXT. (http://www.ietf.org/rfc/rfc2462.txt).

66. IETF RFC 1851. P. Karn, P. Metzger, W. Simpson. The ESP Triple DES Transform. September 1995. 11 c. TXT. (http://www.ietf.org/rfc/rfc 1851 .txt)

67. IETF RFC 2401. S. Kent, R. Atkinson. Security Architecture for the Internet Protocol. November 1998. 66 c. TXT. (http://www.ietf.org/rfc/rfc2401 .txt)

68. IETF RFC 2402. S. Kent, R. Atkinson. IP Authentication Header. November 1998. 22 c. TXT. (http://www.ietf.org/rfc/rfc2402.txt)

69. IETF RFC 2403. C. Madson, R. Glenn. The Use of HMAC-MD5-96 within ESP and AH. November 1998. 7 c. TXT. (http://www.ietf.org/rfc/rfc2403.txt)

70. IETF RFC 2404. C. Madson, R. Glenn. The Use of HMAC-SHA-1-96 within ESP and AH. November 1998. 7 c. TXT. (http://www.ietf.org/rfc/rfc2404.txt)

71. IETF RFC 2405. C. Madson, N. Doraswamy. The ESP DES-CBC Cipher Algorithm With Explicit IV. November 1998. 10 c. TXT. (http://www.ietf.org/rfc/rfc2405.txt)

72. IETF RFC 2406. S. Kent, R. Atkinson. IP Encapsulating Security Payload (ESP). November 1998. 22 c. TXT. (http://www.ietf.org/rfc/rfc2406.txt)

73. IETF RFC 2410. R. Glenn, S. Kent. The NULL Encryption Algorithm and Its Use With IPsec. November 1998. 6 c. TXT. (http://www.ietf.org/rfc/rfc2410.txt).

74. IETF RFC 2407. D. Piper. The Internet IP Security Domain of Interpretation for ISAKMP. IETF, 1998. 32 c. TXT. (http://www.ietf.org/rfc/rfc2407.txt)

75. IETF RFC 2408. D. Maughan, M. Schertler, M. Schneider, J. Turner. Internet Security Association and Key Management Protocol (ISAKMP). IETF, 1998. 86 c. TXT. (http://www.ietf.org/rfc/rfc2408.txt)

76. IETF RFC 2409. D. Harkins, D. Carrel. The Internet Key Exchange (IKE). IETF, 1998.41 c. TXT. (http://www.ietf.org/rfc/rfc2409.txt)

77. IETF RFC 2710. S. Deering, W. Fenner, B. Haberman. Multicast Listener Discovery (MLD) for IPv6. October 1999. 22 c. TXT. (http://www.ietf.org/rfc/rfc2710.txt).

78. Bourdonov, I., Kossatchev, A., Kuliamin, V., Petrenko, A. UniTesK Test Suite Architecture // Proceedings of FME, LNCS 2391. Springer-Verlag, 2002. P. 77-88.

79. IETF RFC 2223. J. Postel, J. Reynolds. Instructions to RFC Authors. IETF, 1997. 20 c. TXT. (http://www.ietf.org/rfc/rfc2223.txt).

80. Редактор и издатель IETF RFC. URL. http://www.rfc-editor.org/.

81. Центр назначения числовых идентификаторов для Интернета. URL. http://www.iana.org/.

82. IETF ВСР 14 | IETF RFC 2119. S. Bradner. Key words for use in RFCs to Indicate Requirement Levels. IETF, 1997. 3 c. TXT. (http://www.ietf.org/rfc/rfc2119.txt).

83. IETF RFC 2292. W. Stevens, M. Thomas. Advanced Sockets API for IPv6. February 1998.67 c. TXT. (http://www.ietf.org/rfc/rfc2292.txt).

84. IETF RFC 2553. R. Gilligan, S. Thomson, J. Bound, W. Stevens. Basic Socket Interface Extensions for IPv6. March 1999. 41 c. TXT. (http://www.ietf.org/rfc/rfc25 53 .txt).

85. IETF RFC 3775. D. Johnson, C. Perkins, J. Arkko. Mobility Support in IPv6. June 2004. TXT. (http://www.ietf.org/rfc/rfc3775 .txt).

86. CTesK 2.1: SeC Language Reference. M.: ИСП PAH, 2005. 167 c. PDF.http://vvww.unitesk.com/download/papers/ctesk/CTesK2.lLanguageRefere nce.eng.pdf).

87. IETF RFC 2579. K. McCloghrie, D. Perkins, J. Schoenwaelder. Textual Conventions for SMIv2. April 1999. TXT. (http://www.ietf.org/rfc/rfc2579.txt).

88. IETF RFC 1213. K. McCloghrie, M. T. Rose. Management Information Base for Network Management of TCP/IP-based internets: MIB-II. March 1991. TXT. (http://www.ietf.org/rfc/rfcl213.txt).

89. IETF RFC 2011 K. McCloghrie, Ed. SNMPv2 Management Information Base for the Internet Protocol using SMIv2. November 1996. TXT. (http://www.ietf.org/rfc/rfc201 l.txt).

90. IETF RFC 2465. D. Haskin, S. Onishi. Management Information Base for IP Version 6: Textual Conventions and General Group. December 1998. TXT. (http://www.ietf.org/rfc/rfc2465.txt).

91. IETF RFC 2665. J. Flick, J. Johnson. Definitions of Managed Objects for the Ethernet-like Interface Types. August 1999. TXT. (http://www.ietf.org/rfc/rfc2665.txt).

92. IETF RFC 2863. K. McCloghrie, F. Kastenholz. The Interfaces Group MIB. June 2000. TXT. (http://www.ietf.org/rfc/rfc2863.txt).

93. IETF RFC 3635. J. Flick. Definitions of Managed Objects for the Ethernet-like Interface Types. September 2003. TXT. (http://www.ietf.org/rfc/rfc3635.txt).

94. IETF RFC 4293. S. Routhier, Ed. Management Information Base for the Internet Protocol (IP). April 2006. TXT. (http://www.ietf.org/rfc/rfc4293.txt).

95. IETF RFC 4295. G. Keeni, K. Koide, K. Nagami, S. Gundavelli. Mobile IPv6 Management Information Base. April 2006. TXT. (http://www.ietf.org/rfc/rfc4295.txt).

96. И.Б. Бурдонов, A.C. Косачев, B.B. Кулямин. Неизбыточные алгоритмы обхода ориентированных графов. Детерминированный случай. // Программирование, 2003, №5.

97. И.Б. Бурдонов, А.С. Косачев, В.В. Кулямин. Неизбыточные алгоритмы обхода ориентированных графов. Недетерминированный случай. // Программирование, 2004, №1.

98. И.Б.Бурдонов, А.С.Косачев, В.В.Кулямин. Асинхронные автоматы: классификация и тестирование. // Труды ИСП РАН, том 4. М.: ИСП РАН, 1999.

99. IETF RFC 792. J. Postel. Internet Control Message Protocol. IETF, 1981. TXT. (http://www.ietf.org/rfc/rfc0792.txt).

100. IETF RFC 791. J. Postel. Internet Protocol. IETF, 1981. TXT. (http://www.ietf.org/rfc/rfc0791 .txt).

101. IETF RFC 2464. M. Crawford. Transmission of IPv6 Packets over Ethernet Networks. December 1998. 7 c. TXT. (http://www.ietf.org/rfc/rfc2464.txt).

102. ISO/IEC 13818-11. Information technology Generic coding of moving pictures and associated audio information - Part 11: IPMP on MPEG-2 systems. Geneva, Switzerland: ISO, 2004. 74 c.

103. P. Levis, S. Madden, J. Polastre, R. Szewczyk, K. Whitehouse, A. Woo, D. Gay, J. Hill, M. Welsh, E. Brewer, D. Culler. TinyOS: An operating system for wireless sensor networks. // Ambient Intelligence. Springer-Verlag, 2005. ISBN: 3-540-23867-0.

104. B. Meyer. Applying "Design by Contract". // IEEE Computer, vol. 25 №10. USA, 1992. P. 40-51.

105. C. A. R. Hoare. An axiomatic basis for computer programming. // Communications of the ACM, volume 12 №10, 1969. C. 576-580.

106. I. Bourdonov, A. Kossatchev, A. Petrenko, D. Gaiter. KVEST: Automated Generation of Test Suites from Formal Specifications. // Formal Methods 99, LNCS 1708, Springer-Verlag, 1999. C. 608-621.

107. И. Б. Бурдонов, А. В. Демаков, А. С. Косачев, А. В. Максимов, A. К. Петренко. Формальные спецификации в технологиях обратной инженерии и верификации программ. // Труды ИСП РАН, том 1. М.: ИСП РАН, 1999. С. 35-47.

108. IETF RFC 3513. R. Hinden, S. Deering. Internet Protocol Version 6 (IPv6) Addressing Architecture. April 2003. 26 c. TXT. (http://www.ietf.org/rfc/rfc3513 .txt).

109. ETSI TS 102 351. Methods for Testing and Specification (MTS); IP Testing; TTCN-3 IPv6 Test Specification Toolkit VI. 1.1. Sophia-Antipolis, France: ETSI, 2004. 29 c.