Содержание к диссертации
Введение
Глава 1. Анализ методов повышения качества и надежности СПО ИУС 8
1.1. Специфика СПО ИУС 8
1.2. Методы повышения качества и надежности ПО ИУС 16
1.2.1. Использование образцов17
1.2.2. Тестирование. 18
1.2.3. Повторное использование компонент 20
1.2.4. Использование средств автоматической генерации кода 20
1.2.5. Использование средств сквозного цикла разработки 22
1.2.6. Использование систем контроля требований 22
1.2.7. Построение и верификация моделей 23
1.3. Построение и верификация моделей СПО ИУС 25
1.3.1. Модель СПО 25
1.3.2. Моделирование СПО 27
1.3.3. Верификация моделей СПО 32
1.3.4. Современные средства построения и верификации моделей ПО 36
1.4. Постановка задачи 45
Глава 2. Методы построения и верификации моделей СПО ИУС... 48
2.1. Основные понятия. Классификация объектов СПО ИУС 48
2.2. Выбор базового метода построения и верификации моделей 56
2.3. Анализ базового метода построения и верификации моделей ПО 58
2.4. Метод построения и верификации моделей СПО ИУС 64
2.4.1. Входные данные метода 64
2.4.2. Выходные данные метода 65
2.4.3. Определение и классификация требований 66
2.4.4. Общая последовательность этапов метода 68
2.4.5. Специфика этапов метода в зависимости от типа модели СПО 73
2.4.5.1. Особенности при исследовании архитектуры СПО 73
2.4.5.2. Особенности при исследовании КВМ СПО 75
2.5. Особенности метода построения и верификации моделей СПО ИУС 77
2.5.1. Выбор форматов для этапа построения моделей 77
2.5.2. Выбор форматов отчетов верификации 82
2.5.3. Дополнительные операции темпоральной логики 84
2.5.4. Образцы требований с различными областями видимости 85
2.5.5. Интеграция cMSDev 87
2.5.6. Интеграция с системой контроля версий 88
2.5.7. Классификация элементов моделей 89
2.5.8. Выбор формата описания элементов моделей 90
2.5.9. Таблица описания библиотеки элементов 91
2.6. Библиотека элементов моделей 93
Выводы 106
Глава 3. Исследование характеристик методов построения и верификации моделей СПО ИУС 107
3.1. Исследование базового и расширенного методов 108
3.2. Исследование расширенного метода и метода на основе SMV 114
Выводы 118
Глава 4. Исследование и разработка моделей СПО ИУС 120
4.1. Исследование архитектуры СПО (модель драйвера Windows NT)... 120
4.2. Исследование критически важного механизма арбитража активности резервированных модулей 125
Выводы , 131
Заключение 132
Список литературы 135
Приложение 1 145
Приложение 2 147
Приложение 3 152
- Современные средства построения и верификации моделей ПО
- Анализ базового метода построения и верификации моделей ПО
- Исследование расширенного метода и метода на основе SMV
- Исследование критически важного механизма арбитража активности резервированных модулей
Введение к работе
Информационно-управляющие системы (ИУС) востребованы современным рынком, поскольку их применение помогает решать задачи в самых различных областях человеческой деятельности. Использование ИУС позволяет повышать эффективность хозяйственной и экономической деятельности, сберегать ресурсы и улучшать условия жизни человека. Автоматизация процесса проектирования программного обеспечения (ПО) ИУС является важной задачей, позволяющей улучшить характеристики, как конечного изделия, так и самого процесса разработки.
При создании ПО ИУС, в том числе системного ПО (СПО), существует ряд проблем. Одной из основных проблем является повышения качества и надежности ПО. Перспективным способом решения данной задачи является построение и верификация моделей ПО ИУС, позволяющая делать математически доказанные выводы о выполнении требований безопасности и надежности для сложных систем, которые не могут быть исследованы другими методами.
В настоящее время существует ряд методов построения и автоматизированной верификации моделей ПО ИУС, однако их использование на практике затруднено из-за сложности применения методов и высокой стоимости инструментов. Кроме того, существующие методы недостаточно полно учитывают особенности СПО ИУС. Между тем именно в СПО, за счет независимости от решаемых прикладных задач, наблюдается высокий коэффициент повторного использования элементов моделей и требований верификации между различными разработками. Отмеченные факторы позволили сформулировать целью работы создание метода построения и верификации моделей СПО ИУС, учитывающего особенности процесса разработки СПО ИУС и обладающего невысокой стоимостью использования, применимого в реальных проектах по созданию ИУС.
5 В соответствии с поставленной целью в работе были решены следующие задачи:
Выполнена оценка состояния проблемы и анализ современных методов верификации программного обеспечения;
Выявлены специфические особенности системного программного обеспечения ИУС;
Разработан метод построения и верификации моделей СПО ИУС, использующий в качестве основы метод G. Holzmann [83] и соответствующий инструмент SPIN;
Разработанный метод применен в ряде проектов, что позволило получить положительные результаты по качеству и скорости создания СПО ИУС;
Выполнена оценка эффективности применения предложенного метода для исследования системного программного обеспечения ИУС в сравнении с другими методами верификации моделей.
При решении поставленных задач использовались методы теории автоматов конечных состояний, методы истощающей и вероятностной верификации моделей, аппарат темпоральной логики, метод экспертных оценок, методы дискретного программирования и математического моделирования.
Научная новизна работы состоит в следующем:
Разработан расширенный метод построения и верификации высокоуровневых моделей СПО ИУС, базирующийся на методе G. Holzmann. Метод отличается от известных расширенным составом операторов представления требований верификации и механизмами ограничения областей видимости.
Определен ряд понятий: операционная среда, критически важные механизмы СПО, архитектура СПО в контексте процесса верификации,
начальная модель, результат-модель, а также разработана классификация элементов СПО ИУС.
Разработана технология автоматизированной верификации моделей СПО ИУС на основе расширенного метода, включающая работу с таблицами требований и единиц моделирования, алгоритмы построения модели, метод получения результат-модели.
Произведена классификация элементов моделей СПО ИУС по способу активации исполнения, что позволило структурировать сведения о поведении элементов модели.
Показана возможность и целесообразность использования результатов моделирования в форматах расширенного метода для последующего этапа реализации СПО ИУС.
Практическая ценность работы была подтверждена при применении автоматизированного инструментального комплекса на основе предложенного метода к решению практических задач разработки ИУС. При этом наблюдалось снижение времени верификации моделей на 10%, а также сокращение времени построения моделей системного программного обеспечения на 20-40%.
Отмечено сокращение числа ошибок при составлении требований верификации с ограниченной областью видимости на 45% за счет использования образцов.
В настоящее время результаты работы используются при решении научно-практических задач разработки СПО ИУС. Объем файлов истории изменения моделей, отчетов и протоколов верификации составляет более 2.5 Мбайт. При этом осуществлена проверка более 500 требований верификации в режимах истощающей верификации, верификации со сжатием пространства состояния и вероятностной верификации.
Разработанный метод был использован при реализации СПО арбитража активности резервируемых модулей управления устройствами радиолокатора
7 МВРЛ-СВК, проектировании драйвера управления связевым оборудованием системы КТС "Тракт" для Windows NT 5.0 и др.
По результатам работы было сделано 10 докладов на 9 конференциях. Всего по теме диссертации выполнено 11 публикаций. Доклад на Политехническом симпозиуме «Молодые ученые - промышленности Северозападного региона» 17 декабря 2002 года был удостоен звания лучшего доклада. За активное участие в конференциях Политехнического симпозиума 20 февраля 2004 года автор работы награжден медалью «За преданность науке», удостоверение № 54.
Часть материалов диссертации вошла в курс лекций и лабораторных работ по дисциплине «Операционные системы реального времени» кафедры ВТ СПБГУИТМО.
Предложенный в работе метод рекомендуется к применению разработчиками системного программного обеспечения ИУС, поскольку позволяет повысить качество и надежность ИУС за счет обнаружения алгоритмических ошибок и ошибок специфицирования на ранних этапах разработки, сократив при этом время построения и верификации моделей по сравнению с базовым методом. Метод обладает низкой стоимостью при внедрении и использовании, а также ориентирован на применение в условиях реального цикла проектирования.
s Глава 1. Анализ методов повышения качества и надежности СПО ИУС
1.1. Специфика СПО ИУС
Существует ряд проблем при разработке программного обеспечения, и в частности СПО. Исследованию этих проблем посвящены такие фундаментальные работы, как [44] [65]. В настоящее время острота этих проблем увеличилась [2]. Появились работы, в которых даже название свидетельствует о непростом состоянии дел в отрасли производства программного обеспечения [12]. Поэтому большой интерес представляет поиск путей преодоления данных проблем.
По числу сложностей и проблем при разработке программного обеспечения одной из наиболее сложных областей является разработка программного обеспечения ИУС [91].
Информационно-управляющие системы — это «системы для управления и сбора информации, работающие в реальном масштабе времени» [16]. При создании программного обеспечения для ИУС кроме проблем, типичных для разработки обычного программного обеспечения, приходится учитывать дополнительные требования, предъявляемые к процессу и результату разработки из-за специфики ИУС. Автоматизация процесса проектирования программного обеспечения (ПО) ИУС и разработка систем САПР ПО ИУС являются важными задачами, позволяющей улучшить характеристики конечного изделия и процесса разработки.
Программное обеспечение ИУС разделяют, по меньшей мере, на 2 класса: системное и прикладное. Определим понятие СПО.
«СПО - программное обеспечение, необходимое для организации выполнения прикладных программ, но которое при этом не относится к конкретным приложениям» [87]. Прикладное программное обеспечение
9 осуществляет решение прикладных задач, важных для конечных пользователей системы.
С точки зрения данной работы, СПО, в свою очередь, можно разделить на самостоятельно разработанное СПО и СПО сторонних производителей. СПО сторонних производителей можно далее разделить на коммерческое СПО и свободно поставляемое СПО. Иначе, СПО сторонних производителей можно разделить на СПО с открытыми исходными текстами и на СПО с закрытыми исходными текстами. Некоторые производители СПО готовы предоставлять исходные тексты на условиях дополнительной оплаты. Исходные тексты СПО могут быть необходимы при сертификации изделия, в составе которого используется СПО, для детального исследования характеристик поведения СПО в составе ИУС и т.п.
Также в контексте данной работы целесообразно определить ряд понятий, так или иначе связанных с СПО ИУС. Вычислительная платформа.
Вычислительная платформа - это набор готовых аппаратно-программных средств, использующийся в качестве основы для функционирования самостоятельно реализованных элементов разработки. В ходе разработки ИУС не происходит значительной модификации вычислительной платформы. Как правило, вычислительная платформа представляет собой набор готовых изделий, которые могут настраиваться в соответствии с определенными правилами. По настройке и использованию каждого элемента вычислительной платформы, как правило, существует исчерпывающая документация. Состав средств, образующих вычислительную платформу может изменяться в зависимости от конкретных условий разработки. Понятие вычислительной платформы, используемое здесь, близко к понятию системы времени исполнения (run time system), используемому в технологии ROOM [102].
«Нижние уровни в вертикальной структуре предоставляются системой времени выполнения. Эта система охватывает базовый набор примитивных
10 сервисов, которые могут быть расширены определяемыми пользователем сервисами. Этот нижний уровень реализован в языках программирования окружения узла (host environment). С помощью перепрограммирования этого уровня на различных платформах, проект может быть портирован в разнородные вычислительные системы» [102]. Операционная система.
Операционные системы традиционно относятся к СПО. Операционная система - это программное обеспечение, которое предоставляет некоторый сервис и выполняет ряд функций. Сервис, предоставляемый операционной системой:
Коммуникация (межпроцессное взаимодействие);
Синхронизация (синхронизация процессов);
Контроль и планирование задач;
Управление памятью;
Управление прерываниями и оборудованием ввода/вывода;
Высокоуровневый интерфейс ввода/вывода и управления периферийными устройствами;
Управление файлами;
Управление транзакциями (сообщениями и передачами данных);
9. Обработка ошибок и исключений;
10.Управление временем.
Функции операционной системы:
Выделение памяти и адресация объектов;
Создание и удаление объектов;
Доступ к другим машинам. Данный список построен на основе [4].
Определим для дальнейшего использования понятие архитектуры программного обеспечения. Фактически, в настоящее время не существует стандартного, универсального и общепринятого определения этого термина в
приложении к вычислительной технике. Это, безусловно, затрудняет использование данного понятия при разработке систем.
Следует разделять понятия архитектуры системы и архитектуры программного обеспечения. Подробнее обсудим эти понятия.
Известны следующие определения.
«Архитектура программного обеспечения - это ряд значительных решений об организации программной системы, выборе структурных элементов и их интерфейсов, с помощью которых собирается система, а также их поведение во взаимодействии с этими элементами, объединение этих структурных и поведенческих элементов в большие системы и архитектурный стиль этой организации - этих элементов и их интерфейсов, их взаимодействия и их объединения» [64].
«Архитектура программного обеспечения - это абстрактная спецификация системы, состоящая в основном из функциональных компонент, описанных в терминах их поведения и интерфейсов, а также межсоединений компонент» [86].
«Программная архитектура системы определяет высокоуровневую структуру, определяющую ее общую (в ориг. англ. "gross") организацию как объединение взаимодействующих компонент. Хорошо определенная архитектура позволяет инженеру составлять мнение о свойствах системы на высоком уровне абстракции. Типичные свойства, с которыми необходимо считаться, включают протоколы взаимодействия, пропускную способность и задержки, положение центральных хранилищ данных и предполагаемых направлений эволюции (системы)» [81].
«Программная архитектура была предложена как многообещающий подход для того, чтобы заполнить разрыв между требованиями и реализацией в проектировании сложных систем. Программная архитектура описывает общую организацию системы в терминах ее компонент и их взаимодействия» [93].
«Программная архитектура программы или вычислительной системы — это структура или структуры системы, которые включают программные компоненты, внешне видимые свойства этих компонент и отношения между ними.
Под внешне видимыми свойствами, мы подразумеваем те, о которых могут делать предположения другие компоненты, такие как предоставляемые сервисы, характеристики производительности, обработка отказов, использование разделяемых ресурсов и т.п. В этом определении указывается, что программная архитектура должна абстрагироваться от некоторой информации о системе (иначе нет причин определять архитектуру, мы бы просто говорили обо всей системе), а также предусматривать достаточно информации для того, чтобы быть основой анализа, принятия решений и, следовательно, сокращения рисков.
Рассмотрим некоторые последствия из этого определения подробнее.
Во-первых, архитектура определяет компоненты. Архитектура содержит информацию о том, как компоненты взаимодействуют друг с другом. Это означает, что архитектура специально пропускает содержательную информацию о компонентах, которая не относится к их взаимодействию.
Во-вторых, определение делает ясным, что системы могут состоять больше чем из одной структуры, и что ни одна структура не претендует на то, чтоб неопровержимо быть архитектурой. Определение намеренно не указывает, что такое архитектурные компоненты и отношения. Является ли программный компонент объектом? Процессом? Библиотекой? Базой данных? Коммерческим продуктом? Им может быть все перечисленное и больше.
В-третьих, определение подразумевает, что каждая программная система имеет архитектуру, поскольку каждая система может быть представлена в виде компонент и отношений между ними.
В-четвертых, поведение каждой компоненты является частью архитектуры настолько, насколько это поведение может быть обозримо или
ІЗ различимо с точки зрения другого компонента. Это то поведение, которое позволяет компонентам взаимодействовать друг с другом, являющееся ясной частью архитектуры. Следовательно, большинство рисунков из «квадратов и стрелочек», которые проходят как архитектуры, фактически не являются архитектурой вовсе. Это просто рисунки из «квадратов и стрелочек» » [62].
«Программная архитектура - это множество концепций и проектных решений о структуре и текстуре программного обеспечения, которые должны быть сделаны до начала параллельной инженерной разработки для того, чтобы обеспечить эффективное удовлетворение архитектурно значимых явных функциональных и качественных требований и неявных требованиях семейства продукции, проблемы и области решений» [88].
Определение архитектуры, как «абстрактной спецификации», приведенное в работе [86] способствует неправильному пониманию термина, из-за указания на такую характеристику спецификации, как абстрактность.
Вообще говоря, существуют следующие типы абстракции [34]:
Изолирующая - вычленяющая исследуемое явление из некоторой целостности;
Обобщающая - дающая обобщенную картину явления;
Идеализация - замещение реального эмпирического явления идеализирующей схемой.
Именно то, что понятие абстракции может восприниматься как идеализирующая абстракция, обуславливает неоднозначную трактовку понятия.
Кроме того, в контексте широко распространенной объектно-ориентированной технологии разработки программного обеспечения, понятие «абстрактный» применяется к тем объектам, экземпляр которых не может быть создан в действительности (см., например [41]). Предлагаемый метод предназначен в первую очередь разработчикам программного обеспечения,
14 работающим, в том числе, и с объектно-ориентированными технологиями. Таким образом, создаются предпосылки к тому, что использование понятия «абстрактный» будет неверно истолковано, а архитектура будет восприниматься как оторванная от действительности сущность.
Архитектура и структура
Отличие архитектуры от структуры состоит в том, что структура не включает в себя поведенческой составляющей и не акцентирует внимание на способе соединения элементов.
Одним из самых емких определений является следующее. «Структура (от лат. structure - строение, расположение, порядок) - это совокупность устойчивых связей объекта, обеспечивающих его целостность и тождественность самому себе, т.е. сохранение основных свойств при различных внешних и внутренних изменениях» [34]. Данное определение говорит о наличии связей внутри объекта, и отмечает их значимую роль в образовании целостной и постоянной сущности.
Отметим, что в архитектуру программного обеспечения должно входить значительно больше аспектов, чем в структуру программного обеспечения.
Понятие архитектуры в процессе разработки ИУС
В процессе разработки архитектура программного обеспечения играет значительную роль. Во-первых, архитектура должна содержать декомпозированную функцию системы. В архитектуре явно представлены компоненты, каждый из которых отвечает за некоторую функцию в системе. Такое архитектурное представление системы используется в процессе разработки для планирования работ, распределения заданий и определения зон ответственности в коллективе разработчиков.
Во-вторых, архитектура содержит способы интеграции компонент. Таким образом, акцентируется внимание разработчиков на том, что требуется работа
15 не только по реализации компонент архитектуры, но еще и по их интеграции (способ интеграции).
В-третьих, архитектура содержит в концентрированном виде основные проектные решения. Эти решения бывает целесообразно представлять в общем виде, чтобы все разработчики могли в случае необходимости составить свое представление о месте решаемой ими задачи в общей функции системы. «Большие программные системы требуют механизмов декомпозиции для того, чтобы сделать их понимаемыми. Разбивая систему на элементы, становится возможным судить об общих свойствах, понимая свойства каждой из частей» [59]. Такое понимание оказывается полезным в процессе разработки системы.
Однако следует помнить, что могут существовать некоторые соображения, в соответствии с которыми оказывается целесообразным скрывать проектную информацию (в том числе и архитектурное представление).
Включению в типовой цикл разработки фазы активной работы с понятием архитектуры мешают следующие факторы:
Отсутствие устоявшегося понимания термина архитектура;
Отсутствие (неразвитость) формальных способов спецификации архитектуры;
Отсутствие (неразвитость) способов и средств формальных оценок, анализа, проверок, тестирования архитектур и их сравнения;
Недостаточное количество средств разработки, включающее работу с архитектурными описаниями в сквозной цикл проектирования.
16 1.2. Методы повышения качества и надежности ПО ИУС
Одной из основных причин, усложняющей создание программного обеспечения, является его высокая сложность. Кроме того, ситуация усугубляется необходимостью взаимодействия с объектами управления в реальном масштабе времени с высокой степенью безопасности и надежности. Высокая степень параллелизма выполняемых процессов, ограниченные вычислительные ресурсы, сложность отладки, специфические режимы функционирования, необходимость использования компонент в виде черных ящиков и т.п. обостряют проблему. Становится практически невозможным на основании анализа реализации ПО ИУС удостовериться, что предъявляемые к системе требования выполняются на самом деле.
Использование средств автоматизации процесса разработки (САПР) ПО помогает уменьшить число ошибок, улучшить пользовательские качества применяемых технологий. САПР освобождают разработчиков от рутинных операций, повышая при этом производительность труда инженеров.
Если требование, предъявляемое к программному обеспечению, не выполняется, то имеет место ошибка. Можно сказать, что разработка программного обеспечения без ошибок является основной проблемой разработки всех видов программного обеспечения, в том числе и СПО.
В настоящее время существуют следующие способы уменьшения количества ошибок в программном обеспечении:
Использование образцов;
Тестирование;
Повторное использование компонент;
Использование средств автоматической генерации кода;
Использование средств сквозного цикла разработки;
Использование систем контроля требований;
Построение и верификация моделей.
1.2.1. Использование образцов
Каждый образец (паттерн), в соответствии с [6], состоит из четырех основных элементов
Имя. Ссылаясь на него, можно сразу описать проблему проектирования, ее решения и их последствия. Присваивание образцам имен позволяет проектировать на более высоком уровне абстракции. С помощью словаря образцов можно вести обсуждения в команде разработчиков, ссылаться на образцы в документации.
Задача. Описание того, когда следует использовать образец. При этом описывается не только задача, но и некоторый контекст.
Решение. Описание элементов проекта, отношений между ними и функций каждого элемента. Это достаточно абстрактное описание задачи проектирования и того, как она может быть решена с помощью некоторого обобщенного сочетания элементов.
Результаты. Следствия применения образца и компромиссы различного рода. Указываются требования к реализации образца, необходимых языках программирования и ресурсах.
Использование образцов означает, что при решении каждой задачи, возникающей в процессе разработки, не происходит ее решение «с нуля». Вначале разработчик осуществляет поиск подходящего решения задачи в некотором хранилище образцов. Таким образом, уменьшается количество неопределенности при решении задачи и, следовательно, уменьшается количество ошибок. Кроме того, образцы создают условия для накопления удачных решений. Мы рассматриваем образцы как один из способов повторного использования элементов разработок.
Однако, в [6] находим, что в их работу «не включено описание паттернов, имеющих отношение к параллельности, распределенному программированию и программированию систем реального времени. Отсутствуют также сведения и о паттернах, специфичных для конкретных предметных областей... вы не
18 узнаете, как строить интерфейсы пользователя, как писать драйверы устройств».
Исследование образцов, специфичных для систем реального времени показало, что существует значительная связь между предметной областью и образцами проектирования. Кроме того, в новаторских разработках невозможно использовать образцы. Выделение и накопление образцов требует дополнительных ресурсов. Отметим, что использование образцов создает предпосылки к уменьшению ошибок, но абсолютно не гарантирует того, что ошибки отсутствуют в образце и в реализации системы с использованием образца.
1.2.2. Тестирование
Тестирование программного обеспечения является детально разработанной областью. Следует отметить такие работы, как [18], [19], [13]. Существует множество подходов к тестированию программного обеспечения. При этом основная сложность состоит в том, что ПО реальных размеров, как правило, имеет большое количество состояний, поэтому обеспечить полное тестовое покрытие практически невозможно.
«Рассмотрим попытку тестирования тривиальной программы, получающей на входе три числа и вычисляющей их среднее арифметическое. Тестирование этой программы для всех значений входных данных невозможно. Даже для машины с относительно низкой точностью вычислений количество тестов исчислялось бы миллиардами. Даже имей мы вычислительную мощность, достаточную для выполнения всех тестов в разумное время, мы потратили бы на несколько порядков больше времени для того, чтобы эти тесты подготовить, а затем проверить. Такие программы, как системы реального времени, операционные системы и программы управления данными, которые сохраняют «память» о предыдущих входных данных, еще хуже. Нам потребовалось бы тестировать программу не только для каждого входного
значения, но и для каждой последовательности, каждой комбинации входных данных» [19].
Тестирование ПО ИУС затрудняется спецификой предметной области,
особенностями используемых вычислителей и сложностью подготовки тестов.
Кроме того, необходимость взаимодействия с реальными объектами
управления вносит существенные коррективы в процессы тестирования.
Например, существуют такие объекты управления, на которых отладка может
быть принципиально или практически невозможна (система управления
ядерным реактором, системы железнодорожной автоматики,
кардиостимулятор).
Попытка исчерпывающего тестирования программы, при котором выполняются все возможные пути, рассмотрена на рисунке 1.1.
Рис. 1.1. Возможные пути небольшой программы
«Кружками представлены последовательные сегменты, а стрелками -передачи управления (с помощью развилок или циклов). Модуль состоит из цикла, выполняемого от 0 до 10 раз, за которым следует развилка и за ней -второй цикл. В каждом цикле имеется ряд вложенных развилок, как это
20 показано на рисунке. Предполагая, что каждое решение полностью независимо от других (наихудший случай), можно оценить число путей в модуле примерно как 10Л18. Чтобы лучше представить себе это число, укажем, что возраст Вселенной оценивается в 4*10Л17 секунд» [19].
1.2.3. Повторное использование компонент
Проблемы повторного использования изучаются уже в течение длительного времени и, безусловно, в этой области получены значительные результаты. Повторное использование компонент означает, что успешные элементы предыдущих разработок включаются в новые проекты. Осуществляется как использование исходных кодов программ, так и использование готовых объектных и исполняемых файлов.
Разумеется, использование ранее оттестированных компонент способствует уменьшению числа ошибок в конечной системе. Однако, даже тот факт, что компонент уже когда-то прошел тесты, не гарантирует того, что в нем абсолютно отсутствуют ошибки. При включении в состав новой системы может проявиться часть ранее не обнаруженных ошибок внутри компонента. При этом встает вопрос, как поступить с предыдущими версиями компонента, которые уже включены в версии созданных ранее систем; следует ли изменять компонент, вошедший в предыдущие системы или нет?
1.2.4. Использование средств автоматической генерации кода
Перспективным направлением создания программного обеспечения, по мнению ряда авторов, является использование средств автоматической генерации кода на основе высокоуровневых спецификаций. К системам такого рода, например, относят языки визуального программирования. Бесспорным достоинством таких средств является простота использования. Как правило, такие средства предоставляют разработчикам несложный и наглядный
интерфейс, хорошо соответствующий проблемной специфике. В качестве примеров таких систем следует упомянуть RTWin для QNX 4.2х. Использование инструментов данного типа позволяет снизить требования к квалификации разработчиков, которая прямо пропорциональна их стоимости.
Однако при использовании таких средств для разработки программного обеспечения ИУС далеко не всегда удается добиться требуемого результата. Объективная сложность происходящих в ИУС процессов, специфика предметной области, требования к функционированию в реальном масштабе времени и взаимодействие с внешними устройствами усложняют создание систем автоматической генерации исполняемого кода.
Кроме того, для анализа функционирования и отладки таких систем требуется понимание внутренней организации исполняемого кода. При возникновении ошибочных ситуаций разработчику приходится переходить на уровень исполняемого кода, который создается системой автоматической генерации. Сложность анализа этого исполняемого кода высока, для выполнения данного анализа нужна высокая программистская квалификация.
Отметим также, что избыточность, неизбежно вносимая в конечную систему за счет использования высокоуровневых описаний предметной области, требует дополнительных ресурсов на этапе исполнения. Вдобавок, стоимость таких средств автоматической генерации весьма высока.
Снижение числа ошибок при использовании таких средств, по заверениям создателей, происходит за счет уменьшения, если не полного устранения необходимости низкоуровнего программирования. Повышение наглядности и простоты исходных описаний действительно способствует уменьшению числа ошибок и повышению прозрачности описания для анализа экспертами и разработчиками.
1.2.5. Использование средств сквозного цикла разработки
Многообещающим направлением, активно развивающимся в настоящее время, являются системы сквозного цикла разработки. Такие системы, как Rational Rose UML [14], TAU G2 [103], позволяют привнести в процесс разработки программного обеспечения новое качество. Многоуровневое (logical view, component view и других) или многоязыковое представление программного обеспечения позволяет повысить наглядность языковых описаний. Возможность генерации заготовок исполняемого кода на основе моделей и, наоборот, возможность построения моделей на основе существующего исполняемого кода, позволяют улучшить качество документации, упростить исследование и сопровождение программного обеспечения.
Дополнительные средства тестирования, которые могут поставляться в составе со средствами сквозного цикла разработки или отдельно, создают предпосылки для уменьшения количества ошибок в конечной системе.
Однако, сложность таких систем достаточно высока. Как правило, их использование требует существенных изменений в производственном процессе программного обеспечения ИУС, и СПО ИУС в частности. Автоматическая генерация кода в таких системах осуществляется на ограниченное количество вычислительных платформ, а в тех случаях, когда это возможно, описание обладает дополнительной избыточностью. Для успешного внедрения таких систем необходимы значительные затраты на обучение и использование. Данные системы требуют для своей работы значительных вычислительных ресурсов. Приходится также учитывать наличие, стоимость и качество поддержки (support). Эти факторы затрудняют, если не делают невозможным, использование таких систем при разработке СПО ИУС.
1.2.6. Использование систем контроля требований
Интересным является подход к разработке программного обеспечения, основанный на контроле требований. В числе таких систем следует упомянуть
23 пакет DOORS фирмы Telelogic. Данная система позволяет отследить выполнение требований, предъявляемых к конечной системе, во всей проектной документации, в том числе, и в исходном коде программ.
Данная система интегрируется с системами CM Synergy и Change Synergy, которые осуществляют хранение проектных файлов, контроль версий и управляют процессом разработки.
Сквозной контроль требований повышает прозрачность программного обеспечения, создает благоприятные условия для управления жизненным циклом программного продукта и приводит к уменьшению числа ошибок в программном обеспечении.
Однако стоимость систем контроля требований высока. Использование систем контроля требований вносит свои коррективы в процесс разработки программного обеспечения. Внедрение систем требует достаточно больших затрат, в том числе обучения персонала. Требуется создание и поддержка соответствующей инфраструктуры.
1.2.7. Построение и верификация моделей
Значительные усилия ученых и инженеров направлены на исследование методов и создание инструментов для построения и верификации моделей программного обеспечения в целом, и СПО в частности. Методы построения и верификации моделей позволяют уже на ранних этапах разработки получить модели элементов ПО ИУС и удостовериться, что ряд их свойств удовлетворяет предъявляемым к конечной системе требованиям. Полученные модели могут быть использованы в качестве основы для формализованных или формальных методов реализации ИУС, то есть использоваться в системах автоматической генерации кода и средствах сквозного цикла разработки.
Особенностью некоторых методов верификации моделей является возможность получения гарантированных сведений о поведении объекта моделирования (которым является ПО ИУС). Таким образом, становится
24 возможным получение формально подтвержденных сведений о функционировании ПО ИУС.
Моделирование — это основной способ исследования сложных объектов, к которым, безусловно, относится СПО. Возможность формальной обработки моделей СПО и их верификация чрезвычайно полезна при создании ИУС. Построение ПО, в том числе и СПО на основе формально обработанных моделей позволяет гарантировать (при определенных условиях) безошибочную работу ПО в составе ИУС.
Известно, что стоимость обнаружения и исправления ошибки прямо пропорциональна времени с момента начала разработки [36]. Таким образом, очевидно, что дешевле обнаруживать ошибки на ранних этапах разработки, нежели на поздних этапах. Необходимо отметить, что в ИУС с большой серийностью, стоимость исправления ошибки после выпуска серии изделий увеличивается во много раз (видимо, прямо пропорционально количеству выпущенных изделий). Существует ряд ИУС, в которых уделяется огромное внимание поиску и исправлению ошибок. Процесс создания таких систем требует высочайшей культуры разработки.
Яркий пример успешного использования анализа моделей ПО приведен ниже. «Встроенное программное обеспечение для 14-ой линии метро Meteor в Париже, в котором нет водителя, было формально спроектировано на основе метода В. 115000 строк спецификации, написанных на В, были скомпилированы в 87000 строк программы на ADA. Доказательство корректности, использовавшее интерактивное доказательство теорем, потребовало обработать вручную 27800 необходимых требований. Для этой цели 1400 правил должны были быть добавлены в систему доказательства и быть подтверждены. 900 требований было добавлено автоматически. С тех пор, пока метро запущенно, ни одной ошибки не было найдено ни во встроенном программном обеспечении, ни в спецификации В... Для приведенного примера 600 человеко/лет не будут преувеличенной оценкой трудоемкости задачи» [71].
Использование метода построения и верификации моделей СПО на ранних этапах разработки (до этапа реализации СПО) позволяет уменьшить число ошибок в СПО, и, таким образом, уменьшить затраты на обнаружение и исправление ошибок в конечном ПО. Кроме того, верифицированные модели СПО могут использоваться в качестве основы для последующих этапов разработки, в том числе, при реализации ПО и создании проектной документации.
Уменьшение ошибок на ранних этапах является критическим для ИУС, поскольку сложность готовых систем велика, что делает полное тестирование невозможным, В связи с этим построение и верификация моделей СПО является перспективным способом повышения качества и надежности ИУС. Кроме того, данный вопрос недостаточно разработан применительно к ПО ИУС в целом и к СПО ИУС в частности. В связи с этим, настоящая работа является исследованием, посвященным построению и верификации моделей СПО ИУС.
1.3. Построение и верификация моделей СПО ИУС
1.3.1. Модель СПО
Зафиксируем понятие модели СПО в контексте данной работы. Для этого воспользуемся определением модели в качестве основы.
«Модель: 1. образец (эталон, стандарт) для массового изготовления какого-либо изделия или конструкции; 2. устройство, воспроизводящее, имитирующее строение и действие какого-либо другого устройства в научно-производственных или спортивных целях» [34],
Рассмотрим определение модели применительно к решаемым задачам. Во-первых, важно отметить, что оба приведенных значения понятия «модель» используются при моделировании СПО ИУС. В самом деле, с одной стороны, в ходе моделирования СПО ИУС производится создание объектов, имитирующих (воспроизводящих) СПО ИУС. Это соответствует второму
26 значению понятия «модель». В ходе моделирования происходит исследование свойств моделей. Если свойства полученных моделей удовлетворительны, то они могут использоваться в качестве образца (эталона) при создании или модификации СПО ИУС. Таким образом, происходит использование модели СПО ИУС в первом значении приведенного выше определения.
Следует сделать несколько важных замечаний. Во-первых, в приведенном выше определении указывается, что модель подражает «какому-либо ... устройству». Применительно к моделированию СПО ИУС оказывается, что на практике модель СПО часто строится до того, как будет создано то устройство, которому подражает модель. Предлагается расширить определение модели СПО ИУС так, чтобы этот факт был явно отмечен. Во-вторых, обычно неявно подразумевается, что модель - это упрощенное описание объекта моделирования. Однако, как отмечено в [3], существуют модели, которые сравнимы или даже превосходят по сложности моделируемые объекты. В рамках данной работы под моделью будет пониматься упрощение объекта моделирования. В самом деле, в модели отражаются лишь важные с точки зрения решаемой задачи аспекты объекта моделирования. Если же отразить в модели все аспекты объекта моделирования, то модель вырождается в объект моделирования (становится тождественна ему). В тех же случаях, когда модель СПО ИУС оказывается субъективно (с точки зрения исследователя) сложнее системы, на это могут быть две причины:
Исследователь недостаточно хорошо владеет средствами моделирования, использование которых предполагает метод моделирования. В этом случае сложность модели объясняется сложностью восприятия средств моделирования самим исследователем;
Средства моделирования недостаточно хорошо подходят для простого выражения аспектов объекта моделирования, и для их выражения приходится использовать сложные конструкции, которые сложно воспринимать.
Зафиксируем определение модели СПО:
«модель СПО 1. образец для создания СПО; 2. описание, имитирующее строение и действие реального или возможного СПО в научно-производственных целях».
1.3.2. Моделирование СПО
Зафиксируем понятие моделирования СПО в контексте данной работы на основе понятия «моделирование».
«Моделирование - исследование каких-либо явлений, процессов или систем объектов путем построения и изучения их моделей, использование моделей для определения или уточнения характеристик и рационализации способов построения вновь конструируемых объектов» [34]. Данное определение может быть с успехом конкретизировано для определения моделирования СПО. Автор считает необходимым дополнить определение тем, что моделирование - это процесс.
«Моделирование СПО — это процесс исследования СПО путем построения и изучения моделей СПО, использования моделей СПО для определения и уточнения характеристик и рационализации способов построения вновь конструируемых объектов».
Существует ряд подходов к моделированию программного обеспечения ИУС. Ниже представлен их перечень в соответствии с [91]: 1. Диаграммы потоков данных (dataflow). В диаграммах потоков данных в качестве элементов используются неделимые вычисления, которые приводятся в действие при наличии выходных данных. Связи между элементами представляют поток данных от производящего элемента к потребляющему элементу. Примеры коммерческих систем: SPW (Cadence), Lab View (National Instruments). Синхронные потоки данных (Synchronous dataflow - SDF) являются частным ограниченным случаем с полезным свойством определения тупиковых ситуаций и граничного анализа. Выделяют также Boolean Dataflow (BDF) и Dynamic Dataflow (DDF), чьи
28 свойства относительно определения тупиковых ситуаций и граничного анализа слабее.
Управляемые временем модели (Time Triggered). Данная модель была использована при проектировании аппаратных архитектур. Примерами являются Scenic, SystemC. Язык программирования Giotto использовался также для моделирования программных систем, в которых преобладают периодические события. В нем используются машины конечных состояний, которые дают достаточную выразительность.
Синхронно/реактивные модели (Synchronous/Reactive - SR). В данных моделях вычислений соединения между компонентами представляют значения данных, которые передаются с глобальными тактами синхронизации, так же как в управляемых временем моделями. Однако, в данных моделях нет предположений о том, что все (или даже большая часть) сигналов иммет значение при каждом такте времени. Это модели эффективны при работе с параллельными моделями с нерегулярными событиями. Компоненты представляют отношения между входными и выходными значениями при каждом такте (при этом разрешается отсутствие значений), а также обычно частные функции с определенными техническими отношениями для того, чтобы осуществлялся детерминистический выбор. Сложные технологии компиляции позволяют чрезвычайно эффективное исполнение, которое может сократить все параллельное исполнение к последовательному. Примеры языков, которые используют синхронно/реактивную модель вычислений, включают Esterel, Signal и Lustre. Пример приложения, для которго идеально подходит данная модель - это управление протоколом token-ring (маркерный кольцевой доступ). Синхронно/реактивные модели отлично подходят для приложений с параллельной и сложной управляющей логикой. Приложения реального времени, к которым предъявляются требования безопасного функционирования, хорошо подходят к данной модели. Однако по причине
29 тесной синхронизации задач, некоторые приложения достаточно сложно выразить в данной модели, которая ограничивает альтернативы реализации и делает достаточно сложным моделирование распределенной системы. Кроме того, в некоторых реализациях из-за необходимости определения глобальной фиксированной точки на каждый такт синхронизации, приходится жертвовать модульностью.
Модели дискретных событий (Discrete Event - DE). В данной модели, соединения представляют множества событий, размещенных на шкале времени. Событие состоит из значения и штампа времени. Эта модель вычислений популярна при определении аппаратуры и имитации телекоммуникационных систем, была реализована во множестве имитационных окружений, языков имитации и языках описания аппаратуры, включая VHDL и Verilog. Как SR, в этой модели присутствует глобально определенное понятие времени, но в отличие от SR время имеет меру, в которой может время между событиями имеет значение. DE модели часто используются при проектировании сетей коммуникации. Также эти модели являются отличным описанием параллельной аппаратуры, хотя увеличение глобально определенного времени является проблемой. Ключевой недостаток данной модели в том, что ее относительно сложно реализовать в программном обеспечении, что подтверждается относительно сложной имитацией.
Сети процессов (Process Networks - PN). Общим случаем обработки параллельного программного обеспечения является такой, в котором компоненты являются процессами или потоками, которые взаимодействуют с помощью асинхронных, буферизируемых сообщений. Отправителю сообщения нет необходимости ожидать, пока получатель будет готов получить сообщение. Существует несколько вариантов данной технологии. Одним из способов, который использует детерминистические вычисления, являются сети процессов Kahn. В данной модели вычислений, соединения
зо представляют последовательности значений данных (токенов), а компоненты представляют функции, которые отображают входные последовательности в выходные последовательности. Определенные технические ограничения, налагаемые на данные функции, необходимы для удостоверения детерминизма, что означает полное определение данных последовательностей. Модель потоков данных является специальным случаем сетей процессов, которая конструирует процессы как неделимые действия актеров. Сети процессов отлично подходят для обработки сигналов. Они слабо связаны, и следовательно, относительно легко могут быть выполнены параллельно или сделаны распределенными. Сети процессов могут быть эффективно реализованы как в программном обеспечении, так и в аппаратуре. Ключевой недостаток моделей сетей процессов в том, что они не подходят для указания сложной управляющей логики. Управляющая логика указывается только значениями данных маршрутизации. 6. Рандеву (Rendezvous). При синхронной посылке сообщений компонентами являются процессы, обменивающиеся с помощью неделимых, мгновенных действий, называемых рандеву. Если два процесса должны взаимодействовать, и один первым достигает точки, в которой он должен взаимодействовать, тогда он приостанавливается до тех пор, пока другой процесс не станет готовым к взаимодействию. Неделимость (атомарность) означает, что два процесса одновременно вовлекаются в обмен, и этот обмен начитается и завершается за один неделимый шаг. Примеры моделей рандеву включают взаимодействующие последовательные процессы (Communicating Sequential Processes - CSP) Xoapa (Hoare) и вычисления взаимодействующих систем (Calculus of Communicating Systems - CCS) Милнера (Milner). Robin Milner работал в университете Эдинбурга (University of Edinburgh). Эти модели вычислений были реализованы во множестве языков параллельного программирования, включая Lotos и
ЗІ Occam. Данная модель достаточно хорошо подходит для приложений, в которых разделение ресурсов является ключевым элементом, например, для клиент-серверных баз данных, многозадачных систем или мультиплексирования аппаратных ресурсов. Возможные недостаток модели рандеву - это то, что поддержание детерминизма может быть сложным. Однако сторонники этого подхода считают способность модели к выражению недетерминистических вычислений сильной стороной.
Подписка и публикация (Publish and Subscribe). В этих моделях, связи между компонентами осуществляются через именованные потоки событий. Компонент, который является потребителем такого потока событий, регистрирует свой интерес к данному потоку. Когда создатель события передает событие в поток, потребитель уведомляется, что доступно новое событие. Далее, потребитель запрашивает сервер о значении события. Примеры таких моделей: Linda, JavaSpaces.
Модели непрерывного времени (Continuous Time). Физические системы часто могут быть промоделированы с использованием систем дифференциальных уравнений. Дифференциальные уравнения превосходно подходят для моделирования физических систем, с которыми взаимодействуют ИУС. Объединенное моделирование таких систем и программного обеспечения, которое взаимодействует с ними, важно при получении сведений о программном обеспечении. Такое объединенное моделирование поддерживается такими системами, как Simulink, Saber, Ptolemey II.
Машины конечных состояний (Finite State Machine — FSM). Все модели вычислений, которые были рассмотрены выше, параллельны. Часто полезно комбинировать эти параллельные модели иерархически с машинами конечных состояний, для получения модальных моделей. FSM отличаются от множества моделей в том, что они являются последовательными. Компонент данной модели имеет состояние, и только одно состояние может
32 быть активно в один момент времени. Связи между состояниями представляют переходы, или передачу управления между состояниями. Исполнение - это точно упорядоченная последовательность переходов между состояниями. Системы переходов являются общим случаем, в котором заданный компонент может представлять более чем одно заданное состояние. FSM отлично подходят для описания управляющей логики во встроенных системах, в частности, в системах с повышенными требованиями по безопасности. FSM незаменимы в глубоком формальном анализе, используя системы проверки моделей, что может помочь избежать неожиданного поведения. Более того, FSM модели легко отображаются как в аппаратную, так и в программную реализацию. Однако FSM модели имеют ряд ключевых недостатков. Во-первых, на самом фундаментальном уровне, они не настолько выразительны, как другие модели вычислений, описанные ранее. Они недостаточно богаты для описания любых рекурсивных функций. Однако, эти недостатки приемлемы в свете возможности формального анализа. Многие вопросы о проекте могут быть выяснены с помощью FSM и не выяснены для других моделей вычислений. Другой ключевой недостаток в том, что число состояний может быть очень большим даже в случае небольшой сложности. Это делает моделирование громоздким. Однако данная проблема может быть решена, используя FSM вместе с параллельными моделями вычислений. FSM могут быть иерархически скомбинированы с большим числом параллельных моделей вычислений. Примером таких систем может быть система Ptolemey П.
1.3.3. Верификация моделей СПО
Рассмотрим два важных понятия, которые также используются в работе. В классической работе Майерса [19] находим:
«Верификация — попытка найти ошибки, выполняя программу в тестовой, или моделируемой, среде».
«Валидация - попытка найти ошибки, выполняя программу в заданной реальной среде».
Там же находим ряд смежных понятий:
«Тестирование - процесс выполнения программы (или части программы) с намерением найти ошибки».
«Доказательство - попытка найти ошибки в программе безотносительно к внешней для программы среде».
«Отладка - деятельность, направленная на установление точной природы известной ошибки, а затем, на исправление этой ошибки».
К сожалению, в этих определениях используется понятие программы, а не понятие модели. Рассмотрим другие определения:
«Верификация - подтверждение на основе представления объективных свидетельств того, что установленные требования были выполнены» [8].
«Валидация - подтверждение на основе представления объективных свидетельств того, что требования, предназначенные для конкретного использования или применения, выполнены» [8].
Из этих определений следует, что валидация - это верификация требований, которые установлены с учетом специфики конкретного использования или применения. В исследовании в основном используется понятие верификации, поскольку работа не рассматривает конкретики применений СПО в тех или иных условиях.
Известно о том, что некоторые типы моделей ПО, могут быть эффективно использованы при решении задач верификации.
Определим понятие верификации СПО в том виде, в котором оно используется в работе.
«Верификация СПО - это подтверждение на основе предоставления объективных свидетельств того, что установленные требования к СПО были выполнены». Отметим, что исходными данными для верификации СПО, являются модели СПО и реализация СПО.
Определим также понятие верификации модели СПО.
«Верификация модели СПО — это подтверждение на основе предоставления объективных свидетельств того, что установленные требования к модели СПО были выполнены».
При построении моделей в них переносятся определенные аспекты реальной или абстрактной системы. Разумеется, для того, чтобы осуществлять проверки некоторых свойств модели, эти свойства должны быть связаны с отраженными в модели аспектами.
Можно выделить следующие типы проверок моделей СПО [83].
Синтаксической корректности;
Истинности логических условий;
a. Локальное;
b. Глобальное (весь период выполнения модели);
c. Интервальное (открытые и закрытые в том числе);
Отсутствие тупиков;
Отсутствие циклов самогенерации;
Причинно-следственные проверки;
Временные проверки;
Нагрузочные проверки.
Самыми простыми типами проверок, являются проверки синтаксической корректности, и локальной истинности логических условий. Такие проверки могут быть выполнены над моделью, описанной даже с помощью обычных языков программирования. Например, для программы, написанной на языке С, требование синтаксической корректности проверяется компилятором, а локальная истинность логических условий может быть проверена с помощью утверждений assert. Такая техника проверок модели программ может быть названа прототипированием. Выполняя тестовые прогоны программы с различными наборами входных данных, можно выяснить поведение модели в
35 интересующих нас условиях. Однако, как отмечалось выше, сложность реальных приложений такова, что полное тестовое покрытие на практике обеспечить невозможно.
Другие типы проверок над такими моделями также в ряде случаев можно выполнять, применяя дополнительные ухищрения. Однако полученные результаты, как и в предыдущем случае, носят частный характер, и не гарантируют выполнения данных условий во всем диапазоне возможных тестовых данных.
Для проверки логической правильности СПО желательно иметь возможность строить предположения о причинно-следственных отношениях внутри модели, а затем выполнять их проверку. Если бы средства проверки давали гарантированный ответ о справедливости сделанных предположений, или же давали ответ с определенной степенью вероятности, то использование таких проверок обеспечило бы существенные преимущества с кратко рассмотренной выше техникой тестовых прогонов.
Отметим, что проверка временных и нагрузочных характеристик СПО является сложной задачей. Для исследования данных свойств модели необходимо использование сложного математического аппарата. В некоторых областях получены интересные результаты. Например, в теории планирования вычислительных процессов существуют применимые на практике методы, которые позволяют составлять расписание обслуживания потоков задач вычислителем [63]. Однако существует значительные сложности при получении требуемых характеристик СПО, в частности, времени наихудшего выполнения WCET. Данная величина зависит от множества факторов, в том числе, от производительности вычислительной платформы, процессора, загрузки оперативной памяти и от состава мультипроцессной смеси. Ряд работ, в частности [68], показывает сложность данной проблемы.
1.3.4. Современные средства построения и верификации моделей ПО
В приведенном ранее обзоре указывалось, что наиболее пригодным для формального анализа видом представления моделей ПО являются модели на основе конечных автоматов (FSM, см. выше). При этом отмечалось, что описания в виде FSM обладают недостаточно большой выразительностью. Также было отмечено, что при использовании FSM необходимы дополнительные приемы для описания параллельно выполняющихся потоков управления.
Большей выразительностью, чем FSM, обладают модели Rendezvous и
SR. Такие мощные языки, как CSP [82], используют модель Rendezvous для
описания асинхронного параллельно выполняющегося программного
обеспечения. На основе CSP разработаны системы моделирования и
верификации FDR и FDR2 фирмы Formal Systems England [77]. Известно об
успешном применении данных систем для верификации моделей в ряде
V проектов [80].
Желательным было бы использовать такой подход к верификации моделей СПО, при котором возможность формальных проверок моделей сочеталась бы с выразительным синтаксисом. Иначе говоря, предпочтителен такой подход, при котором представление модели, к примеру, на языке уровня CSP, однозначно транслировалось (отображалось) в представление уровня FSM. Полученное представление на уровне FSM могло бы послужить исходными данными для формального анализа. При этом формальный анализ должен позволять выполнять проверки типов 1-5 из предыдущего раздела.
Отметим, что актуальность исследований в данном направлении подтверждается, например, работами [71] и [83]. В качестве основного способа исследований моделей асинхронных программных систем исследователи называют аппарат темпоральной логики.
Использование недетерминированных автоматов представляется возможным для описания моделей СПО ИУС. Многие события в ИУС на практике нельзя достоверно предсказать. Например, при использовании ненадежного канала передачи данных определить вероятность сбоя возможно далеко не всегда. Вероятность сбоя при передаче данных может зависеть от множества факторов, например, от температуры, влажности и т.п. Введение в модель аспектов, отражающих множество таких факторов, приводит к ее чрезвычайному усложнению, и, следовательно, невозможности анализа модели.
Рассмотрим другой пример, показывающий сложность и недетерминированность процессов в СПО ИУС. Пусть существует поток, выполняющийся под управлением операционной системы реального времени. Для постановки потока на выполнение в соответствии с выбранной дисциплиной планирования выполняется алгоритм планирования и принимается решение о том, какому потоку предоставляется процессор. Современные операционные системы реального времени используют различные алгоритмы планирования, в том числе, достаточно сложные [100]. Кроме того, в системе выполняются потоки с различными приоритетами. На практике часто невозможно выполнять статический анализ многоприоритетной смеси потоков выполнения, в которой потоки выполняются в соответствии с различными алгоритмами планирования. Ситуация усугубляется тем, что многие компоненты операционных систем реального времени поставляются в виде «черных ящиков», что усложняет исследование свойств системы. Наконец, взаимодействие с реальными объектами управления еще больше усложняет задачу анализа. Это показывает сложность практического использования детерминированных методов описания моделей СПО.
Для выполнения проверок 6,7 требуется дополнительные исследования. Во-первых, их проведение может требовать введения дополнительных параметров в модели (например, WCET, см. выше), и, следовательно,
38 усложнения средств описания моделей. Во-вторых, для их выполнения может потребоваться выполнение части или всех проверок 1-5.
В соответствии с изложенными выше соображениями, для построения моделей и верификации СПО представляется целесообразным использовать инструменты, в которых выразительные описания асинхронного взаимодействия программных компонент (с использованием языков уровня CSP) сочетались бы с наличием средств формальных проверок. При этом в качестве средства анализа логической состоятельности программ видится аппарат темпоральной логики.
Рассмотрим современные методы и инструменты построения и верификации моделей ПО.
FDR2. Один из лидеров в области систем формальных проверок, фирма Formal Systems (England), предлагает инструмент FDR2, использующий для описания моделей язык CSP с расширениями. Данный инструмент доступен для универсальной платформы (х86) для систем Linux, Solaris, FreeBSD, а также для вычислительной платформы IBM 3090 и далее. Не существует для платформы MS Windows. Коммерческий продукт. Демонстрационные версии инструмента недоступны.
Для отображения моделей, описанных на CSP с расширениями, предлагается инструмент РгоВЕ. Инструмент доступен для тех же платформ, что и FDR2, а также для MS Windows.
SMV. Система символической верификации SMV разработана в университете Carnegie Mellon, США. SMV (Symbolic Model Verifier) - это средство для проверки систем конечных состояний на выполнение спецификаций, записанных в виде утверждений темпоральной логики. Формат записи выражений темпоральной логики назван авторами как CTL (computational tree logic - логика вычислительного дерева) [98]. Язык описания
39 входных моделей - SMV и Verilog. Это был первый верификатор, который смог обработать системы с числом состояний более 10 в 300 степени [96].
«SMV - это система формальной верификации для проектов аппаратуры» [59]. Изначально система не предназначалась для верификации программного обеспечения с высокой степенью параллелизма.
SMV свободно доступен для некоммерческого использования. Исходный и объектный код инструмента не должен включаться в состав других инструментов (в т.ч. коммерческих) без разрешения разработчиков.
SPIN. Данный инструмент разработан фирмой Bell Labs и Lucent Techlology. Инструмент использует оригинальный язык PROMELA (сокр. от PROcess MEta LAnguage). Синтаксис данного языка удобен для использования, поскольку представляет собой объединение выразительных возможностей языка С и интуитивно понятных выражений CSP, используемых для описания взаимодействия модулей. Инструмент позволяет осуществлять исполнение и верификацию моделей, используя при этом для описания требований к поведению системы выражения темпоральной логики. Инструмент сделан переносимым на различные платформы, доступны его версии для использования под Linux, MS Windows, FreeBSD. Инструмент поставляется с открытыми исходными текстами на языке С. Инструмент свободно предлагается для использования в учебных и коммерческих целях.
Рассмотрим подробнее возможности системы SPIN.
«Верификационные модели фокусируется на доказательстве правильности взаимодействия процессов, и модели пытаются абстрагироваться настолько, насколько это возможно, от внутренних последовательных вычислений. Взаимодействие процессов может быть определено в SPIN с помощью примитивов рандеву, асинхронной посылки сообщений через буферизированные каналы, через доступ к разделяемым переменным или с помощью любых комбинаций вышеперечисленного. Направленность на
асинхронное управление в программных системах, отличного от синхронного управления в аппаратных системах, SPIN отличается сам от других подходов к проверки моделей» [85].
Telelogic TAU SDL SUITE. Система TAU SDL - это пакет от одного из лидеров производства коммерческих продуктов для обеспечения процесса разработки ПО. Использует язык SDL. В составе пакета существует интеграция с UML. Для тестирования моделей используется язык тестирования TTCN. Существуют пакеты генерации C++ кода из SDL и UML моделей. Коммерческий продукт. Доступна ознакомительная версия сроком 1 месяц.
SDL (Specification and Description Language) - это графический язык, который разработан для моделирования телекоммуникационных процессов. Наряду с графической формой существует равноправная текстовая форма. Исследования по созданию SDL велись с 1968 года. SDL стандартизован ISO-CCITT (ныне ITU-T) в 1993 году в виде стандарта SDL-92. Не так давно появился стандарт SDL-2000. На основе данного языка созданы такие инструменты, как Cinderella SDL и TAU G2 от Telelogic. «Несмотря на использование в промышленности, хорошо известен тот факт, что SDL - не подходящий язык для верификации приложений» [83]. В настоящее время ведутся исследования в области трансляции моделей из SDL в различные представления FSM. Например, в работе [61] изложены попытки трансляции SDL в язык COSPAN.
Lotos Toolbox. Инструмент Lotos Toolbox доступен для платформ Sun, HP Unix. Использует язык Lotos. Позволяет проводить синтаксические проверки и исполнение моделей, имеет графический интерфейс. Не позволяет выполнять поверки выражений темпоральной логики или проверки типа refinement. Позволяет генерировать реализацию прототипа на языке С. Коммерчески доступен.
*ягЯКАі
Lotos (Language of Temporal Ordering Specification)"^TjEni разработан ISO, TC97/SC21/WG1. Язык основывается на CCS. «Главная цель алгебры процессов - это формальная спецификация поведения процессов на высшем уровне абстракции. Алгебра определяет строгое множество правил трансформации и отношений эквивалентности, которые могут позволить проектировщику формально судить о поведении. Lotos был выпущен как международный стандарт ISO IS8807 в феврале 1989» [83].
EDT, Инструмент EDT (Estelle Development Toolset) доступен для платформ Sun под Solaris 2.5 и PC под Linux 2.0.35 и выше. Использует язык Estelle. Позволяет проводить исполнение моделей. Использует трансляцию моделей в язык С. Коммерческий продукт, доступна ознакомительная версия сроком на один месяц.
Estelle - это язык формального описания, разработанный в ISO, TC97/SC21/WG1. Язык Estelle основан на расширенной концепции конечных автоматов. Язык может быть представлен как множество расширений к стандартизованному Pascal (IS7185) уровня 0. Расширения позволяют моделировать систему как иерархическую структуру недетерминистических взаимодействующих автоматов, которые могут выполняться параллельно и могут взаимодействовать с помощью сообщений и разделения переменных. Он был выпущен ISO в виде международного стандарта IS9074 в июле 1989» [83].
По оценке Хольцмана [83], SDL, Lotos и Estelle не подходят для решения проблемы верификации проекта на уровне спецификации протоколов компонент. В частности, в Lotos и SDL существует возможность спецификации неограниченных систем, что делает множество проблем верификации формально неразрешимыми.
Ptolemy П. Поддержка работы с CSP заявлена в мощном пакете моделирования Ptolemy И, разрабатываемом и поддерживаемом UC Berkeley, США. Проект Ptolemy II является частью проекта Ptolemy, направленного на обучение моделированию, симуляции и проектирования параллельных встроенных систем реального времени. Существует версия Ptolemy II, свободно доступная для академического использования. Однако пакет в свободно распространяемой версии не позволяет осуществлять формальные проверки CSP моделей. В данном пакете CSP может использоваться лишь как средство описания моделей.
Пакет интересен тем, что позволяет осуществлять описание моделей системы в виде разнотипных представлений, и далее проводить анализ полученного совокупного описания [91].
Сравнительные характеристики инструментов верификации моделей приведены в таблице 1.1. Таблица составлена на основе [78],
Обозначения в графе средства работы с моделями:
Syntax - выполняет проверки синтаксиса;
Type checking - выполняет проверки типов;
Static - выполняет статические проверки;
Execution — возможность визуализации исполнения модели;
Proof- возможность доказательств корректности;
Refinement - возможность выполнения проверок типа Refinement;
Graphic — наличие графического интерфейса инструмента;
Test Case Generation - возможность генерации тестовых наборов;
Some - означает частичную поддержку данного средства.
Таблица 1.1 Таблица сравнения инструментов верификации моделей
Окончание таблицы 1.1
1.4. Постановка задачи
В результате анализа современных методов повышения качества и надежности СПО ИУС сделаны следующие выводы:
Признана перспективность методов построения и верификации моделей СПО ИУС, поскольку они позволяют уменьшить число ошибок в СПО на ранних этапах разработки и, таким образом, значительно снизить затраты на проектирование;
Специфика СПО ИУС состоит в высокой сложности, большой связности элементов, высоких требованиях по безопасности и надежности и невозможности полного тестирования в составе конечного изделия;
Проведение проверок требований типов 1-5 раздела 1,3.3. является достаточным для обеспечения приемлемого уровня проверки моделей при относительно невысоком уровне затрат;
Большинство автоматизированных методов построения и верификации моделей требуют значительных затрат при включении в процесс разработки СПО ИУС;
Большинство методов и инструментов автоматизированного построения и верификации моделей обладают высокой стоимостью и требуют значительных ресурсов на освоение.
В рамках указанных ниже ограничений для повышения качества и надежности СПО ИУС ставится задача создания метода построения и верификации моделей СПО ИУС.
Введем ряд ограничений на разрабатываемый метод: 1. Метод должен учитывать существующие способы разработки СПО с целью уменьшения стоимости внедрения и его использования в процессе разработки
Метод должен учитывать специфику СПО ИУС
Метод должен быть ориентирован на использование в небольших коллективах разработчиков
Метод должен основываться на формальных подходах и позволять получать гарантированный результат или результат с известной вероятностью.
Метод должен допускать создание автоматизированных средств для исследования и верификации моделей (там, где это возможно)
Метод должен быть поддержан примерами типовых моделей СПО ИУС для использования на практике.
Метод должен позволять выполнять верификацию требований типов 1-5 раздела 1.3.3, для выбранных моделей.
Перспективным видится использование автоматных моделей, наиболее полно отражающих поведенческий аспект СПО ИУС.
В соответствии с этим необходимо произвести выбор современных методов и инструментов построения и верификации моделей, в том или ином виде использующих модели автоматов конечных состояний. Данные методы и средства позволяют выполнять формальные проверки поведения моделей, в частности, с использованием аппарата темпоральной логики.
Таким образом, в рамках решения общей проблемы построения и верификации моделей СПО ИУС должны быть решены следующие подзадачи:
Конкретизировать область и типы объектов СПО в составе ПО ИУС;
На основе выполненного выше анализа особенностей СПО ИУС и введенных ограничений на условия применения выбрать базовый метод построения и верификации моделей;
Разработать методы и средства представления СПО ИУС для создания моделей, согласованных с выбранным методом моделирования;
Разработать технологию построения и верификации моделей СПО ИУС на основе выбранного метода моделирования;
Определить перечень необходимых инструментов, обеспечивающих реализацию предлагаемой технологии;
По возможности усовершенствовать базовый метод в части представления требований верификации и сокращения объема пространства состояний;
Разработать автоматизированный комплекс средств моделирования и верификации на основе предложенной технологии. Комплекс должен быть ориентирован на практическое применение малыми коллективами разработчиков ИУС, должен допускать создание библиотек элементов моделей и поддерживать повторное использование наработок;
Оценить корректность и результативность разработанных средств построения и верификации СПО ИУС.
Современные средства построения и верификации моделей ПО
В приведенном ранее обзоре указывалось, что наиболее пригодным для формального анализа видом представления моделей ПО являются модели на основе конечных автоматов (FSM, см. выше). При этом отмечалось, что описания в виде FSM обладают недостаточно большой выразительностью. Также было отмечено, что при использовании FSM необходимы дополнительные приемы для описания параллельно выполняющихся потоков управления.
Большей выразительностью, чем FSM, обладают модели Rendezvous и SR. Такие мощные языки, как CSP [82], используют модель Rendezvous для описания асинхронного параллельно выполняющегося программного обеспечения. На основе CSP разработаны системы моделирования и верификации FDR и FDR2 фирмы Formal Systems England [77]. Известно об успешном применении данных систем для верификации моделей в ряде V проектов [80]. Желательным было бы использовать такой подход к верификации моделей СПО, при котором возможность формальных проверок моделей сочеталась бы с выразительным синтаксисом. Иначе говоря, предпочтителен такой подход, при котором представление модели, к примеру, на языке уровня CSP, однозначно транслировалось (отображалось) в представление уровня FSM. Полученное представление на уровне FSM могло бы послужить исходными данными для формального анализа. При этом формальный анализ должен позволять выполнять проверки типов 1-5 из предыдущего раздела.
Отметим, что актуальность исследований в данном направлении подтверждается, например, работами [71] и [83]. В качестве основного способа исследований моделей асинхронных программных систем исследователи называют аппарат темпоральной логики.
Использование недетерминированных автоматов представляется возможным для описания моделей СПО ИУС. Многие события в ИУС на практике нельзя достоверно предсказать. Например, при использовании ненадежного канала передачи данных определить вероятность сбоя возможно далеко не всегда. Вероятность сбоя при передаче данных может зависеть от множества факторов, например, от температуры, влажности и т.п. Введение в модель аспектов, отражающих множество таких факторов, приводит к ее чрезвычайному усложнению, и, следовательно, невозможности анализа модели.
Рассмотрим другой пример, показывающий сложность и недетерминированность процессов в СПО ИУС. Пусть существует поток, выполняющийся под управлением операционной системы реального времени. Для постановки потока на выполнение в соответствии с выбранной дисциплиной планирования выполняется алгоритм планирования и принимается решение о том, какому потоку предоставляется процессор. Современные операционные системы реального времени используют различные алгоритмы планирования, в том числе, достаточно сложные [100]. Кроме того, в системе выполняются потоки с различными приоритетами. На практике часто невозможно выполнять статический анализ многоприоритетной смеси потоков выполнения, в которой потоки выполняются в соответствии с различными алгоритмами планирования. Ситуация усугубляется тем, что многие компоненты операционных систем реального времени поставляются в виде «черных ящиков», что усложняет исследование свойств системы. Наконец, взаимодействие с реальными объектами управления еще больше усложняет задачу анализа. Это показывает сложность практического использования детерминированных методов описания моделей СПО.
Для выполнения проверок 6,7 требуется дополнительные исследования. Во-первых, их проведение может требовать введения дополнительных параметров в модели (например, WCET, см. выше), и, следовательно, усложнения средств описания моделей. Во-вторых, для их выполнения может потребоваться выполнение части или всех проверок 1-5.
В соответствии с изложенными выше соображениями, для построения моделей и верификации СПО представляется целесообразным использовать инструменты, в которых выразительные описания асинхронного взаимодействия программных компонент (с использованием языков уровня CSP) сочетались бы с наличием средств формальных проверок. При этом в качестве средства анализа логической состоятельности программ видится аппарат темпоральной логики. Рассмотрим современные методы и инструменты построения и верификации моделей ПО. FDR2. Один из лидеров в области систем формальных проверок, фирма Formal Systems (England), предлагает инструмент FDR2, использующий для описания моделей язык CSP с расширениями. Данный инструмент доступен для универсальной платформы (х86) для систем Linux, Solaris, FreeBSD, а также для вычислительной платформы IBM 3090 и далее. Не существует для платформы MS Windows. Коммерческий продукт. Демонстрационные версии инструмента недоступны. Для отображения моделей, описанных на CSP с расширениями, предлагается инструмент РгоВЕ. Инструмент доступен для тех же платформ, что и FDR2, а также для MS Windows. SMV. Система символической верификации SMV разработана в университете Carnegie Mellon, США. SMV (Symbolic Model Verifier) - это средство для проверки систем конечных состояний на выполнение спецификаций, записанных в виде утверждений темпоральной логики. Формат записи выражений темпоральной логики назван авторами как CTL (computational tree logic - логика вычислительного дерева) [98]. Язык описания входных моделей - SMV и Verilog. Это был первый верификатор, который смог обработать системы с числом состояний более 10 в 300 степени [96]. «SMV - это система формальной верификации для проектов аппаратуры» [59]. Изначально система не предназначалась для верификации программного обеспечения с высокой степенью параллелизма. SMV свободно доступен для некоммерческого использования. Исходный и объектный код инструмента не должен включаться в состав других инструментов (в т.ч. коммерческих) без разрешения разработчиков.
Анализ базового метода построения и верификации моделей ПО
Проведем анализ базового метода, изложенного в [83], [85], с точки зрения решаемой задачи верификации моделей СПО ИУС.
Базовый метод построения моделей ПО и их верификации, разработанный доктором G. Holzmann, изложен в [83]. Базовый метод предназначен для исследования коммуникационных протоколов и ПО в целом, предполагая использование инструмента SPIN.
Разработка базового метода началась в 1979 году. «Работа над технологиями проверки моделей, первопроходцами которой были Clarke и Emerson [70] и Sifakis и Queille [101], заложила основание для нового поколения средств с большими верификационными способностями. Vardi и Wolper расширили эту работу моделью теоретических автоматов [105], которая стала формальной основой для проверки моделей в системе SPIN. Рабочая модель кратко описана ниже.
Описание параллельной системы в PROMELA состоит из одного или более определяемых пользователем шаблонов процессов, или определений proctype, и по меньшей мере одного экземпляра процесса. Шаблон процесса определяет поведение различных типов процессов. Любой запущенных экземпляр процесса может создавать другие асинхронные процессы, используя шаблоны процессов.
SPIN транслирует каждый шаблон процесса в конечный автомат (FSM). Глобальное поведение параллельной системы получается вычислением асинхронно чередующегося продукта автомата, один автомат для каждого поведения асинхронного процесса. Результирующее глобальное поведение системы само также представляется автоматом. На этот чередующийся продукт часто ссылаются как на пространство состояний системы, и, поскольку он легко может быть представлен как граф, также обычно называется графом глобальной достижимости (global reachability graph).
Для выполнения верификации, SPIN берет требования корректности, которые указаны в формуле темпоральной логики, конвертирует эту формулу в автомат Буши, и вычисляет синхронный продукт этого требования и автомата, представляющего глобальное пространство состояния. Результат также является автоматом Буши. Если язык, присоединенный к данному автомату, пуст, то это значит, что оригинальное требование не удовлетворяется данной системой. Если язык не пуст, он содержит в точности то поведение, которое удовлетворяет исходной формуле темпоральной логики. В SPIN мы используем требования корректности для формализации ошибочного поведения системы, то есть нежелательного поведения. Верификационный процесс доказывает, что такое поведение невозможно или он предоставляет конкретные примеры соответствующего поведения.
В худшем случае, граф глобальной достижимости имеет размер картезианского продукта (Cartesian product) всех компонент системы. Язык спецификаций PROMELA определен таким образом, что каждый компонент всегда имеет точно определенные границы. Это применяется к процессам (которые имеют только конечное множество управляющих состояний), но также и ко всем локальным и глобальным переменным (которые могут иметь ограниченное множество различных значений), и всем каналом сообщений (каждый ограничен определяемой пользователем емкостью). Хотя, на практике, размер глобальной достижимости никогда не превышает размера худшего случая, достижимая часть картезианского продукта может быть также слишком большой для истощающего конструирования. Множество техник управления сложностью было разработано для борьбы с этой проблемой» [85].
Базовый метод состоит из следующих этапов: 1. Построение модели протокола; 2. Построение модели взаимодействующих процессов, соответствующей модели п.1, в том числе: а. Обобщение модели (generalization) — устранение лишних аспектов модели [83], глава 8; 3. Проверка синтаксиса модели п.2 с помощью SPIN; 4. Формулировка требований к модели в терминах линейной темпоральной логики; 5. Возможно, настройка модели или требования для верификации очередного требования (технология slice); 6. Проверка (верификация) выполнения требования к модели на основе требований п.4 с помощью SPIN; 7. Возможно, исправление модели или требования по результатам п.6; 8. Повторение пунктов 5-8 для каждого из требований п.4. Следует отметить, что базовый метод обладает большой универсальностью. Это позволяет его использовать для верификации ПО различных типов и на различных инструментальных системах. Сам по себе базовый метод является интересным и мощным средством для исследования свойств программного обеспечения, изучения свойств протоколов и распределенных систем. Однако, при использовании базового метода в условиях, соответствующих решаемой задаче, обнаруживается ряд особенностей и недостатков, рассмотренных ниже: 1. Отсутствие формализованного перечня входных и выходных данных. В базовом методе в явном виде не указано, какими входные данные должны быть в наличии у разработчиков до применения метода. В описании метода подразумевается, что этих данных должно быть достаточно для построения моделей протокола и модели взаимодействующих процессов, а также для предъявления требований верификации. Кроме того, базовый метод не содержит формализованного перечня выходных данных. Подразумевается, что в результате применения метода формируется вывод о том, выполняются или нет требования верификации данной моделью. При развитии базового метода для построения и верификации моделей СПО полезно в явном виде определить перечни входных и выходных данных. Кроме того, желательно предложить форму фиксации полученных результатов. Эта форма может быть использована в качестве основы для накопления и повторного использования элементов разработок, а также использоваться для удостоверения качества произведенного программного продукта. Соблюдение данных процедур предписывается стандартом ISO 9000:2000 (см., например, [21], часть 1, глава 3). Предложенное развитие метода может быть использовано в качестве одного из стандартов предприятия.
Исследование расширенного метода и метода на основе SMV
Как было показано в главе 2, предложенный метод является расширением базового метода Holzmann G. [83]. Особенностью расширенного метода является его адаптация к решению задачи построения и верификации СПО в условиях поставленных ограничений.
Было проведено исследование эффективности применения расширенного метода для построения и верификации моделей СПО ИУС относительно базового метода Holzmann, в ходе которого было подготовлено и проведено более 50 экспериментов.
Суть экспериментов состояла в измерении ряда характеристик процесса исследования СПО с помощью каждого из методов. После этого для каждого эксперимента строилось процентное отношение по каждой из характеристик. Затем полученные характеристики усреднялись по всем экспериментам.
Были измерены следующие характеристики: 1. Трудоемкость верификации СПО - трудоемкость использования метода [человеко-часы]; 2. Трудоемкость построения модели общая - затраты, требуемые для построения модели [человеко-часы]; 3. Трудоемкость построения модели драйвера - затраты, требуемые для построения модели класса драйверов [человеко-часы]; 4. Выразительность записей требований - длина требования верификации [число элементов, из которых состоит требование верификации в синтаксисе линейной темпоральной логики]; 5. Время предъявления требований - время составления требований верификации [часы]; 6. Вероятность ошибок - вероятность получения ошибочного требования при его предъявлении [число ошибочных требований/общее число требований]; 7. Время навигации по истории моделирования - время, необходимое для выполнения навигации по истории моделирования к результатам требуемого этапа моделирования [секунды]; 8. Время этапа моделирования и верификации [часы]; 9. Время обработки моделей верификатором [секунды]. Каждый из экспериментов проводился одним исследователем, что уменьшает влияние экспериментатора на результаты эксперимента. Каждый из экспериментов проводился полностью на одном из персональных компьютеров: ПК1 или ПК2, чтобы исключить влияние различий систем на характеристики экспериментов. В ходе экспериментов исследовались: 1. модель драйвера OS Windows NT; 2. модель драйвера OS QNX 4.25; 3. модель драйвера OS Lynx 4.0.0; 4. модель драйвера OS DOS 6.22; 5. модель механизма арбитража активности резервированных модулей управления устройствами; 6. модель доступа потоков к разделяемому ресурсу с синхронизацией через семафор; 7. модель доступа потоков к разделяемому ресурсу с синхронизацией через мютех; 8. модель многопоточной системы обработки запросов с выделением сервисного потока из пула; 9. модель многопоточной системы обработки запросов с динамическим созданием сервисного потока; 10. модель системы выдачи ответственных команд управления устройствами; 11.и т.д. В таблице и на рисунке приведен пример результатов экспериментов измерения трудоемкости построения указанных выше моделей. Трудоемкость построения моделей СПО Из приведенных данных видно, что трудоемкость этапа построения первой версии модели СПО (в расширенном методе используется название начальная модель) по базовому методу на 25 процентов больше, чем при использовании расширенного метода. Уменьшение трудоемкости происходит за счет применения готовых элементов моделей из библиотеки СПО. Для моделей СПО класса драйверов получено сокращение трудоемкости до 40 процентов (модели 1,2,3,4), поскольку библиотека элементов моделей содержит все основные элементы, входящие в состав драйверов. В ходе исследований были получены следующие результаты: 1. Время навигации по истории моделирования в расширенном методе сократилось в среднем на 15 процентов по сравнению с базовым методом. Это оказалось возможным за счет использования дополнительных форматов данных, в частности таблицы требований, выступающей в качестве основы при навигации по истории моделирования и за счет использования системы контроля версий (структуры каталогов или системы контроля версий Source Safe). Однако уменьшение времени навигации привело к увеличению требований к вычислительным ресурсам для хранения дополнительных данных и потребовало использования системы контроля версий в одном из двух вариантов исполнения. 2. В расширенном методе созданы предпосылки к автоматизации процесса построения и верификации моделей за счет дополнительных введенных форматов и более детальной алгоритмизации этапов алгоритма (вместо 8 в базовом методе в расширенном выделено 11 шагов с 20 подэтапами). 3. Применение дополнительных операций W,R,P, которые достаточно часто используются при составлении требований верификации моделей СПО (примерно 30% от всех требований), позволили увеличить выразительность записи до 25% по сравнению с базовым методом. Однако это потребовало введения дополнительных операций в базис расширенного метода и увеличило время освоения метода. 4. Использование в расширенном методе образцов ограничения области действия требований позволяет сократить время предъявления требований данного типа на 45%. При этом требования с ограниченной областью действия составляют 30-40 процентов от всех требований верификации, характерных для области СПО. 5. Введение образцов позволило значительно сократить (до 30%) число ошибок, при составлении требований с ограниченной областью видимости. Самостоятельное составление требований достаточно сложно и чревато ошибками. Однако, использование образцов на практике требует дополнительных затрат на обучение их использованию. 6. Использование MSDev и добавление синтаксической подсветки выражений PROMELA в расширенном методе позволило уменьшить время этапа верификации и итеративных изменений модели на 7,5%. Однако, при использовании пакета необходимы затраты на обучение работы с интегрированной средой MSDev, и затраты на приобретение Microsoft Visual Studio 6.0, если его нет в числе программ, доступных для разработчиков. 7. В расширенном методе предложено отказаться от этапа составления протокола обмена, который присутствует в базовом методе. Это позволило сократить на 10% время этапа построения и верификации моделей в расширенном методе. Однако в расширенном методе отсутствует спецификация протокола, и для исследования протоколов взаимодействия элементов СПО приходится исследовать модель системы.
Исследование критически важного механизма арбитража активности резервированных модулей
Проведенное исследование подтвердило возможность использования расширенного метода применительно к КВМ СПО ИУС. Достоинством исследования является то, что оно было применено к практической задаче, стоящей перед группой разработчиков ИУС.
Важным полученным результатом является создание предложенного в расширенном методе приема деления модели на уровни. Выработана рекомендация, в соответствии с которой, после верификации каждого из уровней моделей выполняется построение объединенной модели и ее верификация в режиме supertrace.
Другим важным выводом исследования является то, что даже при обнаружении невыполнения требований верификации в частных случаях при реализации системы можно использовать дополнительные приемы защиты, которые обеспечат в конечной реализации выполнение необходимых требований.
Данное исследование, как и исследование архитектуры драйвера Windows NT, проводилось с использованием разработанного пакета интеграции SPIN и MSDev. Это обеспечило ускорение процесса редактирования модели, что особенно актуально с учетом большого числа выполненных изменений.
Исследование показало, что можно добиться относительно высокой степени детализации при построении модели. При этом, однако, отмечен быстрый рост пространства состояний, что затрудняет исследование.
В ходе исследования была обнаружено практическое удобство копирования элементов глобального состояния модели в локальную область единицы моделирования (процесса). Такой прием позволяет улучшить читаемость модели за счет использования коротких имен переменных локальной области. Кроме того, упрощается синхронизация различных процессов, каждый из которых работает со своей копией глобального состояния. Недостатком такого приема является потребление дополнительных ресурсов.
Также был сделан вывод о том, что использование техники изменяемого вектора состояния моделей (rubber-state vector), который используется в инструменте SPIN, позволяет исследовать переходные процессы в моделях (на этапе старта или останова системы), которые оказываются недоступными для систем с фиксированным числом состояний для каждого элемента моделей.
Полученная результат-модель КВМ арбитража активности представлена в приложении 2, 1. Выполненные исследования показали возможность практического использования предложенной в работе технологии построения и верификации моделей СПО. При этом была выполнена проверка применимости как для исследования архитектуры СПО ИУС, так и для КВМ СПО ИУС. Проиллюстрировано решение практических задач из области разработки СПО ИУС. 2. Продемонстрировано удобство использования автоматизированного комплекса построения и верификации моделей СПО ИУС на основе расширенного метода. Отмечена целесообразность использования понятия начальной модели и результат-модели при использовании метода в реальных условиях разработки СПО. 3. Выработан ряд практических рекомендаций по применению предложенного метода, связанных с построением моделей. Необходимость создавать сложные ИУС, в том числе, осуществлять надежную и качественную разработку СПО ИУС, уменьшая количество ошибок, заставляет разработчиков активно искать пути решения данной проблемы. В настоящее время в данном направлении ведется множество исследований. Представленные в работе методы и средства автоматизации процесса создания и верификации моделей СПО ИУС развивают положительно зарекомендовавшую себя методику G. Holzmann. Основные теоретические результаты настоящей работы состоят в следующем: 1. Разработан расширенный метод построения и верификации высокоуровневых моделей СПО ИУС, базирующийся на методе G. Holzmann. Метод использует расширенный состав операторов представления требований верификации и механизмы ограничения областей видимости. 2. Определен ряд понятий: операционная среда, критически важные механизмы СПО, архитектура СПО в контексте процесса верификации, начальная модель, результат-модель, а также предложена классификация элементов СПО ИУС. 3. Разработана технология автоматизированной верификации моделей СПО ИУС на основе расширенного метода, включающая работу с таблицами требований и единиц моделирования, алгоритмы построения модели, метод получения результат-модели. 4. Произведена классификация элементов моделей СПО ИУС по способу активации исполнения, что позволило структурировать сведения о поведении элементов модели. 5. Показана возможность и целесообразность использования результатов моделирования в форматах расширенного метода для последующего этапа реализации СПО ИУС. К практическим результатам относится следующее: 1. Разработан автоматизированный инструментальный комплекс построения и верификации высокоуровневых моделей СПО ИУС. 2. Разработана оригинальная библиотека типовых элементов моделей СПО ИУС в специальном формате, позволяющая ускорить процесс построения моделей. 3. Предложен способ накопления и обработки протоколов верификации, учитывающий итерационный характер процесса. Данный способ реализован с помощью оригинальной структуры каталогов, а также хорошо согласован с современными системами контроля версий ПО. 4. В рамках автоматизированного комплекса реализован интерфейс верификатора со средой MSDev, включающий возможность использования синтаксической подсветки операторов языка PROMELA. Это позволило повысить комфортность и сократить количество ошибок при разработке и исследовании модели. Эффективность предложенного в работе расширенного метода построения и верификации моделей подтверждена проведенными экспериментами и успешным использованием в реальных проектах по разработке ПО ИУС.
