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

На правах рукописи

ОКУЛЕВИЧ ВЛАДИМИР ВИКЕНТЬЕВИЧ

МЕТОДЫ ПОСТРОЕНИЯ И ВЕРИФИКАЦИИ МОДЕЛЕЙ СИСТЕМНОГО ПРОГРАММНОГО ОБЕСПЕЧЕНИЯ ИНФОРМАЦИОННО-УПРАВЛЯЮЩИХ СИСТЕМ

Специальность 05.13.12 "Системы автоматизации проектирования (приборостроение)"

АВТОРЕФЕРАТ диссертации на соискание ученой степени кандидата технических наук

ЦлСл^-

Санкт-Петербург - 2004

Работа выполнена в Санкт-Петербургском Государственном университете информационных технологий, механики и оптики

Научный руководитель:

Официальные оппоненты:

доцент, кандидат технических наук Платунов Алексей Евгеньевич

профессор, доктор технических наук Гатчин Юрий Арменакович

доцент, кандидат технических наук Кругликов Вячеслав Константинович

Ведущее предприятие: ФГУП Санкт-Петербургское

ОКБ "Электроавтоматика"

Защита диссертации состоится 18 мая 2004 г. в 15 часов 50 минут на заседании Специализированного Совета Д212.227.05 при Санкт-Петербургском Государственном университете информационных технологий, механики и оптики по адресу: 197101, Санкт-Петербург, ул. Саблинская, д. 14.

С диссертацией можно ознакомиться в библиотеке СПбГУИТМО. Автореферат разослан 16 апреля 2004 г.

Ученый секретарь

Совета Д212.227.05, к.т.н., доцент

Владимир Иванович

ОБШДЯ ХАРАКТЕРИСТИКА РАБОТЫ

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

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

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

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

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

1. Конкретизированы область и типы объектов СПО в составе ПО ИУС;

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

3. Разработаны методы и средства представления СПО ИУС для создания моделей, согласованных с выбранным методом моделирования;

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

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

6. Базовый метод усовершенствован в части представления требований верификации и сокращения объема пространства состояний;

1 РОС НАЦИОНАЛЬНАЯ 1 1 БИБЛИОТЕКА !

!

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Разработанный метод был использован при реализации СПО арбитража активности резервируемых модулей управления устройствами радиолокатора МВРЛ-СВК, проектировании драйвера управления связевым оборудованием системы КТС "Тракт" для Windows NT 5.0 и др. Полученные теоретические и практические результаты использовались при постановке учебного курса "Операционные системы реального времени". Акты о внедрении прилагаются.

Апробация работы. По материалам диссертации были выполнены доклады на следующих конференциях и семинарах: Политехнический симпозиум "Молодые ученые - промышленности Северо-Западного региона" (г.Санкт-Петербург, 2001,2002,2003 г.), XXXII научная и учебно-методическая конференция СП6ТИТМО(ТУ), посвященная 300-летию Санкт-Петербурга (г.Санкт-Петербург, 2003 г.), XXXI и ХХХШ научные и учебно-методические конференции СП6ГИТМО(ТУ) (г.Санкт-Петербург, 2002 и 2004 г.), Региональная научная конференция студентов, аспирантов и молодых ученых "Наука. Техника. Инновации. " (г. Новосибирск, 2002 г.), X Всероссийская

научно-методическая конференция "Телематика 2003" (г. Санкт-Петербург, 2003 г.).

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

Публикации. По теме диссертационной работы опубликовано И печатных работ. Список приводится в конце автореферата.

Структура и объем работы. Диссертационная работа состоит из введения, четырех глав, заключения, списка литературы из 107 наименований и трех приложений. Основная часть работы изложена на 144 страницах машинописного текста, содержит 15 рисунков и 53 таблицы.

ОСНОВНОЕ СОДЕРЖАНИЕ РАБОТЫ

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

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

1. Большая сложность;

2. Высокая связность элементов;

3. Высокая степень параллельности выполняемых потоков управления,

усложняющая анализ возможных сценариев развития вычислений;

4. Высокие требования по безопасности и надежности;

5. Невозможность полного тестирования;

6. Взаимодействие с объектами управления;

7. Реальный масштаб времени.

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

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

представить характерную для них логику управления, устраняя при этом избыточное описание информационной обработки. Проанализированы модели диаграмм потоков данных (dataflow), управляемые временем модели (time triggered), синхронно-реактивные модели (SR), модели дискретных событий (Discrete Event), сети процессов (Process Networks), модели рандеву (Rendezvous) и модели на основе автоматов конечных состояний (Finite State Machine).

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

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

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

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

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

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

Для достижения поставленной цели необходимо решить следующие задачи:

1. Конкретизировать область и типы объектов СПО в составе ПО ИУС;

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

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

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

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

6. По возможности усовершенствовать базовый метод в части представления требований верификации и сокращения объема пространства состояний;,

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

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

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

Во второй главе для уточнения области исследования и типов объектов СПО введено следующее понятие:

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

Операционная среда является той частью СПО, которая создается разработчиками самостоятельно. Таким образом, именно операционная среда является наиболее вероятным объектом исследования при помощи методов построения и верификации моделей СПО.

Проведенный анализ, в котором исследовались стандарты SCEPTRE, POSIX 1003.1, операционные системы QNX 4.2x, Lynx 4.0, MS Windows 5.0, Red Hat Linux и СПО систем без использования операционных систем (OS-less systems), позволил разработать открытую классификацию элементов СПО. Элементы разбиты на 2 категории и сгруппированы следующим образом:

1. Готовые объекты, предоставляемые операционной системой, или средой разработки:

а. Обработчики прерываний; b. Заместители (proxy);

с. Отложенные вызовы (DPC); d. Обработчики сигналов;

е. Фоновые потоки и функции; ... и другие;

2. Объекты, самостоятельно создаваемые разработчиком:

а. Очереди сообщений; b. Буфера;

с. Стеки; d. Обработчики событий;

е. Планировщики прикладных потоков; ... и другие. Базовый метод моделирования СПО выбирался из методов, использующих недетерминированные автоматы конечных состояний, поскольку они:

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

СПО;

2) предоставляют широкие возможности для формального анализа при верификации требований.

Автомат конечных состояний представлен как {S,s0,L,T,F)J где S-ограниченное множество состояний, начальное состояние

s0 eS,¿-ограниченное множество меток, Г-множество переходов, TçzfSxLxS), F-ограниченное множество конечных состояний, причем FçS.

Для детерминированных автоматов конечных состояний справедливо: VsVl,((s,l,s') е 7a(î,/,s") 6 Т) ->îW. Это условие не выполняется для недетерминированных автоматов.

В результате исследования в качестве базового был выбран метод G.Holzmann, использующий инструмент SPIN (Bell Labs). Близким по возможностям признан метод, разработанный в университете Carnegie Mellon, и использующий инструмент SMV.

Система SPIN свободно доступна для коммерческого использования, поставляется в виде открытых исходных текстов на С, что дает возможность ее использования на различных инструментальных платформах. Модель ПО описывается на языке PROMELA. Требование верификации в системе SPIN формулируется в синтаксисе линейной темпоральной логики (Linear Temporal Logic), которая затем автоматически транслируется в -автомат Buchi.

Пример требования: Всегда после события а случается событие !g, которое происходит раньше, чем событие b.

Каждое событие может быть представлено логическим условием или состоянием объекта модели:

tidefine a (qWriteIrp?[writeReq,J) tidefine b (was Write=-true) tidefine g (was Write && IE)

Запись требования в линейной темпоральной логике: [](я—W>)). Система SMV свободно доступна для. образовательного и исследовательского использования. Коммерческое использование возможно при заключении специального соглашения. Модель описывается на языке SMV. Требования верификации представляются в синтаксисе логики вычислительного дерева (Computational Tree Logic).

Пример требования: Всегда событие (qWriteIrp=l) происходит до события (Dev.wasWrite=l).

Запись требования в логике вычислительного дерева

Е{АГ(д№гИе1гр) иОеу.ыазН'гНе].

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

1. Недостаточно учтена специфика СПО ИУС:

a. Ориентация на верификацию протоколов, а не СПО;

b. Высока трудоемкость построения моделей СПО ИУС;

c. Высока сложность построения требований верификации СПО;

2. Недостатки при использовании в реальных условиях разработки СПО ИУС:

a. Отсутствие средств получения формализованного перечня входных и выходных данных;

b. Отсутствие средств контроля версий и хранения истории;

c. Ограниченные возможности редактора моделей.

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

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

Обоснована целесообразность применения в расширенном методе дополнительных операторов темпоральной логики. Ниже показана связь дополнительных операторов с базовыми операторами линейной темпоральной -логики:

Оператор К:

1аЯЬ=а-^оЬ (2)

Оператор Р:

аРЫЦаЩ (3)

Введение операторов W,R,P позволяет повысить выразительность записи типовых требований для СПО ИУС. Данные операторы используются в протоколах верификации.

Ограничения области действия требований -

□Отсутствие 0(1а)

□Существование <>а

□Ограниченное существование (!а \Л/ (а \Л/ (!а П'а))))

□Ответ а1ЧЬ=П(а -> <>Ь)

□Универсальность []а

□Предшествование аРЬ

Образцы отображения требований на области действия

Ответ Ограниченное существование

<1 отвечает иа в Переход » в осуществляется по меньшей мере 2 раза

г-__ П U -> 04> Гя4ми* <•• W (Я Ш (•!« <• «* |)t«l)ll

п^я « Os -> ((!• * to» U (а 1 ((• 4 )с| О (а 1 (<'• * ♦«» О (в | ((к * foi О |в 1 <•« 0 «1)1111)1)

П«р»яс Ofl -> (• -> (la О (4 4 !«>)! О •

Пм ъ ОЪ -> (fb 0 <Ь • (U W <* V (Г* « <• W [)(*))>)))

Пшгк 1Kb -> (К* -> <Х»> )

kfc««jr Ь ш С|((Ь 4 О«) ->(!♦• 4 let Q <в | (<» 4 to) О (в I <»*• 4 let 0 (в | <(1 4 1в> 9<в | (1* О >|)Ш|)|||

Мввауьв ^ [) {<Ь С Га ft -> U -> <•« О <4 « !с)Н Ос»

Пмм к «* в [)<Ь -> <<•» 4 »с» О <« I |(» « lo> V (о \ СП» 1 Is) О |а | <|* 4 1в) О to i и» v в) t (ummm

Пмм к«« О № Ь to -> <U -> <»• « v 14 4 fcl)) * «>

Рис.1

При построении и верификации моделей СПО ИУС была отмечена необходимость накопления и обработки протоколов верификации, связанная с итеративным характером процесса. В базовом методе отсутствуют рекомендации по решению данного вопроса. Для решения задачи была разработана оригинальная структура каталогов, позволяющая обеспечить накопление, хранение и удобную обработку протоколов. Данная структура каталогов согласуется с современными системами контроля версий ПО, в частности с Source Safe, CVS, CM Telelogic Synergy. Этот результат также создает предпосылки для интеграции инструментов расширенного метода с системами контроля требований (например, с Telelogic Doors).

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

генерации каркаса реализации СПО автоматизированными Процедура построения результат-модели представлена на рис.2.

средствами.

Рис.2

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

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

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

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

В конце главы подведены основные итоги.

Рис.3

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

При выполнении экспериментов были исследованы модели драйверов операционных систем Windows NT, QNX 4.25, Lynx 4.0, DOS 6.22, а также модели механизма арбитража активности резервированных модулей управления устройствами автоматики, доступа потоков к разделяемому ресурсу с синхронизацией через семафор и мютекс, многопоточных систем обработки запросов с динамическим созданием сервисного потока и выделением сервисного потока из пула, системы выдачи ответственных команд управления устройствами и другие.

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

Вероятность ошибок при предъявлении требований снизилась в среднем на 25%, а для требований с ограниченной областью видимости на 45%.

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

Сравнение характеристик расширенного метода и метода на основе 8МУ проводилось по трудоемкости и времени исследования, объему использованной памяти и времени верификации требований.

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

Главу завершают выводы по изложенному материалу.

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

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

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

proctypc CMJ>Levell(byte ID;cliu qTX^RX)

{byte p.c*; /»local copies*/

do

:: atomic (p-P]ID|; c-qiD|; a-U|ID|;) IT ::suteLevdl|ID|—a f»U->

¡r:: alone < (((c—fake) || (c—true)) && /"CAN.L*/

((»—Z) 11 <«—false))) -> stateUvdlllDHJocal; I = atonic ( <((p—Z) U (p—the)) ¿4 (c—Z) 4A /*CAN R*/

«r-blsc)|(>—trae))>| ((p—trae) && (c—Z) 44 (a—trae)) II

(((c—raise) g (c—Ir«)) 44 (a—trae)) -> stateLevdl [lDl-tjjun ( n ebe •> skip; II; :: stiteLeve 1111D1—»local oiT:: atooac ((«c—Z) 44 (a—Z)) I fCAH_fl

((p—trae) 44 <c—Z) 44 (a—Take))) -><t»teLevdl|lU|-lf«il;) x atofaic ( ((|J>—Z) || (p—bbe)) 44 (c—Z) 44 /*CAN RV

((a—raise) I («—trae») II ((p—trae) 44 (c—Z) 44 (r—trae)) ||

(((c—blse) II (c—trae)) U (a U at)) -> stateLavdl |JO|-»_p«ir; ) :: tfa«-> /»local mode activity sdectioo*/

. ir::atoaac I<C—bkc)£4((a—Z)||(a—blse))-> lbtAethe|IDl-blsci/*possi«e*/) :: atomic f(e-tnie) &&((•—Z) I («—trae))-> Ia(Active|ID|-tnK; /*activt'l ) :: else -»lev; G; 0; — fi; ad;)

Рис.4.

ОСНОВНЫЕ РЕЗУЛЬТАТЫ РАБОТЫ И ВЫВОДЫ

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

следующем:

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

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

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

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

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

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

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

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

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

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

Эффективность предложенного в работе расширенного метода построения и

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

успешным использованием в реальных проектах по разработке ПО ИУС.

СПИСОК РАБОТ, ОПУБЛИКОВАННЫХ ПО ТЕМЕ ДИССЕРТАЦИИ

1. Окулевич В.В. Разделение системных и прикладных задач при разработке информационно-управляющих систем // Научно-технический вестник СПбГИТМО(ТУ), выпуск 10, СПб.СПбГИТМО(ТУ), 2003 г., С. 95-98.

2. Окулевич В.В. Исследование операционных сред прикладных задач в информационно-управляющих системах // Научно-технический вестник СПбГИТМО(ТУ), выпуск 6, СПб:СПбГИТМО(ТУ), 2002 г., С. 92-94.

3. Окулевич В.В., Платунов А.Е. Исследование и разработка операционных сред прикладных задач в информационно-управляющих системах // Политехнический симпозиум «Молодые ученые промышленности Северозападного региона». Тез. докл. ноябрь 2001г.- СПб., 2001.- С. 25.

4. Окулевич В.В., Самохвалова О.Г. Использование стандартных библиотек во встроенных системах (на примере стандартной библиотеки языка С++) II Научно-технический вестник СПбГИТМО(ТУ), выпуск 10, СПб:СПбГИТМО(ТУ), 2003 г., С. 112-115.

5. Окулевич В.В., Самохвалова О.Г. Внедрение и поддержка новых технологий в процессе разработки ПО // Телематика 2003. Тез. докл. конф. 14-17 апреля 2003г.- СПб., 2003.- Т. 1.- С. 283-284.

6 Окулевич В.В., Самохвалова О.Г. Повторное использование механизмов операционной среды в информационно-управляющих системах // Политехнический симпозиум «Молодые ученые промышленности Северозападного региона». Тез. докл. декабрь 2002г.- СПб., 2002.- С. 69-70.

7. Окулевич В .В., Самохвалова О.Г. Повторное использование операционных сред при создании ПО СРВ // Наука. Техника. Инновации. Тез. докл. конф. 5-8 декабря 2002г.- Новосибирск, 2002.- Ч. 2. - С. 19-20.

8. Окулевич В.В., Самохвалова О.Г. Проектирование операционных систем реального времени на базе архитектурных шаблонов // Современные технологии. Сборник научных статей. СПб.:СПбГИТМО(ТУ), 2001.- С. 135-138.

9. Окулевич В.В., Самохвалова О.Г., Платунов А.Е. Разработка программного обеспечения встроенных систем с использованием стандартной библиотеки языка С++ // Политехнический симпозиум «Молодые ученые промышленности Северо-западного региона». Тез. докл. 18 апреля 2003г.- СПб., 2003.- С. 13-14.

10. Окулевич В.В., Самохвалова О.Г., Платунов А.Е. Автоматизация процессов повторного использования и реинжиниринга в разработке программного обеспечения систем реального времени // Политехнический симпозиум «Молодые ученые промышленности Северо-западного региона». Тез. докл. ноябрь 2003г.- СПб., 2003.- С. 13.

11. Окулевич В.В., Самохвалова О.Г., Платунов А.Е. Использование инкапсуляции, наследования и полиморфизма при создании программного обеспечения систем реального времени // Современные технологии. Сборник научных статей. СПб.:СПбГИТМО(ТУ), 2003.- С. 128-132.

Тиражирование и брошюровка выполнены в Центре "Университетские Телекоммуникации" Санкт-Петербург, Саблинская ул , 14 Тел (812) 23346-69 Лицензия ПДЛ № 69-182 от 26 11 96

Оглавление.

Введение.

Глава 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. Это позволило повысить комфортность и сократить количество ошибок при разработке и исследовании модели.

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

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

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

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 факс: 356-01-41, тел./факс:355-16-93 e-mail: MIKE@VNIIRA.SPB.SU1. АКТ О ВНЕДРЕНИИ

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. ТЕЛ: (812) 168-8631 ФАКС: (812) 312-13231. АКТ О ВНЕДРЕНИИ

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

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

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

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

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

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

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

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

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

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

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

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

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