Главная | Обратная связь | Поможем написать вашу работу!

Спецификация поведения систем

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

Альтернативным подходом к созданию формальных спецификаций, который широко используется в программных проектах, является спецификация, основанная на моделях системы. Такие спецификации используют модели состояний системы. Системные операции определяются посредством изменений состояний системной модели. Таким образом определяется поведение системы.

Для разработки спецификаций, основанных на системных моделях, используются системы нотаций методов VDM [192, 193], В [348] и Z [158, 325]. Здесь я использую нотацию метода Z. В этом методе система описывается на основе теории множеств, которая дополняется специальными логическими структурами, разработанными для специфицирования программных систем. Полное описание метода Z очень объемно. Поэтому я представлю несколько небольших примеров для иллюстрации метода и приведу необходимые обозначения. Полное описание метода Z дается в [98, 347, 84].

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

Рис. 9.8. Структура Z-схемы

Сигнатура схемы определяет сущности, которые составляют состояние системы, схемные предикаты – это набор условий, которые должны быть всегда истинны для этих сущностей. Если схема определяет операции, предикаты могут представлять пред- и постусловия для этих операций.

Для иллюстрации применения метода Z в разработке спецификации критической системы рассмотрим упрощенный пример системы инсулинового насоса, используемой диабетиками. У диабетиков нарушен естественный метаболизм сахара, им требуются инъекции инсулина – гормона, необходимого для метаболизма глюкозы. Данная система контролирует уровень сахара в крови больного и, если требуется, производит автоматическую инъекцию инсулина. Этот пример также использован в части IV, где рассматривается разработка критических систем.

Уровень сахара в крови больного проверяется через равные промежутки времени, и, если он увеличивается, производится инъекция инсулина, которая понижает уровень сахара. На рис. 9.9 показана структура инсулинового насоса.

1. Набор игл. Подсоединены к насосу, используются для инъекции инсулина в тело диабетика.

2. Датчик. Измеряет уровень сахара в крови больного. В формальной спецификации операция получения данных от датчика названа reading?.

3. Насос. Передает инсулин из резервуара к набору игл. В формальной спецификации величина дозы инсулина названа dose.

4. Управляющее устройство. Управляет объектами системы. Имеет переключатель "Включено – Выключено", кнопку отмены и кнопку установки дозы инсулина. Для упрощения формальной спецификации эти элементы управления не описаны.

5. Устройство аварийной сигнализации. Подает звуковой сигнал при возникновении проблем. В спецификации сигнал на входе устройства аварийной сигнализации обозначен как alarm!.

6. Индикаторы. Имеется два индикатора: один показывает последний анализ уровня сахара в крови, другой – информацию, выдаваемую системой пользователю. Эти индикаторы в формальной спецификации обозначаются display1! и display2!.

7. Часы. Обеспечивают управляющее устройство значением текущего времени.

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

Рис. 9.9. Блок-схема инсулинового насоса

Основная схема Insulin-pump (инсулиновый насос), которая моделирует состояния инсулинового насоса, показана на рис. 9.10. Схема разбита на две части. В верхней части объявляются имена и типы, в нижней приведены условия, которые должны всегда выполняться.

Рис. 9.10. Z-схемл инсулинового насоса

Состояние системы моделируется посредством ряда переменных. В соответствии с соглашениями, принятыми в методе Z, имена, заканчивающиеся знаком?, используются для представления входных данных, а имена, заканчивающиеся знаком!, представляют выходные данные. В схеме инсулинового насоса объявлены следующие имена.

1. reading?. Это неотрицательное целое число, которое представляет данные от датчика, определяющего количество сахара в крови. Это входная величина.

2. dose, cumulative_dose. Это также натуральные числа, представляющие соответственно дозу инсулина и суммарную дозу инсулина, введенную за определенный период времени.

3. r0, r1, r2. Представляют последние три значения, полученные от датчика, и используются для вычисления изменения сахара в крови.

4. capacity. Натуральное число, представляющее объем инсулина в хранилище (резервуаре).

5. alarm!. Эта выходная величина сообщает об аварийных ситуациях в системе.

6. pump!. Это натуральное число, представляющее управляющие сигналы, посылаемые к физическому насосу.

7. display1!, display2!. Эти выходные величины строкового типа представляют два текстовых индикатора. Один индикатор используется для отображения текстовых сообщений, другой – для показа введенной дозы инсулина.

Схемные предикаты определяют ряд условий, которые всегда должны быть истинными.

1. Доза должна быть меньше или равна количеству инсулина в резервуаре.

2. Однократная доза не должна превышать 5 единиц инсулина, а общая доза, введенная за определенный промежуток времени, – 50 единиц инсулина. Это условия безопасности, которые рассматриваются в главе 17.

3. display1!. Показывает сообщения о состоянии инсулинового резервуара. Если резервуар содержит 40 или больше единиц инсулина, сообщений нет. Когда в резервуаре инсулина от 10 до 40 единиц, на дисплее отображается предупреждение, если же в резервуара меньше 10 единиц, звучит звуковой сигнал и отображается соответствующее предупреждение.

Работа инсулинового насоса заключается в определении каждые 10 минут количества сахара в крови пациента и введении инсулина, если уровень сахара увеличивается (это очень упрощенное описание). Вводимое количество инсулина вычисляется согласно схеме DOSAGE (Дозировка), которая приведена на рис. 9.11. Из этой схемы видно, что на вводимую дозу влияет множество различных факторов.

Рис. 9.11. Z-схема вычисления дозы

На рис. 9.11 показано часто используемое средство метода Z, а именно дельта-схема. Если имя схемы включено в раздел описаний, то это равносильно включению всех имен данной схемы, а ее условия включаются в предикатную часть. В данном случае в схему DOSAGE включаются имена и условия схемы Insulin_Pump. Если имени схемы предшествует символ ∆, то вводится новый набор величин, имена которых совпадают с именами данной схемы, но к ним добавляется символ ' (апостроф). Так обозначаются значения переменных состояний, измененные после выполнения операции. Например, если операция изменяет значение переменной val, то после операции эта переменная будет обозначаться val'. Дельта-схема DOSAGE вводит имена capacity'. cumulative_dose' и т.д.

Схемы, моделирующие выходные данные инсулинового насоса, показаны на рис. 9.12. Это модели индикаторов и устройства аварийной сигнализации. Здесь также используется дельта-схема. Из схемы DISPLAY видно, что индикатор display2! показывает вычисленную дозу (Nat_to_string – функция преобразования), индикатор display1! отображает или предупреждающее сообщение, или ОК. В схеме ALARM показаны условия, когда активизируется аварийная сигнализация. Она включается, если уровень сахара в крови очень низкий (меньше 3) или слишком высокий (больше 30).

Рис. 9.12. Схемы выходных данных

Предикаты во всех Z-схемах должны быть согласованы, т.е. не должно быть условий в одной схеме, которые противоречат предикатам в другой схеме. Если в спецификации замечены противоречия, можно применить различные математические методы анализа Z-спецификации. Здесь я не буду их описывать. Рассматривая представленные четыре Z-схемы, вы могли заметить противоречия, которые я сознательно ввел, но которые могли бы появиться в реальной спецификации. В общей схеме инсулинового насоса lnsulin_Pump установлено, что индикатор display1! должен показывать состояние резервуара инсулина. Однако в схеме DISPLAY этот индикатор должен показывать уровень сахара в крови. Здесь противоречие, которое следует разрешить при обсуждении системы с медицинскими экспертами и потенциальными пользователями.

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

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

КЛЮЧЕВЫЕ ПОНЯТИЯ

• Методы формальной системной спецификации дополняют методы неформальной спецификации. Они могут использоваться для детализации спецификации неформальных системных требований. Формальные спецификации являются мостом между системными требованиями и системной архитектурой.

• Формальные спецификации точны и однозначны. Они устраняют “темные” области в спецификации и проблемы неоднозначного толкования требований. Вместе с тем формальные спецификации трудны для понимания неспециалистами.

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

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

• Алгебраические методы формальных спецификаций особенно подходят для разработки интерфейсов, когда интерфейс определен как набор классов объектов или абстрактных типов данных. Эти методы скрывают состояние системы и определяют ее в терминах отношений между интерфейсными операциями.

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

Упражнения

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

9.2. Перед вами поставлена задача "продажи" методов формальной спецификации организации, разрабатывающей программное обеспечение. Как вы будете объяснять преимущества формальной спецификации скептически настроенным разработчикам ПО?

9.3. Объясните, почему необходимо определять интерфейсы подсистем как можно точнее и почему алгебраическая спецификация наиболее подходит для специфицирования интерфейсов подсистем.

9.4. Абстрактный тип данных, представляющий стек, имеет следующие операции:

New (Создать) – создает пустой стек;

Push (Добавить) – добавляет элемент в вершину стека;

Тор (Вершина) – возвращает элемент на вершине стека;

Retract (Удалить) – удаляет элемент из вершины стека и возвращает модифицированный стек;

Empty (Пустой) – возвращает значение истины, если стек пустой.

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

9.5. В примере управления сектором воздушного пространства условием безопасности является то, что два самолета не могут находиться внутри 300-метровой зоны по высоте в одном секторе. Измените спецификацию, показанную на рис. 9.7, позволяющую самолетам занимать одинаковую высоту, если расстояние по горизонтали между ними не менее 8 км. Можно игнорировать самолеты в соседних секторах.

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

9.7. Измените схему инсулинового насоса, показанную на рис. 9.10, и схему DOSAGE, показанную на рис. 9.11, таким образом, чтобы пользователь системы мог отменить вычисленную дозу и сам определить дозу, необходимую для инъекции. Условия безопасности, указанные в схемах, должны сохраниться. Тот факт, что система работает в режиме отмены, должен отобразиться на индикаторе.

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

⇐ Предыдущая 61 62 63 64 656667 68 69 70 Следующая ⇒