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

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

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

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

Формальные спецификации могут быть трудными для чтения и громоздкими, особенно если используются большие математические формулы.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Основная схема Insulin-pump (инсулиновый насос), которая моделирует состояния инсулинового насоса, показана на рис. 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 единиц инсулина. Это условия безопасности.

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

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

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

Выводы

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

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

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

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

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

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