Математическое моделирование верификации процесса разработки программного обеспечения тема диссертации и автореферата по ВАК РФ 05.13.18, кандидат технических наук Григорьев, Михаил Викторович
- Специальность ВАК РФ05.13.18
- Количество страниц 135
Оглавление диссертации кандидат технических наук Григорьев, Михаил Викторович
Введение.
Глава I Обзор методов и алгоритмов верификации программной инженерии.
Методологии разработки программного обеспечения.
Верификация процесса разработки программного обеспечения.
Описание семантики процесса разработки.
Комплексы поддержки программной инженерии.
Выводы.
Глава II Математическая модель верификации процесса программной инженерии.
Модель разработки программного обеспечения.
Динамическая модель процесса разработки программного обеспечения.
Выводы.
Глава III Модель семантических отношений между артефактами проекта.
Метод оценки корректности рабочих продуктов.
Язык определения семантических отношений артефактов.
Компилятор языка семантических отношений артефактов.
Выводы.
Глава IV Программный комплекс поддержки разработки программного обеспечения.
Архитектура программного комплекса.
Описание модулей программного комплекса.
Выводы.
Глава V Апробация программного комплекса.
Модификация унифицированного процесса разработки программного обеспечения.
Проведение эксперимента.
Правила верификации процесса разработки программного обеспечения
Практика использования программного комплекса в учебных проектах.
Выводы.
Выводы по диссертационной работе.
Список источников и литературы.
Рекомендованный список диссертаций по специальности «Математическое моделирование, численные методы и комплексы программ», 05.13.18 шифр ВАК
Методы и программные средства разработки логических компонентов систем с пошаговыми стратегиями2011 год, кандидат технических наук Павлова, Елена Анатольевна
Интегрированная технология обеспечения качества программных продуктов с помощью верификации и тестирования2006 год, кандидат технических наук Дробинцев, Павел Дмитриевич
Разработка методов и средств обработки лингвистических структурно-функциональных моделей цифровых аппаратных средств на основе нейро-семантических сетей2007 год, кандидат технических наук Игонин, Андрей Геннадьевич
Методы и алгоритмы проверки адекватности аналитических моделей организационной деятельности предприятия2009 год, кандидат технических наук Коломиец, Инна Ивановна
Методы проектирования компьютерных обучающих систем для образовательной сферы2007 год, доктор технических наук Черткова, Елена Александровна
Введение диссертации (часть автореферата) на тему «Математическое моделирование верификации процесса разработки программного обеспечения»
Актуальность работы. В современной индустрии программного обеспечения огромное внимание уделяется процессу разработки, который сформировал в последние десятилетия самостоятельную область знаний «Программная инженерия» (В.В. Липаев, JI.A. Мацяшек, P. Naur, В. Randell, D. Parnas, W. Stevens, G. Myers, L. Constantine, А. Шалыто, И. Соммервилл, С. Бобровский и др.). На сегодняшний день нет устоявшихся принципов организации процесса разработки, многие организации пропагандируют собственные методы и процессы программной инженерии (SWEBOK, CMMI, MSF, MDA, RUP и т.д.). В тоже время большинство методологий оценивает качество организации процесса разработки по качеству программного продукта (Е.В. Крылов, В.А. Острейковский, Н.Г. Типикин, П.М. Дюваль, С. Матиас, Э. Гловер и др.).
Существует множество методов инспектирования, позволяющих выявить проблемы и недостатки программных продуктов (ГОСТ Р ИСО 9000, ГОСТ Р ИСО/МЭК 15288, ГОСТ Р ИСО/МЭК 12207, ISO/IEC TR 15504, IEEE Std 1059, С. Орлик и др.). Верификация программного обеспечения известна и широко используется (С.В. Синицын, Н.Ю. Налютин, Э.М. Кларк, О. Грамберг, Д. Пелед, Дж. Сифакис и др.). Метод верификации предоставляет эффективные средства локализации проблем программного обеспечения и поиска их потенциального решения (Е. Ashcroft, S. Owicki, D. Gries, A. Pnueli, C. Jones). Верификация процесса разработки не выделена в самостоятельный процесс программной инженерии. Требуется изучить процесс разработки программного обеспечения и создать механизм его верификации.
Практичность программной инженерии складывается из многочисленных аспектов, связанных как с особенностями организации процессов разработки программного обеспечения, так и с реализацией конечных продуктов. В работах Б. Боэма, Р. Фатрелла, Э. Брауде, J1. Локвуда, Д. Шафера убедительно показано, что успешная разработка программного обеспечения зависит не только от получения удачного программного продукта, но также от получения удачных процессов разработки программных систем. При отсутствии обратной связи и усовершенствований даже самый практичный проект обречен на неудачу. Существуют методы, которые косвенным образом дают возможность оценить качество организации процессов: аттестация, аудит, валидация, верификация, рецензирование, тестирование, экспертиза. Как правило, эти методы привязаны лишь к некоторым дисциплинам программной инженерии и носят декларативный характер.
Современный уровень формализации методов программной инженерии создает все предпосылки для разработки формальных методов инспектирования качества организации процесса разработки программного обеспечения.
Целью работы является повышение качества программной инженерии путем формализации верификации процесса командной разработки проектов.
Для достижения поставленной цели определены следующие задачи исследования:
1) модификация модели процесса разработки для обеспечения возможности проверки корректности организации процессов программной инженерии;
2) создание метода инспектирования процесса разработки программного обеспечения и построение математической модели, формализующей этот метод;
3) разработка комплекса программ поддержки процесса создания программного обеспечения в команде, который позволит проводить оценку организации этого процесса;
4) проведение испытания программного комплекса, с целью проверки адекватности разработанных методов и моделей.
Методы исследований. При решении поставленных задач использовались эффективные математические методы теории формальных языков и автоматов, алгебры темпоральной логики, теории компиляторов, теории графов.
Достоверность и обоснованность результатов подтверждается использованием и применением опробованных методов проектирования и разработки информационных систем, унифицированного языка моделирования, архитектуры, управляемой моделями, а также вычислительным экспериментом, подтвердившим адекватность предложенного метода верификации и математических моделей, реализующих его.
Научная новизна работы заключается в следующем:
1) модифицирована метамодель процесса инжиниринга программного обеспечения, которая дает возможность реализовать верификацию процесса за счет идентификации отношений между артефактами разработки;
2) разработан метод верификации процесса создания программного обеспечения, основанный на выявлении пути в модели Крипке с помощью алгебры темпоральной логики, что дает возможность отобразить динамику процесса в пространстве артефактов;
3) обосновано архитектурное решение проверки семантических отношений артефактов проекта путем оценки выполнения правил, записанных в грамматике формального языка ограничений.
Практическая значимость работы:
1) разработан компилятор языка fOCL, который позволяет выявить синтаксические и семантические ошибки при написании правил взаимодействия рабочих продуктов. Интеграция скомпилированного правила дает возможность выполнять проверку артефактов в однозначных проектах без модификации самого правила;
2) создан программный комплекс, организация которого впервые охватывает все уровни архитектуры моделирования Object Management Group (OMG), позволяющий выполнить верификацию процесса командной разработки проектов;
3) модифицирован унифицированный процесс разработки программного обеспечения для небольших проектных групп, который включает предложенный метод верификации процесса создания программного обеспечения.
Реализация и внедрение результатов работы. Комплекс программ опробован в курсе «Проектирование информационных систем» при подготовке студентов по специальности 080801.65 «Прикладная информатика в экономике», что подтверждается соответствующим актом внедрения, выданным Тюменским государственным университетом. Модифицированный унифицированный процесс для небольших проектных групп внедрен в виде методического пособия по предмету «Проектирование информационных систем», на которое получен гриф УМО для специальности «Прикладная информатика (по областям)».
Апробация работы. Основные результаты диссертационной работы были представлены на следующих научных конференциях: Всероссийская научная конференция молодых ученых «Наука. Технологии. Инновации» (Россия, Новосибирск, декабрь 2006); Межвузовская научно-практическая конференция студентов, аспирантов и молодых ученых «Безопасность информационного пространства» (Россия, Тюмень, ноябрь 2007); Всероссийская научно-практическая конференция с международным участием «Дистанционные образовательные технологии: опыт применения и перспективы развития» (Россия, Тюмень, февраль 2008); Научно-практическая конференция молодых ученых «Современные проблемы математического и информационного моделирования. Перспективы разработки и внедрения инновационных 1Т-решений» (Россия, Тюмень, май
2008); Научно-методические семинары кафедры информационных систем Тюменского государственного университета (2005-2009 гг.).
Публикации. Основное содержание работы отражено в 13 публикациях, из которых 3 свидетельства о государственной регистрации программы для ЭВМ и 1 статья, опубликованная в журнале из списка ВАК.
Структура и объем работы. Диссертация состоит из введения, пяти глав, заключения и списка литературы. Объем диссертации составляет 119 страниц, содержит 34 рисунка, 3 приложения. В библиографии представлено 113 наименований работ российских и зарубежных авторов.
Похожие диссертационные работы по специальности «Математическое моделирование, численные методы и комплексы программ», 05.13.18 шифр ВАК
Верификация автоматных программ в контексте синхронного программирования2008 год, кандидат технических наук Кубасов, Сергей Валерьевич
Синтез и верификация управляющих алгоритмов реального времени для бортовых вычислительных систем космических аппаратов2007 год, доктор технических наук Тюгашев, Андрей Александрович
Методика комплексной функциональной верификации модулей системного обмена микропроцессорных вычислительных комплексов2012 год, кандидат технических наук Стотланд, Ирина Аркадьевна
Автоматизация разработки трансляторов мультисинтаксических языков программирования мультиверсионных программных систем2009 год, кандидат технических наук Кузнецов, Александр Сергеевич
Анализ взаимовлияний при интеграции новой функциональности в существующую систему средствами верификации и тестирования2009 год, кандидат технических наук Тихомиров, Владимир Александрович
Заключение диссертации по теме «Математическое моделирование, численные методы и комплексы программ», Григорьев, Михаил Викторович
Выводы по диссертационной работе
1. Модифицирована метамодель SPEM, формализующая семантические отношения между артефактами, что дает возможность реализовать верификацию процесса разработки ПО.
2. Предложен метод верификации процесса разработки, основанный на применении темпоральной логики к модели Крипке, которая отображает динамику процесса в пространстве артефактов. Метод позволяет построить трассы изменения артефактов в процессе создания ПО, что позволяет выявить как ошибки в рабочих продуктах, так и неправильную организацию процесса.
3. Разработан конечный автомат Мура, реализующий предложенный метод верификации процесса создания ПО, который дает возможность выявить причины возникновения ошибок и оценить влияние этих ошибок на дальнейший процесс разработки. Полученный автомат может быть применен как ко всему процессу, так и к отдельному этапу разработки.
4. Создан язык fOCL, формализующий правила проверки артефактов, инкапсулирующий декларативную грамматику объектного языка ограничений ОСЬ. Разработан компилятор, который позволяет выявить синтаксические и семантические ошибки при написании правила. Интеграция скомпилированного правила дает возможность выполнять проверку артефактов в однозначных проектах без модификации самого правила.
5. Разработан программный комплекс, реализующий возможности верификации процесса командной разработки проектов. Организация программного комплекса охватывает все уровни архитектуры моделирования OMG.
6. Модифицирован унифицированный процесс для небольших проектных групп, позволяющий реализовать предложенный метод верификации процесса создания ПО. Данный процесс был внедрен в виде методического пособия по предмету «Проектирование информационных систем», на который был получен гриф УМО для специальности «Прикладная информатика по областям»
7. Автоматическая верификация процесса разработки ПО, выполненных в учебных группах показала возможность снижение темпа роста ошибок по мере выполнения проекта. Успешное применение программного комплекса, реализующего разработанные модели верификации процесса разработки ПО, подтверждает адекватность построенных моделей.
Список литературы диссертационного исследования кандидат технических наук Григорьев, Михаил Викторович, 2009 год
1. Г. Буч. UML. Классика CS. 2-ое изд. / Г. Буч, А. Якобсон, Дж. Рамбо: Пер. с англ.; Под общей редакцией проф. С. Орлова СПб.: Издательство: «Питер», 2006. — 736 е.: ил.
2. Г. Буч. Язык UML. Руководство пользователя. 2-ое изд. / Г. Буч, Д. Рамбо, И. Якобсон.: Пер. с англ. Мухин Н. М.: Издательство: «ДМК Пресс», 2007. - 496 е.: ил.
3. Г. Буч. Язык UML. Руководство пользователя. / Г. Буч, Д. Рамбо, А. Джекобсон.: Пер. с англ. Слинкин А.А. 2-ое изд., стер. - М.: Издательство: «ДМК Пресс»; СПб.: Издательство: «Питер», 2004, — 432 е.: ил.
4. Д. Рамбо. UML. Специальный справочник. / Д. Рамбо, А. Якобсон, Г. Буч. СПб.: Издательство: «Питер», 2002. - 656 с.
5. Д. Рамбо. UML 2.0. Объектно-ориентированное моделирование и разработка. 2-ое изд. / Д. Рамбо, М. Блаха. СПб.: Издательство: «Питер», 2007 - 544 е.: ил.
6. А. Якобсон. Унифицированный процесс разработки программного обеспечения. / А. Якобсон, Г. Буч, Д. Рамбо. СПб.: Издательство: «Питер», 2002, - 496 е.: ил.
7. Дж. Шмуллер. Освой самостоятельно UML за 24 часа, 3-е изд. : Пер. с англ. М.: Издательский дом «Вильяме», 2005. — 416 е.: ил. — Парал. тит. англ.
8. К. Ларман. Применение UML и шаблонов проектирования. 2-ое изд.: Пер. с англ. М.: Издательский дом "Вильяме", 2004. — 624 е.: ил. -Парал. тит. англ.
9. К. Ларман. Применение UML 2.0 и шаблонов проектирования.: Пер. с англ. — М.: Издательский дом "Вильяме", 2008. — 736 е.: ил. — Парал. тит. англ.
10. М. Фаулер. UML. Основы. 2-ое изд. Краткое руководство по унифицированному языку моделирования / М. Фаулер, К. Скотт.: Пер. с англ. СПб.: Издательство: «Символ-Плюс», 2006. — 192 е.: ил.
11. М. Фаулер. UML. Основы. 3-е изд. Краткое руководство по стандартному языку объектного моделирования.: Пер. с англ. — СПб.: Издательство: «Символ-Плюс», 2002. 192 е.: ил.
12. Э. Нейбург. Проектирование баз данных с помощью UML. / Э. Нейбург, Дж. Максимчук, А. Роберт.: Пер. с англ. — М.: Издательский дом «Вильяме», 2002. 288 е.: ил. - Парал. тит. англ.
13. Hans-Erik Eriksson. Business Modeling with UML: Business Patterns at Work. / H. Eriksson, M. Penker. OMG Press. John Wiley & Sons, 2000. -459 pages.
14. Ф. Крачтен. Введение в Rational Unified Process. 2-ое изд.: Пер. с англ. М.: Издательский дом «Вильяме», 2002. — 240 е.: ил. — Парал. тит. англ.
15. Г. Поллис. Разработка программных проектов: на основе Rational Unified Process (RUP). / Г. Поллис, JI. Огастин, К. Jloy, Д. Мадхар. -М.: Издательство: ООО «Бином-Пресс», 2005 г. 256 е.: ил.
16. Электронное справочное руководство Rational Unified Process Version 7.0 Copyright (С) IBM Corporation 1987, 2005.
17. S. Ambler. The Enterprise Unified Process: Extending the Rational Unified Process. / S. Ambler, J. Nalbone, M. Vizdos. Prentice Hall PTR, 2005. -408 pages.
18. J. Warmer. The Object Constraint Language. Precise Modeling with UML. / J. Warmer, A Kleppe.: Addison-Wesley Professional, 1998. 112 pages.
19. J. Warmer. The Object Constraint Language Second Edition. Getting Your Models Ready for MDA (2nd Edition). / J. Warmer, A Kleppe.: Addison-Wesley Professional, 2003 — 206 pages.
20. Д. Хопкрофт. Введение в теорию автоматов, языков и вычислений, 2-ое изд. / Д. Хопкрофт, Р. Мотвани, Д. Ульман.: Пер. с англ. М.: Издательский дом «Вильяме», 2008. — 528 е.: ил. — Парал. тит. англ.
21. Б.А. Трахтенброт. Конечные атоматы (поведение и синтез). / Б.А. Трахтенброт, Я.М. Барздинь. — М.: Издательство: «Наука», 1970. 400 е.: ил.
22. Н.К. Верещагин. Лекции по математической логике и теории алгоритмов. Часть 1. Начала теории множеств. / .К. Верещагин, А. Щень. -М.: Издательство: «МЦНМО», 1999. 128 с.
23. А.В. Гладкий. Формальные грамматики и языки. — М.: Издательство: «Наука», 1973.-368 с.
24. Н. Хомский. Введение в формальный анализ естественных языков. / Н. Хомский, Дж. Миллер. М.: Издательство: «Едиториал УРСС», 2003. -64 с.
25. Э. Брауде. Технология разработки программного обеспечения. СПб.: Издательство: «Питер», 2004. - 655 е.: ил.
26. С. Амблер. Гибкие технологии: экстремальное программирование и унифицированный процесс разработки. Библиотека программиста. -СПб.: Издательство: «Питер», 2005. 412 е.: ил.
27. JT. Константайн. Разработка программного обеспечения. / JI. Константайн, JI. Локвуд. СПб.: Издательство: «Питер», 2004. - 592 е.: ил.
28. Scott W. Ambler. The Object Primer, Third Edition. Cambridge University Press, 2004 572 pages.
29. Э. Роллингз. Проектирование и архитектура игр. / Э. Роллингз, Д. Моррис.: Пер. с англ. М.: Издательский дом «Вильяме», 2006. — 1040 е.: ил. - Парал. тит. англ.
30. Д. Шафер. Управление программными проектами: достижение оптимального качества при минимуме затрат. / Д. Шафер, Р. Фатрелл, J1. Шафер.: Пер. с англ. — М.: Издательский дом «Вильяме», 2003. — 1136 е.: ил. Парал. тит. англ.
31. IEEE Guide to the Software Engineering Body of Knowledge -SWEBOK®. California, Computer society, 2004 version.
32. М. Bonsangue. Formal Methods for Open Object-Based Distributed Systems: 9th IFIP WG 6.1 International Conference, FMOODS 2007, Paphos, Cyprus, June 6-8, 2007, Proceedings. / M. Bonsangue, E. Johnsen.: Springer, 2007. — 317 pages.
33. B. Beckert. Verification of Object-Oriented Software. The KeY Approach: Foreword by K. Rustan M. Leino. / B. Beckert, H. Hahnle, P. Schmitt.: Springer, 2007. 658 pages.
34. E. Najm. Formal Methods for Open Object-Based Distributed Systems: 6th IFIP WG 6.1 International Conference, FMOODS 2003, Paris, France, November 19.21, 2003, Proceedings. / E. Najm, U. Nestmann, P. Stevens.: Springer, 2003. 293 pages.
35. A. Ахо. Компиляторы: принципы, технологии, инструменты. / А. Ахо, Р. Сети, Дж. Ульман. М.: Издательский дом «Вильяме», 2003. — 768 с.
36. ГОСТ Р ИСО 9000-2001 Системы менеджмента качества. Основные положения и словарь. — М.: Издательство: «Госстандарт России», 2001.
37. ГОСТ Р ИСО 9001-2001 Системы менеджмента качества. Требования. М.: Издательство: «Госстандарт России», 2001.
38. ГОСТ Р ИСО/МЭК 12207-99 Информационная технология. Процессы жизненного цикла программных средств. — М.: Издательство: «Госстандарт России», 2000.
39. ГОСТ Р ИСО/МЭК 15288-2005 Информационная технология. Системная инженерия. Процессы жизненного цикла систем. М.: Издательство «Сгандартинформ», 2006.
40. Object Management Group (OMG) (2006, May 01). Object Constraint Language Specification (OCL) Version 2.0 WWW document. URL http://www.omg.org/cgi-bin/doc7fomial/2006-05-01 46.The Object Constraint Language [WWW document].
41. URL http://www.csci.csusb.edu/dick/samples/ocl.html 47.Object Constraint Language WWW document.
42. URL http://en.wikipedia.org/wiki/ObjectConstraintLanguage
43. Some Shortcomings of OCL, the Object Constraint Language of UML WWW document.
44. URL http://www.omg.org/docs/ad/99-12-05.pdf 49.Introduction to OCL WWW document.
45. URL http://www.klasse.nl/ocl/ocl-introduction.html 50. Why Combine UML and OCL? WWW document.
46. URL http://www.klasse.nl/ocl/ocl-reasons.html 51.0bject-zto OCL dictionary WWW document.
47. URL http://www.klasse.nl/ocl/oz-ocl-mapping.pdf 52.On the Expressive Power of the Object Constraint Language OCL WWW document.
48. URL http://projekte.fast.de/Projekte/forsoft/ocl/ocl.html 53.Architecture and Design: Unified Modeling Language (UML) WWW document.
49. URL http://www.omg.Org/spec/SPEM/2.0/PDF 56.Object Management Group (OMG) (2006, January 01). Meta Object Facility (MOF) Core specification Version 2.0 WWW document. URL http://www.omg.org/spec/MOF/2-0/PDF/
50. UML to XMI Export Functionality WWW document. URL http://msdn.microsoft.com/en-us/library/aal40339.aspx
51. Eclipse Process Framework (EPF) 1.2.0 WWW document.
52. URL http://nvoynov.blogspot.eom/2007/08/eclipse-process-framework-epf-120.html
53. IBM Rational Method Composer WWW document.
54. URL http://www.interface.ru/home.asp7artI d=543 5 63.IBM Rational Requisite Pro WWW document.
55. URL http://www.interface.ru/liome.asp?artId=l0131 64.IBM Rational Requisite Pro-2 WWW document. URL http://www.interface.ru/liome.asp?artId=l 0294
56. RequisitePro средство управления требованиями URL http://www.interface.ru/home.asp?artld=4835
57. Моделирование процессов разработки ПО и процессов с помощью Rational Method Composer URL http://www.interface.ru/home.asp?artId=l 524
58. Выпуск Eclipse Process Framework (EPF) версии 1.2.0 WWW document.
59. URL http.7/www.it4business.ru/archives/444/ 68.IBM Rational Unified Process WWW document.
60. URL http://www.interface.ru/home.asp?artld=486 69.Унифицированный процесс разработки от Rational Software RUP (Rational Unified Process) WWW document. URL http://www.interface.ru/home.asp?artId=34221. WWW document.создание сайтов WWW document.
61. IBM Rational Unified Process (RUP) WWW document. URL http://www.interface.ru/home.asp?artTd=5154
62. Модель качества разработок CMM и ее поддержка линейкой продуктов Rational WWW document.
63. URL http://www.interface.m/home.asp?artld:=2304
64. Rational Unified Process как достичь 2-го уровня CMM WWW document.
65. URL http://www.interface.ru/home.asp?artId=2310
66. Rational Unified Process как достичь 3-го уровня CMM WWW document.
67. URL http://www.interface.ru/home.asp?artld=2312
68. Использование RUP для небольших проектов: расширение экстремального программирования WWW document.
69. URL http://www.interface.ru/home.asp?artld=4720
70. Динамичный RUP: Вести с передовой WWW document. URL http://www.interface.m/home.asp?artId=l9794
71. RUP и другие методологии разработки ПО WWW document. URLhttp://cmcons.com/articles/obshhiestatimp/rupidrugiemetodologiiraz rabotkipo/
72. OpenUP это просто WWW document.
73. URL http://www.interface.ru/home.asp?artId=9995 78.Отличие формальных и гибких методологий разработки в картинках WWW document.
74. URL http://www.it4business.ru/lib/1299/
75. Технология разработки программного обеспечения WWW document. URL http://www.interface.i-u/home.asp?artId=4718
76. Переход от каскадной разработки к итеративной WWW document. URL http://www.interface.rn/home.asp7arUxNl 15581 .Разработка программного обеспечения группой в составе одного человека WWW document. URL http://www.interface.ru/home.asp?artId=4714
77. Нику да без трассировки: практические советы по внедрению трассируемости WWW document.
78. URL http://www.interface.ru/home.asp?artld=6769
79. В круге разработки WWW document. URL attachment:/70/attachment70.htm84.Компилятор WWW document.
80. URL http://ru.wildpedia.org/wild/KoMnmMTop85.Compiler WWW document.
81. URL http://en.wikipedia.org/wiki/Compiler
82. List of important publications in computer science WWW document. URLhttp://en.wikipedia.org/wiki/Listofimportantpublicationsincomputers cience
83. Temporal logic WWW document.
84. URL http://en.wikipedia.org/wiki/Temporallogic
85. Temporal logic in finite-state verification WWW document.
86. URL http://en.wikipedia.org/wiki/Temporallogicinfinitestateverification
87. Семантика Крипке WWW document.
88. URL http://ru.wikipedia.org/wiki/CeMaHTHKaKpHnKe
89. Kripke semantics WWW document.
90. URL http://ru.wikipedia.org/wiki/CeMaHTHKaKpHnKe
91. Kripke structure WWW document.
92. URL http://en.wikipedia.org/wiki/Kj-ipkestructure
93. J. Burgess. Kripke Models. WWW document.,
94. URL http://www.princeton.edu/~jburgess/Kripkel .doc
95. Конечный автомат WWW document.
96. URL http://ru.wikipedia.0rg/wiki/K0He4HbieaBT0MaTbi
97. Finite state machine WWW document.
98. URL http://en.wikipedia.org/wiki/Finitestatemachine
99. Moore machine WWW document.
100. URL http://en.wikipedia.org/wiki/Mooremachine
101. Алгебра логики WWW document.
102. URL http://ru.wikipedia.org/wiki/Алгебралогики
103. Boolean logic WWW document.
104. URL http://en.wikipedia.org/wiki/Booleanlogic
105. Формальная грамматика WWW document.
106. URL http://ш.wikipedia.org/wiki/Фopмaльнaягpaммaтикa
107. Formal grammar WWW document.
108. URL http://en.wikipedia.org/wiki/Formalgrammar
109. Formal verification WWW document.
110. URL http://en.wikipedia.Org/wiki/Formalverification
111. А.Г. Ивашко, М.В. Григорьев, И.И. Коломиец. Проектирование информационных систем: Учебно-методическое пособие / А.Г. Ивашко, М.В. Григорьев, И.И. Коломиец. Тюмень. Изд-во ТюмГУ,2007. 328 с.
112. А.Г. Ивашко, М.В. Григорьев. Объектно-ориентированный язык ограничений для верификации процесса командной разработки программного обеспечения // Вестник ТюмГУ, 2008. — №6. — Тюмень. С. 152-158.
113. М.В. Григорьев. Верификация процесса разработки программного обеспечения в команде // Математическое и информационное моделирование. Сборник научных трудов. Вып. 10. — Тюмень. Изд-во «Вектор Бук», 2008. С. 98-106.
114. М.В. Григорьев, О.И. Гладич. Об одном подходе к реализации редактора объектного языка ограничений // Проблемы информатики в образовании, управлении, экономике и технике: сборник статей VIII
115. Всероссийской научно-технической конференции — Пенза. Изд-во «Приволжский Дом знаний», 2008. — С. 100-102.
116. М.В. Григорьев, Ф.Ф. Мусин. Свидетельство о государственной регистрации баз данных №2009620056 «Веб-представление учебного процесса разработки программного обеспечения» от 22.01.2009.
117. М.В. Григорьев, А.В. Урзиков. Свидетельство о государственной регистрации программы для ЭВМ №2008613269 «Viewer for Eclipse» от 09.07.2008.
118. М.В. Григорьев, О.И. Гладич. Свидетельство о государственной регистрации программы для ЭВМ №2008613270 «Tools for EUR» от 09.07.2008.
Обратите внимание, представленные выше научные тексты размещены для ознакомления и получены посредством распознавания оригинальных текстов диссертаций (OCR). В связи с чем, в них могут содержаться ошибки, связанные с несовершенством алгоритмов распознавания. В PDF файлах диссертаций и авторефератов, которые мы доставляем, подобных ошибок нет.