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

  • Карпов, Андрей Николаевич
  • кандидат технических науккандидат технических наук
  • 2007, Санкт-Петербург
  • Специальность ВАК РФ05.13.11
  • Количество страниц 212
Карпов, Андрей Николаевич. Технология настраиваемой генерации тестов по формальным спецификациям для встроенных приложений и программных интерфейсов, реализованных на Java-подобных языках: дис. кандидат технических наук: 05.13.11 - Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей. Санкт-Петербург. 2007. 212 с.

Оглавление диссертации кандидат технических наук Карпов, Андрей Николаевич

ВВЕДЕНИЕ.

1. АНАЛИЗ МЕТОДОВ И СРЕДСТВ АВТОМАТИЗАЦИИ ТЕСТИРОВАНИЯ РЕАКТИВНЫХ СИСТЕМ.

1 1 современная пазовая терминология и опредт ление задачи tec iирования

12 Автоматизация т естиронания

13 анализ Java технологии для мобильных устройств

1 4 срьдства автоматизации тестирования для java программных интерфейсов и приложений

15 современные баит-код анализаторы

16 Сравнительный анализ средс! в автоматизации тестирования

17 Выводы

2 МОДЕЛЬ ВЗАИМОДЕЙСТВИЯ ТЕСТИРУЕМОЙ СИСТЕМЫ И ТЕСТОВОГО ОКРУЖЕНИЯ

2 1 Реактивная система как объект тестирования 41 2 2 Представление тестируемой сис1емы итестового окружения в виде системы временных переходов 43 2 3 Расширение системы временных переходов 47 2 4 Обобщенная формулировка модели 52 2 5 Постановка задачи на разработку технологии автоматизации тестирования

2 6 Выводы

3 КОНЦЕПЦИЯ ТЕХНОЛОГИИ АВТОМАТИЗАЦИИ ТЕСТИРОВАНИЯ.

3 1 ТЕХН0Л01 ИЧЕСКАЯ ЦЕПОЧКА И СЦЕНАРИЙ ЕЕ ИСПОЛЬЗОВАНИЯ

3 2 Модули ядра техноло! ии ав гоматизации тестирования

3 3 Структура абстрактных тестовых наборов (АТН)

3 4 Язык спецификации требовании тестируемой системы

3 5 Структура компонента сопряжения ингерфгисов

3 6 Выводы

4 КОМПЛЕКС МЕТОДИК ТЕХНОЛОГИИ АВТОМАТИЗАЦИИ ТЕСТИРОВАНИЯ.

4 1 методика разработки тестовых сценариев 78 42 Методика i енерации трасс и абстракт ных iectob 83 4 з Методика управления балансом выбора обоыценных сценариев и линейных трасс

4 4 методика создания шаклона iенерации целевого кода тестовых наборов

4 5 методика встраивания тестовых агентов

4 6 выводы но

5 ПРАКТИЧЕСКОЕ ПРИМЕНЕНИЕ РАЗРАБОТАННОЙ ТЕХНОЛОГИИ АВТОМАТИЗАЦИИ ТЕСТИРОВАНИЯ.

5 1 обобщенная cxfma применения техноло! ии 112 52 применение технологии для тестирования java API 114 5 3 применение технологии для тестирования пользовательских java приложении (MIDI тт) 118 5 4 применение технолоеии для тестирования системных java приложении (CORFI ет) 121 5 5 анализ результатов применения технологии 125 5 6 выводы

Рекомендованный список диссертаций по специальности «Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей», 05.13.11 шифр ВАК

Введение диссертации (часть автореферата) на тему «Технология настраиваемой генерации тестов по формальным спецификациям для встроенных приложений и программных интерфейсов, реализованных на Java-подобных языках»

1. Актуальность работы. В рамках технологии производства программного обеспечения (ПО) важное значение имеет организация процессов тестирования, которые во многом определяют длительность, трудоемкость цикла разработки и качество ПО.

Возрастающая сложность ПО встроенных систем требует от соответствующих инструментальных средств

- поддержки процессов тестирования, начиная с ранних этапов разработки;

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

- поддержки автоматической генерации тестов;

- организации тестирования на разных этапах разработки с обеспечением преемственности (переиспользования) уже полученных результатов и наработок,

- поддержки тестирования в реальном окружении.

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

Анализ предметной области показал, что в настоящее время широкое распространение имеют различные нотации для формальною представления требований к тестируемой системе UML, MSC, VDM-SL, Murcp, Alloy, T-VEC LF, LOTOS, Esterel, SCR, которые основаны на использовании таких известных моделей программ как сети Петри (Петри), конечные автоматы (Мили, Мура), темпоральные логики (Приора), алгебры параллельных процессов (Милнера, Хоара, Бергстры и Клоппа), традиционные системы (Д Парка) Существующий инструментарий, основанный на их использовании, TVG (от T-VFC Technologies), Rational Rose Test Realtime (от Rational), Rhapsody I estConductor (от I-Logix), UniTesK (ИСП PAH), GOTCHA-TCBEAN (от AGEDIS), MulSaw (от Ml Г), JUnit (от RoleModel Software) не удовлетворяет требованиям современного процесса производства ПО в области разработки встроенных Java программных интерфейсов и приложений, например, для мобильных телефонов, что является следствием следующих причин

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

- отсутствуют подходы платформо-независимой интеграции тестовых наборов и тестируемо! о Java приложения,

- затруднено получение эффективного настраиваемого вида целево1 о кода тестов

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

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

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

- разработка модели взаимодействия тестируемого объекта и окружения на базе аппарата реактивных систем;

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

- создание программного инструментария, обеспечивающего: 1) адаптивную генерацию целевого кода тестовых сценариев по формальному описанию; 2) встраивание тестовых агентов в тестируемую систему для сопряжения с тестовым окружением;

- проверка работоспособности предложенных методик и инструментальных средств на 8 реальных проектах для 4 моделей мобильных телефонов

Разработка и результаты решения этих задач выносятся на защиту

3. Предметом исследования являются методы и инструментарий автоматизации тестирования встроенных Java программных интерфейсов и приложений.

4. Методы исследования. В диссертации используется теория реактивных систем и конечных автоматов, аппарат формальных спецификаций, концепция абстрактных тестовых сценариев В коде применялись стандарты Message Sequence Charts (MSC), ANSI С и Java Основными критериями являлись универсальность, адаптивность и простота автономного использования разрабатываемой технологии автоматизации тестирования, а также возможность интеграции с существующими инструментальными средствами В основу исследований положен системный подход

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

6. Научные результаты и их новизна: в диссертации разработаны методологические основы технологии создания систем автоматизированного тестирования Суть этих результатов сводится к следующему.

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

2 На базе стандарта MSC создана методика формализации требований к тестируемой системе посредством применения параметризованных, инвариантных тестовых сценариев, для последующего их автоматизированного преобразования в платформо-независимое представление

3 Разработана методика генерации платформо-независимого абстрактною тестового набора в виде трасс и обобщенных сценариев для обеспечения возможности генерации целевого кода тестов на заданную платформу с помощью адаптируемого шаблона;

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

5 Разработана методика создания шаблонов адаптивнои генерации кода, позволяющая преобразовать платформо-независимое представление тестовых сценариев в платформо-зависимый целевой код тестов путем интерпретации команд абстрактного теста

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

7. Практическая значимость работы. На базе полученных научных результатов разработан комплекс программных средств, предназначенных для автоматизации тестирования Java программных интерфейсов и приложений для мобильных телефонов Программный комплекс использован в компании Motorola в 8 программных проектах в таких областях как разработка Java программных интерфейсов (JSRs) и базового приемочного (Sanity) тестирования, а также при разработке пользовательских (MIDlet) и системных

CORLIet) Java приложений Созданная технология внедрена в проекте по разработке аппарата оповещения о статусе систем контроля в ОАО "Иителтех" и проекте "Исследование применения мобильных технологий в задаче отслеживания движения поездов" в ЗАО "Северо-Западная лаборатория Лтд" Созданные комплекс методик и программные средства являются универсальными и могут быть использованы для автоматизации тестирования Java программных интерфейсов и приложений различной направленности Применение разработанной технологии автоматизации тестирования позволяет в среднем сократить время фазы тестирования в 2,5 раза.

8. Апробация работы. Основные результаты и выводы диссертации докладывались на следующих международных научных конференциях: "IEEE Russia Northwest Section, 110 Anniversary of Radio Invention confe rence" ( СПб , 2005 г.), "2006 IEEE Tenth International Symposium on Consumer Electronics" (СПб, 2006 г.), Motorola Technology Day (Spb 2005, 2006), конференциях "Технологии Microsoft в теории и практике программирования" 2002, 2004, 2005 и 2006 гг, конференциях XXIX-2001 г, ХХХ-2002г, XXXII-2004 г, XXXIII-2005 г, недели науки СПбГПУ. По материалам диссертации опубликовано В печатных работ, в том числе статья в издании из списка ВАК, где достаточно полно изложены основные результаты работы

9. Внедрение. Разработанная технолошя автоматизации тестирования внедрена в ЗАО "Северо-Западная лаборатория", НПО "Интелтех", ЗАО "Моторола" и использована при разработке учебно-методического комплекса СПбГПУ по курсу "Автоматизация тестирования Java на мобильных телефонах" на кафедре "Информационных и управляющих систем" Практическое использование представляемых на защиту результатов подтверждено соответствующими актами о внедрении.

10. Структура и объем работы. Работа содержит введение, 5 глав, заключение и 5 приложений Объем работы 145 страниц текста, количество иллюстрации 80, список использованной литературы содержит 95 наименований

Похожие диссертационные работы по специальности «Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей», 05.13.11 шифр ВАК

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

Основные результаты работы докладывались и обсуждались на семинарах ЗАО «Моторола ЗАО» (Санкт-Петербург), Учебной лаборатории Моторолы в СПбГПУ, конференции IEEE Russia Northwest Section, 110 Anniversary of Radio Invention и 2006 IEEE 1 enth International Symposium on Consumer Electronics.

По материалам диссертационной работы опубликовано 8 печатных работ, в том числе одна в издании из списка ВАК.

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

Заключение

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

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

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

1. Проведен анализ методов и средств автоматизации процесса тестирования, существующих в настоящее время на рынке программного обеспечения.

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

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

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

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

Список литературы диссертационного исследования кандидат технических наук Карпов, Андрей Николаевич, 2007 год

1. http //matlab exponcnta ru/statcflow/bookl/1 php

2. А В. Хорошилов Спецификация и естироваиие систем с асинхронным интерфейсом, ИСП РАН, (http //www citforum ru/SE/testing/asynchronousjnterface/)

3. Коул Д, 1омас Г, МакДональд М., Спарджеоп Р, Принципы тестирования ПО, ж. Открытые Системы #02/984J Брукс Ф. Как проектируются и создаются программные комплексы М . Наука, 1979

4. IEEE standard glossary of Software Engineering Terminology, IEEE Std 610.12-1990

5. Котляров ВП, Пинаев ДВ Методы и средства автоматизации тестирования программного проекта. Санкт-Петербург, 1998

6. Мансуров Н Н. Формальные методы для ускоренной разработки телекоммуникационною программного обеспечения, 1999.

7. ISO/IEC 9646-3 1995/ITU-T Х.292. 1995, Information Technology Open Systems Interconnection - Conformance Testing Methodology and Framework - Part 3: Tree and Tabular Combined Notation

8. IEEE standard glossary of Software Engineering Terminology, IEEE Std 610.12-1990

9. Майерс Г Искусство тестирования программ // М * Финансы и статистика, 1982.-176с

10. Software Testing, http //louisa levels unisa edu au/sel/testing-notes/testing htm

11. ISO/IEC 7498-1- 1994/ITU-T X200 1994, Information Technology Open Systems Interconnection - Basic Reference Model The Basic Reference Model.

12. Software Engineering Institute, Capability Maturity Model® (CMM&), 2000

13. Боэм Б Инженерное проектирование программного обеспечения М Радио и связь, 1985 -512 с

14. Moore A, Describing verification and validation a system definition, Artisan Software, 1999, www artisansw com/pdflibrary/michaels pdf

15. Бурдонов И Б Демаков А В , Косачев А С , Максимов А В , Пефсико А К , Формальные спецификации в технологиях обратной инженерии и верификации программ, 1руды Института Системного Программирования №1, 1999

16. Hoare A R, Communicating Sequential Processes Prentice Hall, 1985

17. Milner R, Communication and Concurrency Prentice Hall, 1989

18. ITU Recommendation Z 100 Specification and Description Language (SDL), 1994

19. P H J van Eijk et al eds The Formal Description Technique LOTOS -North Holland, 1989.

20. Design by Contract, http //www ddj com/documents/s=924/ddj9801d/9801dsl htm

21. Rational Rose RT www rational com/products/ rosert/index jsp

22. Rhapsody, I-Logix, http //www llogix com/

23. T elelogic Tau 4.3 SDL and TTCN Suite 4 3, www telelogic com

24. IEEE standard glossary of Software Engineering Terminology, IEEE Std 610.12-1990

25. Применение методов теории реактивных систем в задачах моделирования и качественного анализа непрерывно-дискретных систем., http /Лот imm uran ru/~dolly/voll/parijs2/parijs2 html

26. Manna Z, Pnueli A : The Temporal Logic of Reactive and Concurrent Systems Springer-Verlag, 1992

27. Clarke E M , Emerson E.A , Systla A P. Automatic verification of finite-state concurrent systems using temporal-logic specifications. ACM Transactions on Programming Languages and Systems, 8(2) p 244-263. 1986

28. Henzinger T A , Manna, Z , Pnueli A Temporal proof methodologies for real-time systems Proc 18th Annual Symposium on Principles of Programming Languages, 1991, ACM Press, p 353-366

29. Henzinger T, Nicollin X, Sifalis J, Yovine S. Symbolic Model-Checking for Real-Time Systems In Proc 7th LICS IEEE Comp Soc. Press, 1992.

30. ISO/IEC 7498-1 1994/ITU-T X200 1994, Information Technology Open Systems Interconnection - Basic Reference Model The Basic Reference Model

31. ISO/IEC 9646-1 1995/ITU-T X290 1995, Information Technology Open Systems Interconnection - Conformance Testing Methodology and Framework - Part 1" General Concepts

32. ISO/IEC 9646-2 1995/ITU-T X291 1995, Information Technology Open Systems Interconnection - Conformance Testing Methodology and Framework - Part 2- Abstract Test Suite Specification

33. ISO/IEC 9646-3. 1995/ITU-l X 292: 1995, Information Technology Open Systems Interconnection - Conformance Testing Methodology and Framework - Part 3 Tree and Tabular Combined Notation

34. Booch G Object-Oriented Analysis And Design With Application, second edition The Benjamin/Cummings Publishing Company, Inc 1994. 589 p

35. J Rumbaugh, MBlaha, WPremerlani et al. Object-oriented modeling and design Prentice-Hall. NewJenersy. 1991. 500 p

36. Carrie Kirby Public Relations Coordinator. / Embedded Systems Conference, BOSTON, September 5,2001

37. OMG Unified Modeling Language Spesification Version 1.4. 2001 http //www omg com

38. ITU Recommendation Z 120. Message Sequence Charts (MSC), 2000

39. Mauw S , Reniers M A , Operational Semantics for MSC'96. Computer Networks and ISDN systems, 1998

40. Java ME Unit tutorial, http //www.instrumentalservices com/media/java/Java ME/Java MEUnitTutorial pdf

41. RoleModel Software, http //www rolemodelsoft com

42. Parasoft Jtest. http //www parasoft com/

43. Code Conventions for the Java Programming Language, http //java.sun com/docs/codeconv

44. Rational Purify http //www lbm com/software/awdtools/purify/

45. Parasoft Jtest http //www parasoft com/

46. PTF http //www urbana ess mot com/public/ptf/index html

47. Apache Software Foundation Bcel The Bytecode Engineering Library http //jakarta apache org/bcel/, 2002

48. F Spoto The Julia Generic Static Analyser www sci umvr it/jpoto/julia, p. 5-34, 2005

49. S Cohen Jtrek Developed by Compaq, p 7-31,2001

50. Bytecode level analysis and optimization for Java classes http //cs purdue edu/s3/projects/bloat/

51. JNI Enhancements in JDK 1 2 http //java suncom/j2se/l 4 2/doLs/guide/reJ2eLtion/spec/java-teflection doc html

52. T-VEC Technologies, http //www t-vec com/Home asp

53. White, LJ, EI Cohen, "A Domain Strategy for Computer Program Testing," IEEE Transactions on Software Engineering, 6(3) 247257 May, 1980

54. Conformiq Software Ltd , http //www conformiq com/products html

55. Reactive System Inc, http //www reactive-systems com/

56. Rational Rose RT http //www rational com/products/rosert/index jsp61. leradyne, http //www/geocities com/model-based-testing/sqw97 pdf

57. PTK http //motlabs-uk baseng comm mot com/projects/ptk/

58. TestBuilder http //www testbuilder net

59. Farchi E, Hartman A , Pinter S. S. Using a Model-based Test Generator to Test for Standard Conformance, http //www research lbm com/journal/sj/411/farchi html

60. Friedman G., Hartman A , Nagin К , Shiran Т., Projected State Machine Coverage for Software Testing, http //www haifa.il lbm com/projects/verification/gtcb/papers/projectionissta pdf

61. George Mason University, httpV/www.isse gmu edu/~aynur/rsrch/Spec I est/overview html

62. MIT Software Design Group, http //mulsaw lcs mit edu/

63. Warsaw University of Technology, http //home.elka pw edu pl/~alasota/

64. BestBench Product Description http //www.diagonal com

65. ISP RAS Red Verst, http //www ispras ru/~RedVerst

66. Java 2 MicroEdition technology: http //java sun com/j2me

67. SUN Microsystems CLDC 1.1 (JSR 139) Specifications

68. Java 2 Platform, ME Connected Device Configuration/Foundation Profile Version 1 0 2

69. Bertolomieu В , Diaz M Modeling and verification of time dependent systems using time Petrinets IEEE Transactions on Software Engineering, SE-17,N 3, March 1991

70. Reed G M , Roscoe AW A Timed Model for Communicating Sequential Processes. Lecture Notes in Comp Sc 571, Springer-Verlag, 1986.

71. Moller F, Tofts C.: A Temporal Calculus of Communicating Systems Proceedings of CONCUR'90. Lecture Notes in Comp Sc 458, Springer-Verlag, 1990

72. Henzinger T A , Manna, Z , Pnueli A • Temporal proof methodologies for real-time systems Proc 18th Annual Symposium on Principles of Programming Languages, 1991, ACM Press, p 353-366

73. Baeten J С M , Bergstra J A Real time Process Algebra Formal Aspects of Computing, 3, p 142-188, 1991

74. А А Летичевский, Ю.В Капитонова, В А Волков, А А.Летичевский (мл), С Н Баранов, В П Котляров, Т Вейгарт Спецификация систем с номощыо базовых протоколов, Кибернетика и системный анализ 2, 2005

75. Борщев А, Карпов Ю , Колесов Ю Спецификация и верификация систем логического управления реального времени В сб "Системная информатика", вып 2, ИСИ СО РАН, Н-ск, 1993,40с

76. Ben-An M., Manna, Z , Pnueli A Iemporal Logic of Branching lime Proc 8th Annual Symposium on Principles of Programming Languages, 198 l,ACMPress, Williamsburg,p. 164-176

77. Alur R, Fix L, Ilen/inger I. A.: A Determinizable Class of timed Automata 6th International Conference CAV'94 Lecture Notes in Comp Sci. 818, p 1-13, 1994

78. White Paper Using UML 2 0 to Solve Systems Engineering Problems// July 2003, Andy Gurd, Senior Project Manager, Telelogic 25 c.84. Tcl/Tk www.scriptics com

79. Ben-Abdallah H , I eue S , Timing constraints in Message Sequence Chart Specification, IFIP 1997, Published by Chapman & Hall

80. Новиков ФА, Дискретная математика для программистов С-Пб * Питер, 2000.-49с,118-133с

81. Введение в метаматематику, пер. с англ , М, 1957, Мендельсон Э

82. Ю Г. Карпов Теория алгоритмов и автоматов. Санкт-Петербург 1998.

83. С В Jones Systematic Software Development using VDM. Prentice-Hall Series in Computer Science. Prentice-Hall International, 1986

84. Ю Г Карпов Верификация распределенных алгоритмов и протоколов, курс лекций.

85. Дробинцев ПД. "Интегрированная техноло1ия обеспечения качества программных продуктов с помощью верификации и тестирования", диссертация на соискание ученой степени кандидата технических наук, Санкт-Перебург, 2006

86. J М Spivey. Understanding Z, A Specification Language and its Formal Semantics Cambridge University Press, 1988

87. R Milne The semantic foundations of the RAISE specification language RAISE Report REM/11, STC Technology Ltd, 1990

88. Кружков OA, Ильин BB, Карпов АН, Зыбин КГ, Салиева M.H, Paper for the International Conference on Circuits and Systems for Communications (IEEE sponsored), MESSAGE SEQUENCE BASED TEST GENERATION VS MANUAL TEST CONSTRUCTION PROS AND CONTRAS

89. Котляров В П, Голубев А А, Карпов А Н , Paper for the International Conference 2006 IEEE Tenth International Symposium on Consumer Electronics, " IESIING AUTOMATION

90. FOR SYSTEM CORE KJAVA APPLICATIONS", Proceedings of St Petersburg IFEE Chapters, Year 2006, pp 596-599i

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