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

Прості алгебраїчні методи підходять для опису інтерфейсів, коли операції, асоційовані з об'єктом, не залежать від стану об'єкта. Тоді результати будь-якої операції не залежать від результатів попередніх операцій. Якщо ця умова не виконується, алгебраїчні методи можуть стати громіздкими. Алгебраїчні описи поведінки систем часто штучні і важкі для розуміння.

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

Для розробки специфікацій, заснованих на системних моделях, використовуються системи нотацій методів VDM, У и Z. Тут використовується нотація методу Z. У цьому методі система описується на основі теорії множин, яка доповнюється спеціальними логічними структурами, розробленими для специфікування програмних систем. Повний опис методу Z дуже об'ємний.

Формальні специфікації можуть бути важкими для читання і громіздкими, особливо якщо використовуються великі математичні формули. Це сповільнює розробку ПЗ. Розробники методу Z звернули увагу на цю проблему. У цьому методі специфікації представляються як неформальний текст, доповнений формальними описами. Формальна частина специфікації складається з невеликих простих описів (називаних схемами), які візуально відділяються від іншого тексту специфікації (рис. 6.8). Схеми використовуються для введення змінних станів і визначення обмежень і операцій над станами. У методі також передбачені операції, виконувані над схемами, зокрема для побудови, перейменування і приховання схем.

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

Сигнатура схеми визначає сутності, які складають стан системи, схемні предикати ‒ це набір умов, які повинні бути завжди істинні для цих сутностей. Якщо схема визначає операції, предикати можуть представляти перед-і постумови для цих операцій.

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

Рівень цукру в крові хворого перевіряється через рівні проміжки часу, і, якщо він збільшується, проводиться ін'єкція інсуліну, яка знижує рівень цукру. На рис. 6.9 показана структура інсулінового насоса.

1. Набір голок.Приєднані до насоса, використовуються для ін'єкції інсуліну в тіло діабетика.

2. Датчик.Вимірює рівень цукру в крові хворого. У формальній специфікації операція одержання даних від датчика названаreading?.

3. Насос.Передає інсулін з резервуара до набору голок. У формальній специфікації величина дози інсуліну названа dose.

4. Керуючий пристрій.Управляє об'єктами системи. Має перемикач “Включене ‒ Виключене”, кнопку скасування і кнопку установки дози інсуліну. Для спрощення формальної специфікації ці елементи керування не описані.

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

6. Індікапюри.Є два індикатори: один показує останній аналіз рівня цукру в крові, іншої ‒ інформацію, що видається системою користувачеві. Ці індикатори у формальній специфікації позначаютьсяdisplay 1! іdispiay2!.

7. Годинник.Забезпечують керуючий пристрій значенням поточного часу.

Навіть для невеликої системи, подібній системи керування ін'єкціями інсуліну, формальна специфікація досить велика. Хоча основні системні операції прості, існує багато аварійних ситуацій, які необхідно враховувати. Тут наведені тільки деякі з основних Z-схем специфікації і пояснене, що вони означають.

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

Основна схема Insulin-pump (інсуліновий насос), яка моделює стани інсулінового насоса, показана на рис. 6.10. Схема розбита на дві частини. У верхній частині оголошуються імена і типи, у нижній наведені умови, які повинні завжди виконуватися.

Рис. 6.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. displayl!. Показує повідомлення про стан інсулінового резервуара. Якщо резервуар містить 40 або більше одиниць інсуліну, повідомлень немає. Коли в резервуарі інсуліну від 10 до 40 одиниць, на дисплеї відображається попередження, якщо ж у резервуара менше 10 одиниць, звучить звуковий сигнал і відображається відповідне попередження.

4. Робота інсулінового насоса полягає у визначенні кожні 10 хвилин кількості цукру в крові пацієнта і введенні інсуліну, якщо рівень цукру збільшується (цей дуже спрощений опис), кількість інсуліну, що вводиться, обчислюється згідно зі схемою DOSAGE (Дозування), яка наведена на рис. 6.11. Із цієї схеми видно, що на дозу, що вводиться, впливає безліч різних факторів.

Рис. 6.11. Z-схеми обчислення дози

На рис. 6.11 показаний часто використовуваний засіб методу Z, а саме дельта-схема. Якщо ім'я схеми включене в розділ описів, то це рівносильне включенню всіх імен даної схеми, а її умови включаються в предикатну частину. У цьому випадку в схему DOSAGE включаються імена і умови схеми lnsulin_Pump. Якщо імені схеми передує символ Д, то вводиться новий набір величин, імена яких збігаються з іменами даної схеми, але до них додається символ'(апостроф). Так позначаються значення змінних станів, змінені після виконання операції. Наприклад, якщо операція змінює значення змінноїval, то після операції ця змінна буде позначатисяval'. Дельта-схема DOSAGE вводить іменаcapacity', cumulative_dose' і т.д.

Схеми, що моделюють вихідні дані інсулінового насоса, показані на рис. 6.12. Це моделі індикаторів і пристрою аварійної сигналізації. Тут також використовується дельта-схема. Зі схеми DISPLAY видно, що індикатор display2! показує обчислену дозу(Nat_to string ‒ функція перетворення), індикаторdisplayl! відображає або попереджуюче повідомлення, або ОК. У схемі ALARM показані умови, коли активізується аварійна сигналізація. Вона включається, якщо рівень цукру в крові дуже низький

Рис. 6.12. Схеми вихідних даних

Предикати у всіх Z-схемах повинні бути погоджені, тобто не повинно бути умов в одній схемі, які суперечать предикатам в іншій схемі. Якщо в специфікації замічені протиріччя, можна застосувати різні математичні методи аналізу Z-специфікації. У загальній схемі інсулінового насоса lnsulin_Pump установлено, що індикаторdisplayl! повинен показувати стан резервуара інсуліну. Однак у схеміDISPLAY цей індикатор повинен показувати рівень цукру в крові. Тут протиріччя, яке слід дозволити під час обговорення системи з медичними експертами і потенційними користувачами.

Потрібно враховувати, що датчик контролює рівень цукру в крові кожні 10 хвилин. Хоча це, зазвичай, можливо, але досить громіздко; неформальний опис дій більш короткий і зрозумілий, чим формальна специфікація.

Основною перевагою застосування формальної специфікації є можливість виявлення проблем у системних вимогах. У неформальній специфікації легко упустити ці проблеми, які однаково будуть вирішені, але на більш пізній стадії процесу розробки ПЗ.

Завдання:

1. Банківські автомати використовують інформацію з картки клієнта, що надає ідентифікатор банку, номер рахунку і персональний ідентифікатор клієнта. Вони також одержують інформацію із центральної бази даних і вносять у неї зміни по завершенню транзакції. Використовуючи ваші знання роботи банкоматів, напишіть Z-схему, що визначає стани системи, перевірку картки клієнта і зняття коштів.

Питання:

1. Поясніть, чому архітектурне проектування системи повинне передувати розробці формальної специфікації.

2. Перед вами поставлене завдання “продажу” методів формальної специфікації організації, що розробляє програмне забезпечення. Як ви будете пояснювати переваги формальної специфікації скептично настроєним розробникам ПЗ?

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

4. Абстрактний тип даних, що представляє стек, має наступні операції:

New (Створити) ‒ створює порожній стек;

Push (Додати) ‒ додає елемент у вершину стека;

Тор (Вершина) ‒ повертає елемент на вершині стека;

Retract (Вилучити) ‒ видаляє елемент із вершини стека і повертає модифікований стек;Empty (Порожній) ‒ повертає значення істини, якщо стек порожній.

Визначите цей абстрактний тип даних, використовуючи алгебраїчну специфікацію.