Методы построения и верификации моделей системного программного обеспечения информационно-управляющих систем тема диссертации и автореферата по ВАК РФ 05.13.12, кандидат технических наук Окулевич, Владимир Викентьевич

• Окулевич, Владимир Викентьевич
• кандидат технических наук
• 2004

Оглавление диссертации кандидат технических наук Окулевич, Владимир Викентьевич

Оглавление.

Введение.

Глава 1. Анализ методов повышения качества и надежности СПО ИУС.

1.1. Специфика СПО ИУС.

1.2. Методы повышения качества и надежности ПО ИУС.

1.2.1. Использование образцов.

1.2.2. Тестирование.

1.2.3. Повторное использование компонент.

1.2.4. Использование средств автоматической генерации кода.

1.2.5. Использование средств сквозного цикла разработки.

1.2.6. Использование систем контроля требований.

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

1.3. Построение и верификация моделей СПО ИУС.

1.3.1. Модель СПО.

1.3.2. Моделирование СПО.

1.3.3. Верификация моделей СПО.

1.3.4. Современные средства построения и верификации моделей ПО.

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

Глава 2. Методы построения и верификации моделей СПО ИУС.

2.1. Основные понятия. Классификация объектов СПО ИУС.

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

2.3. Анализ базового метода построения и верификации моделей ПО.

2.4. Метод построения и верификации моделей СПО ИУС.

2.4.1. Входные данные метода.

2.4.2. Выходные данные метода.

2.4.3. Определение и классификация требований.

2.4.4. Общая последовательность этапов метода.

2.4.5. Специфика этапов метода в зависимости от типа модели СПО.

2.4.5.1. Особенности при исследовании архитектуры СПО.

2.4.5.2. Особенности при исследовании КВМ СПО.

2.5. Особенности метода построения и верификации моделей СПО ИУС.

2.5.1. Выбор форматов для этапа построения моделей.

2.5.2. Выбор форматов отчетов верификации.

2.5.3. Дополнительные операции темпоральной логики.

2.5.4. Образцы требований с различными областями видимости.

2.5.5. Интеграция с MSDev.

2.5.6. Интеграция с системой контроля версий.

2.5.7. Классификация элементов моделей.

2.5.8. Выбор формата описания элементов моделей.

2.5.9. Таблица описания библиотеки элементов.

2.6. Библиотека элементов моделей.

Выводы.

Глава 3. Исследование характеристик методов построения и верификации моделей СПО ИУС.

3.1. Исследование базового и расширенного методов.

3.2. Исследование расширенного метода и метода на основе SMV.

Выводы.

Глава 4. Исследование и разработка моделей СПО ИУС.

4.1. Исследование архитектуры СПО (модель драйвера Windows NT).

4.2. Исследование критически важного механизма арбитража активности резервированных модулей.

Выводы.

Введение диссертации (часть автореферата) на тему «Методы построения и верификации моделей системного программного обеспечения информационно-управляющих систем»

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

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

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

В соответствии с поставленной целью в работе были решены следующие задачи:

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

2. Выявлены специфические особенности системного программного обеспечения ИУС;

3. Разработан метод построения и верификации моделей СПО ИУС, использующий в качестве основы метод G. Holzmann [83] и соответствующий инструмент SPIN;

4. Разработанный метод применен в ряде проектов, что позволило получить положительные результаты по качеству и скорости создания СПО ИУС;

5. Выполнена оценка эффективности применения предложенного метода для исследования системного программного обеспечения ИУС в сравнении с другими методами верификации моделей.

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

Научная новизна работы состоит в следующем:

1. Разработан расширенный метод построения и верификации высокоуровневых моделей СПО ИУС, базирующийся на методе G. Holzmann. Метод отличается от известных расширенным составом операторов представления требований верификации и механизмами ограничения областей видимости.

2. Определен ряд понятий: операционная среда, критически важные механизмы СПО, архитектура СПО в контексте процесса верификации, начальная модель, результат-модель, а также разработана классификация элементов СПО ИУС.

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

4. Произведена классификация элементов моделей СПО ИУС по способу активации исполнения, что позволило структурировать сведения о поведении элементов модели.

5. Показана возможность и целесообразность использования результатов моделирования в форматах расширенного метода для последующего этапа реализации СПО ИУС.

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

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

В настоящее время результаты работы используются при решении научно-практических задач разработки СПО ИУС. Объем файлов истории изменения моделей, отчетов и протоколов верификации составляет более 2.5 Мбайт. При этом осуществлена проверка более 500 требований верификации в режимах истощающей верификации, верификации со сжатием пространства состояния и вероятностной верификации.

Разработанный метод был использован при реализации СПО арбитража активности резервируемых модулей управления устройствами радиолокатора

МВРЛ-СВК, проектировании драйвера управления связевым оборудованием системы КТС "Тракт" для Windows NT 5.0 и др.

По результатам работы было сделано 10 докладов на 9 конференциях. Всего по теме диссертации выполнено 11 публикаций. Доклад на Политехническом симпозиуме «Молодые ученые - промышленности Северозападного региона» 17 декабря 2002 года был удостоен звания лучшего доклада. За активное участие в конференциях Политехнического симпозиума 20 февраля 2004 года автор работы награжден медалью «За преданность науке», удостоверение № 54.

Часть материалов диссертации вошла в курс лекций и лабораторных работ по дисциплине «Операционные системы реального времени» кафедры ВТ СПБГУИТМО.

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

Заключение диссертации по теме «Системы автоматизации проектирования (по отраслям)», Окулевич, Владимир Викентьевич

Выводы

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

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

3. Выработан ряд практических рекомендаций по применению предложенного метода, связанных с построением моделей.

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

В настоящее время в данном направлении ведется множество исследований. Представленные в работе методы и средства автоматизации процесса создания и верификации моделей СПО ИУС развивают положительно зарекомендовавшую себя методику G. Holzmann.

Основные теоретические результаты настоящей работы состоят в следующем:

1. Разработан расширенный метод построения и верификации высокоуровневых моделей СПО ИУС, базирующийся на методе G. Holzmann. Метод использует расширенный состав операторов представления требований верификации и механизмы ограничения областей видимости.

2. Определен ряд понятий: операционная среда, критически важные механизмы СПО, архитектура СПО в контексте процесса верификации, начальная модель, результат-модель, а также предложена классификация элементов СПО ИУС.

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

4. Произведена классификация элементов моделей СПО ИУС по способу активации исполнения, что позволило структурировать сведения о поведении элементов модели.

5. Показана возможность и целесообразность использования результатов моделирования в форматах расширенного метода для последующего этапа реализации СПО ИУС.

К практическим результатам относится следующее:

1. Разработан автоматизированный инструментальный комплекс построения и верификации высокоуровневых моделей СПО ИУС.

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

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

4. В рамках автоматизированного комплекса реализован интерфейс верификатора со средой MSDev, включающий возможность использования синтаксической подсветки операторов языка PROMELA. Это позволило повысить комфортность и сократить количество ошибок при разработке и исследовании модели.

Эффективность предложенного в работе расширенного метода построения и верификации моделей подтверждена проведенными экспериментами и успешным использованием в реальных проектах по разработке ПО ИУС.

Использованные сокращения

ИУС - информационно-управляющая система. ПО - программное обеспечение. СПО - системное программное обеспечение. КВМ - критически важный механизм.

Список литературы диссертационного исследования кандидат технических наук Окулевич, Владимир Викентьевич, 2004 год

1. Астапкович A.M., Востриков А.А., Гуляев A.M. Операционные системы реального времени для встраиваемых приложений // BYTE.- 2000.- № 9(25). С. 34-48.

2. Бек К. «Экстремальное программирование», «Питер»,Санкт-Петербург, 2002г.

3. Бешенков С., Ракитина Е. Моделирование и формализация. Методическое пособие: М., Лаборатория Базовых Знаний, 2002. 333 е., ил.

4. Богачев К.Ю. Операционные системы реального времени: Материалы лекций.- М.: МГУ им. Ломоносова, 2000.

5. Бокс Д. Сущность технологии СОМ. Библиотека программиста: Пер. с англ.-СПб.: Питер, 2002.- 400 с.

6. Гамма Э. и др. Приемы объектно-ориентированного проектирования. Паттерны проектирования / Э. Гамма, Р. Хелм, Р. Джонсон, Дж. Влиссидес; Пер. с англ.- СПб.: Питер, 2001. 368 е., ил.

7. Горбунов Н. Встроенные средства диагностики QNX4 // Открытые системы.-2000.- №5-6.

8. ГОСТ Р ИСО 9000-2001. Системы менеджмента качества. -М.:Изд-во стандартов, 2001.

9. ГОСТ Р ИСО 9004-2001. Системы менеджмента качества. Рекомендации по улучшению деятельности. М.:Изд-во стандартов, 2001.

10. Ю.Жданов А.А., Операционные системы реального времени. Москва, PCWeek, N.8,1999.11.3убинский А. Еще одно звено в цепи. Компьютерное обозрение, N. 40, 17-23 октября 2001.

11. Иордон Э. «Путь камикадзе. Как разработчику программного обеспечения выжить в безнадежном проекте. » М. «Лори», 2000г.

12. Канер С., Фолк Дж., Нгуен Е.К. «Тестирование программного обеспечения», «Диасофт», 2000г.

13. М.Кватрани Т. «Rational Rose 2000 и UML. Визуальное моделирование», «ДМК Пресс», Москва, 2001г.

14. Ключев А.О. «Архитектурное проектирование информационно-управляющих систем», Учебное пособие, Кафедра ВТ, СПбГИТМО(ТУ), 2001г.

15. Ключев А.О. «Методы и инструментальное обеспечение разработки распределенных информационно-управляющих систем с программируемой архитектурой» тезисы кандидатской диссертации, СПбГИТМО(ТУ) , Санкт-Петербург , 1999 г.

16. Кузнецов Б.П. Психология автоматного программирования. //BYTE/Россия. 2000. N.11.

17. Майерс Г. «Искусство тестирования программ», «Финансы и статистика», Москва, 1982г.

18. Майерс Г. «Надежность программного обеспечения», «Мир», Москва, 1980г.

19. Матьяш В.А., Никандров А.В., Путилов В.А., Федоров А.Е., Фильчаков В.В. Структурный анализ при разработке программного обеспечения систем реального времени. Апатиты, КФ ПетрГУ, 1997. - 78с.

20. Никитин В.А. Управление качеством на базе стандартов ИСО 9000:2000.-СПб.: Питер, 2002. 272 е.: ил.

21. Прохоров A.M., Советский энциклопедический словарь. Изд. 4-е, Москва, Сов. энциклопедия, 1987.

22. Робачевский А. Операционная система UNIX. СПб.:ВНУ-Санкт-Петербург, 1998.

23. Ройс У. Управление проектами по созданию программного обеспечения: Пер. с англ.- М.: Лори, 2002.

24. Романюк С. Сюрпризы POSIX // Открытые системы, 1999.- №09-10.

25. Самохвалова О.Г. Выбор оптимального алгоритма планирования при разработке программного обеспечения систем реального времени // Научно-технический вестник.- СПб.: СПбГИТМО(ТУ), 2002.- вып. 6. -С. 88-91.

26. Самохвалова О.Г. Планирование в системах реального времени // Сб. аннотаций работ по грантам Санкт-петербуржского конкурса 2001 г. для студентов, аспирантов, молодых ученых и специалистов.- СПб.: Изд-во С.Петерб.ун-та, 2001.- С. 77.

27. Самохвалова О.Г., Платунов А.Е. Планирование в системах реального времени // Политехнический симпозиум «Молодые ученые промышленности Северо-западного региона». Тез. докл. 30 ноября 2001г.- СПб., 2001.- С. 2425.

28. Страуструп Б. Язык программирования С++. 3-е изд./Пер. с англ. СПб., М.: «Невский Диалект» - «Издательство БИНОМ», 1999 г. - 911 е., ил.

29. Фаулер М., Скотт К. UML. Основы. (Второе издание): Пер. с англ.- СПб.: Символ-Плюс, 2002.- 192 е.: ил.

30. Федоров О. Разработка приложений под ОС QXN // Компьютерная неделя, 1998.-№27(151).

31. Фокс Дж. Программное обеспечение и его разработка: Пер. с англ.-, М: Мир, 1985.-368 е., ил.

32. Фридман A.J1. Основы объектно-ориентированной разработки программных систем.- М.: Финансы и статистика, 2000. 192 е., ил.

33. Функционально-временная верификация сложных цифровых систем // Открытые системы, 2002. №6.

34. Цирюлик О.И. QNX: Создание приложений в PhAB. Часть 1. URL: http://qnx.org.ru/docs-devel/phab.html.

35. Шалыто А.А. SWITCH-технология. Алгоритмизация и программирование задач логического управления. СПб: Наука, 1998. - 628 с.

36. Шалыто А.А. Автоматное проектирование программ. Алгоритмизация и программирование задач логического управления //Известия РАН. Теория и системы управления. 2000. N6. с.63-81.

37. Шалыто А.А. Алгоритмизация и программирование задач логического управления техническими средствами. СПб.: МОРИНТЕХ, 1996. 91 стр.

38. Шалыто А.А., Гуров B.C., Нарвский А.С. Автоматизация проектирования событийных объектно-ориентированных программ с явным выделением состояний. //Труды X Всероссийской научно-методической конференции Телематика 2003. Том 1. стр. 282-283.

39. Шалыто А.А., Туккель Н.И. Танки и автоматы //BYTE/Россия. 2003. N.2. http://is.ifmo.ru

40. Шалыто А.А., Туккель Н.И. SWITCH-технология автоматный подход к созданию программного обеспечения «реактивных» систем //Программирование. 2001. N.5. http://is.ifmo.ru

41. Шалыто А.А., Туккель Н.И. От тьюрингова программирования к автоматному //Мир ПК, 2002, N.2.

42. Шалыто А.А., Туккель Н.И. Программирование с явным выделением состояний //Мир ПК. 2001. N.8,9.

43. Шопырин Д.Г., Шалыто А.А. Применение класса «state» в объектно-ориентированном программировании с явным выделением состояний. //Труды X Всероссийской научно-методической конференции Телематика 2003. Том 1. стр. 284-285.

44. Штучкин А.А., Шалыто А.А. Совместное использование теории построения компиляторов и switch-технологии. //Труды X Всероссийской научно-методической конференции Телематика 2003. Том 1. стр. 286-287.

45. Якобсон А. и др. Унифицированный процесс разработки программного обеспечения / А. Якобсон, Г. Буч, Дж. Рамбо; Пер. с англ.- СПб.: Питер, 2002. 496 е., ил.

46. АИ Abbas Mir, Subhashini Balakrishnan and Sofiene Tahar. "Modeling and Veri.cation of Embedded Systems using Cadence SMV", Electrical & Computer Engineering Department, Concordia University (Canada), 1999.

47. Allen R., Garlan D. A Formal Basis for Architectural Connection. ACM Transactions on Software Engineering and Methodology, Vol. 6, No. 3, July 1997, pp. 213-249. School of Computer Science. Carnegie Mellon University. Pittsburgh.

48. Basbugoglu O, Inan K. Compiling SDL Into The Finite State Specification Language COSPAN. Military Electronics Industries, Electrical And Electronic Engineering Department, Middle East Technical University, Turkey.

49. Bass, Clements, Kazman. Software Architecture in Practice, Addison-Wesley 1997.

50. Bestavros A., " Scheduling ", Boston University (USA), 1995.

51. Booch, Rumbaugh, Jacobson. The UML Modeling Language User Guide, Addison-Wesley, 1999.

52. Brooks F.P., Jr., The Mythical Man-Month, Addison-Wesley, 1975.

53. Вгисе Powel Douglass, Ph.D. Chief Evangelist. "Safety-Critical Systems Design" i-Logix, Technical report, 1999.

54. Bruce Powel Douglass, Ph.D. Chief Methodology Scientist. "Real-Time Design Patterns", I-Logix, Technical report, 1999.

55. Chapman R. Program Timing Analysis. Dependable Computing Systems Centre. University of York. Heslington. York, May 31,1994.

56. Cherepov M, Jones C. "Hard Real-Time With RTX on Windows NT". Technical report, VenturCom, Inc. Cambridge, MA, Technical report, 1999.

57. Clarke E.M., Emerson E.A., "Synthesis of Synchronization Skeletons for Branching Time Temporal Logic," Proc. Logic of Programs: Workshop, Yorktown Heights, N.Y., Lecture Notes in Computer Science 131. Springer-Verlag, May 1981.

58. Сотр.realtime: A list of commercial real-time operating systems. URL: http://www.faqs.org/faqs/realtime-computing/list/

59. Comp.realtime: A (LONG) list of real-time operating systems. URL:http://www.immt.pwr. wroc.pl/faq/msg00143 .html

60. Cousot P.,Cousot R. Verification of Embedded Software: Problems and Perspectives. URL:http://www.di.ens.fr/~cousot/publications.www/CousotCousot-EMSQFT01-lg.pdf

61. Garlan D., Monroe R., Wile D. Acme: An Architecture Description Interchange Language. Carnegie Mellon University. USA. Proceedings of CASCON'97, November, 1997.

62. Dekker E.N., Newcomer J.M. Developing Windows NT Device Drivers: A Programmer's Handbook. USA, Pearson Educational, 1999.

63. Dorfman M, Thayer R, Software Engineering, IEEE Computer Society Press, Los Alamos, CA, 1997, pp. 79.

64. Dwyer M. В., Avrunin G. S,Corbett J. C. Patterns in Property Specifications for Finite-state Verification. Proceedings of the 21st International Conference on Software Engineering, May, 1999.

65. Formal Methods Europe. URL:http://www.fmeurope.org/

66. Formal Systems (Europe) Ltd. URL: http://www.fsel.com/software.html

67. FME applications database: Full listing of applications in the database. URL: http ://www. fmeurope.org/databases/full .html

68. Garlan D., Monroe R., Wile D. Acme: An Architecture Description Interchange Language. Proceedings of CASCON'97, November, 1997.

69. Hoare C.A.R., Communicating Sequential Processes. The Queen's University, Belfast, Northern Ireland, Programming Techniques, Communications of the ACM. August 1978, Volume 21.

70. Holzmann G.J. Design And Validation Of Computer Protocols. Bell Laboratories, Murray Hill, New Jersey, PRENTICE-HALL, Englewood Cliffs, New Jersey, 1991.

71. Holzmann G.J. Logic Verification of ANSIC code with SPIN. Bell Laboratories, Lucent Technologies, Murray Hill, New Jersey 07974, USA.

72. Holzmann G.J. The Model Checker Spin. IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, VOL. 23, NO. 5, MAY 1997.

73. Hayes-Roth, F. (1994). Architecture-Based Acquisition and Development of Software: Guidelines and Recommendations from the ARPA Domain-Specific Software Architecture (DSSA) Program. Teknowledge Federal Systems, 1994.

74. HyperDictionary.URL: http://www.hvperdictionary.com/dictionarv/svstem+software.

75. Kuhn M. "A Vision for Linux 2.2 POSIX.lb Compatibility and Real-Time Support", Technical report, 1998-09-03. URL: http://rt22.prao.psn.ru/pub.php?activeb=6&art=3

76. Lee E. F. "Embedded software", "Advances in Computers", Vol. 56, Academic Press, London, 2002.

77. Leveson N., Clark S.T.: An Investigation of the Therac-25 Accidents. IEEE Computer, Vol.26, No.7, July 1993, p.18-41.

78. Magee J., Kramer J., Giannakopoulou D. Analysing the Behaviour of Distributed Software Architectures: a Case Study. Fifth IEEE Workshop on Future Trends of Distributed Computing Systems, FTDCS '97, Tunisia, October 1997.

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

80. Moore G., Progress In Digital Integrated Electronics. 1975 International Electron Device Meeting Tech. Digest, pp.11-13.

81. McMillan K. L., Symbolic Model Checking: An Approach to the State Explosion Problem, Kluwer Academic Publishers, 1993.

82. McMiIlan K.L. The SMV System. 2000. URL: http://www.cs.wpi.edu/~kfisler/Courses/525V/S02/Readings/smv-cadence.pdf

83. Queille J.P., Sifakis J., "Specification and Verification of Concurrent Systems in Cesar," Proc. Fifth Int'l. Symp. Programming, pp. 195-220, Lecture Notes In Computer Science 137. USA. Springer-Verlag 1981.

84. Selic В., Gullekson G., McGee J., Engelberg I, ROOM: An Object-Oriented Methodology for Developing Real-Time Systems, CASE'92 Fifth International Workshop on Computer-Aided Software Engineering, Montreal, Quebec, Canada, July 6-10,1992.

85. Spin Online References. URL: http://spinroot.com/spin/Man/index.html

86. Telelogic products Telelogic TAU - Automated Software Development and Testing tools. URL: http://www.telelogic.com/products/tau/tg2.cfm

87. White R., Syyid U. "Architecture Driven Software Design For Embedded Systems", Technical report, 1999.

88. Результат-модель архитектуры канала передачи данных драйвера Windows NT 5.0

89. NT 5.0 driver model, includes write channel to devicedefine #define #define

90. Результат-модель КВМ арбитража активности

91. U0.=false) && (U[l]=false)) -> U[0]=trae; U[l]=true;} :: atomic {((P[0]=true) && (P[ 1 ]=true) && /*UDP OFF */

92. U0.=true) && (U[l]=true)) -> U[0]=false; U[l]=false;}od;init {1. ClrEnvO;

93. ClrCMP(O); /*clear CMP A*/

94. ClrCMP(l); /*clear CMP В*/atomic {run CMPLevel 1 (0,q0.,q[ 1 ]); run CMPLevell(l,q[l],q[0]); run EnvironmentQ;}

95. Закрытое акционерное общество1. В НИИР А ОВД»почтовый адрес: 199106, г. Санкт-Петербург, Шкиперский пр. 19 факс: [phone], тел./факс:[phone] e-mail: [e-mail]1. АКТ О ВНЕДРЕНИИ

96. Настоящий акт не дает автору право на материальное вознаграждение.

97. Генеральный директор ЗАО ВНИИРА-ОВД Действительный член Международной Академии Транспорта ' Лауреат Государственной премии СССР Кандидат технических наук

98. Главный конструктор МВРЛ-СВК Кандидат технических наук1. Главный специалист

99. Зам. Главного конструктора МВРЛ-СВК1. Сш у Б.А. Лапину1. П.М. ШвайгерГ1. УТВЕРЖДАЮам. генерального директорадиректор пМЖ и НИР1. А—В.М. Корчанов2004 г.о реализации научных результатов диссертационной работы Окулевича Владимир Викеньтьевича

100. Научно-техническая комиссия в составе: Председателя начальника НИО-ЗО, доктора технических наук

101. Лущика Всеволода Леонидовича, Членов комиссии начальника 305 отдела, кандидата технических наук,старшего научного сотрудника Гаврилова Алексея Федоровича,- ведущего научного сотрудника, кандидата технических наук, старшего научного сотрудника

102. Дымента Анатолия Вениаминовича,- ведущего инженера-программиста Беляева Бориса Литмановича,- старшего научного сотрудника, кандидата технических наук, старшего научного сотрудника

103. Начальник НИО-ЗО, доктор технических наук1. Члены комиссии:1. В.Л.Лущик

104. Начальник отдела 305, кандидат технических наук, старший научный сотрудник1. А.Ф.Гаврилов

105. Ведущий научный сотрудник, кандидат технических наук,старший научный сотрудник А.Б.Дымент

106. Ведущий инженер-программист ^Г Б.Л.Бе„яеВ

107. Старший научный сотрудник,кандидат технических наук Л^^-ч. В.Н.Волобуев

108. ОБЩЕСТВО С ОГРАНИЧЕННОМ ОТВЕТСТВЕННОСТЬЮ "ЛМТ"3?" от IZ.O^.ZoqH На №от1. АКТ О ВНЕДРЕНИИ

109. Настоящий акт не дает автору права на материальное вознаграждение.1. Ключев А.О.• о/ ji

110. Технический директор ООйЦШМЪ/Г!1.» j^^^yyr' ,у195197, г. Санкт-Петербург, а/я 148, email: info@lmt.i:ifmo.ru

111. Закрытое акционерное общество190031, САНКТ-ПЕТЕРБУРГ НАБ. Р. ФОНТАНКИ, Я 117

112. ТЕЛ: [phone] ФАКС: [phone]. АКТ О ВНЕДРЕНИИ

113. Окулевич В.В. принимал активное участие в разработке программного обеспечения комплекса технических средств (КТС) 'Тракт".

114. Настоящий акт не дает автору право на материальное вознаграждение.о внедрении в учебный процесс результатов диссертационной работы Окулевича Владимира Вшеентьевича1. Комиссия в составе:

115. Председателя заведующего кафедрой вычислительной техники,профессора, доктора технических наук Алиева Тауфика Измайловича, Членов комиссии профессора, доктора технических наук

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

117. Аналитический обзор методов и инструментов построения и верификации моделей системного программного обеспечения (СПО) информационно-управляющих систем (ИУС).

118. Технологию построения и верификации моделей СПО ИУС в рамках процесса разработки программного обеспечения ИУС.

119. Классификацию объектов СПО ИУС.

120. Библиотеку типовых элементов моделей СПО ИУС, в том числе соответствующих объектам операционных систем реального времени, удовлетворяющим стандарту POSIX 1003.1.

121. Перечисленные результаты диссертационной работы включены вэлектронные учебные пособия для студентов по указанным дисциплинам.

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

123. Настоящий акт не дает автору право на материальное вознаграждение.1. Председатель комиссии

124. Заведующий кафедрой вычислительной техники, профессор, доктор технических наук1. Т.И. Алиев1. Члены комиссии:

125. Профессор, доктор технических наук1. А.Ю. Тропченко1. Э.В. Стародубцев