И. Соммервилл - Инженерия программного обеспечения (1133538), страница 51
Текст из файла (страница 51)
Таким образом определяется поведение системы. 'Для разработки спецификаций, основанных на системных моделях, используются системы нотаций методов 'Л)М (192, 193», В (548] и Х (158, 325]. Здесь я использую нотацию метода Х. В этом методе система описывается на основе теории множеств, которая дополняется специальными логическими структурами, разработанными для специфицирования программных систем. Полное описание метода Х очень объемно.
Поэтому я представлю несколько небольших примеров для иллюстрации метода и приведу необходимые обозна. чения. Полное описание метода Х дается в [98. 547, 84]. Формальные спецификации могут быть трудными для чтения и громоздкими, особенно если используются большие математические формулы. Это замедляет разработку ПО. Разработчики метода Х обратили внимание на эту проблему. В этом методе спецификации 198 Часть 11. Требования представляются как неформальный текст, дополненный формальными описаниями. Формальная часть спецификации состоит из небольших простых описаний (называемых схе. мами), которые визуально отделяются от остального текста спецификации (рис.9.8).
Схемы используются для введения переменных состояний и определения ограничений и операций иад состояниями. В иетоде также предусиотрены операции, выполняемые над схемами, в частности для построения, переименования и сокрытия схем. Имэ савы Сапаттра самы Схемныд врщяшт (Ъс 9.8, Сж(тук эту)тп Встсмтк Сигнатура схемы определяет сущности, которые составляют состояние системы, схемные предикаты — это набор условий, которые должны быть всегда истинны дтя этих сущностей. Если схема определяет операции, предикаты могут представлять пред- и постусловия для этих операций.
Длл иллюстрации применения метода Х в разработке спецификации критической системы рассмотрим упрощенный пример системы инсулинового насоса. используемой диабетиками. У диабетиков нарушен естественный метаболизм сахара, им требуются инъекции инсулина- гормона, необходимого лля метаболизма глюкозы. Данная система контролирует уровень сакара в крови больного и, если требуется, производит автоматическую инъекцию инсулина. Этот пример также использован в части 1У, где рассматривается разработка критических систем, Уровень сахара в крови больного проверяется через равные промежутки времени, и, если он увеличивается, производится инъекция инсулина, которая понижает уровень сахара.
Иа рис. 9.9 показана структура инсулинового насоса. 1. Набе)т ксс Подсоединены к насосу, используются для инъекции инсулина в тело диабетика. 2. Датчкк. Измеряет уровень сахара в крови больного. В формальной спецификации операция получения данных от датчика названа гедд(пд?. 8. Насос. Передает инсулин из резервуара к набору игл. В формальной спецификации величина дозы инсулина названа бове. 4. Утфаэлякквее усмройсавп Управляет объектами системы. Имеет переключатель "Включено — Выключено", кнопку отмены и кнопку установки дозы инсулина. Для упрощения формальной спецификации эти элементы управления не описаны. 5. Упгфокство авлркйксб сигнализации.
Подает звуковой сигнал при возникновении проблем. В спецификации сигнал на входе устройства аварийной сигнализации обозначен как а1апп!. 6. Икдиклжоры. Имеется два индикатора: один показывает последний анализ уровня сахара в крови, другой — информацию, выдаваемую системой пользователю. Эти индикаторы в формальной спецификации обозначаются б(вр(ву11 н б1вр!ву2!. 7. Часы. Обеспечивают управляющее устройство значением текущего времени. Даже для нсболыпой системы, подобной системе управления инъекциями инсулина, формальнэл спеттифиюция довольно обширна. Хотя основные системные операции просты, существует много аварийных ситуаций, которые необходимо учитывать.
Здесь приведены только некоторые из основных Х схем спецификации и объяснено, что они означают. 9. Формальные спецификации ПО 199 Рис. 9.9. Ювоквзглил иивуликовово илсогл Основнал схема 1пяйп-ршпр (инсулиновый насос), которая моделирует состояния инсулино. вого насоса, показана на рис. 9.10. Схема разбита падве части. В верхней части обвиваются имена и типы, в нижней приведены условия, которые должны всегда выпал юпъсл. Рис 9.10. всхлип инсувинового илсосл Состояние системы моделируется посредством ряда переменных. В соответствии с со.
глашениями, принятыми в методе Х, имена, заканчивающиеся знаком ?, используются для представления входных данных, а имена, заканчивающиеся знаком й представллют выходные данные. В схеме инсулинового пасоса объявлены следующие имена. 1. геаб(пй?, Это неотрицательное целое число, которое предсгавляет данные от дат чика, определяющего количество сахара в крови. Зто входная величина. 2.
бове, сипи(айке бозе. Зто также натуральные числа, представляющие соответственно дозу инсулина и суммарную дозу инсулина, введенную за определенный период времени. 3. гй, г1, г2. Представляют последние три значения, полученные от датчика, и исполь. зуются для вычисления изменения сахара в крови. 4. сарасйу. Натуральное число, представляющее объем инсулина в хранилище (резервуаре). 5. а)апп!.
Зта выходная величина сообщает об аварийных ситуациях в системе. 6. рщпрй Зто натуральное число, представляющее управляющие сигналы, посылае. мые к физическому насосу. 200 Часть 11. Требования 7. б!вр)ау11, б!вр1ау21. Эти выходные величины строкового типа представляют два текстовых индикатора. Один индикатор используется для отображения текстовых сообщений, другой — для показа введенной дозы инсулина.
Схемные предикаты определяют ряд условий, которые всегда должны быть истин ными. 1. Доэадолжна быть меньше или равна количеству инсулина в резервуаре. 2. Однократная доза не должна превышать 5 единиц инсулина, а общая доза, введенная за определенный промежуток времени, — 50 единиц инсулина. Это условия безопасности, которые рассматриваются в главе 17. 3. 0)вр!ау1!. Показывает сообщения о состоянии иисулинового резервуара. Если резервуар содержит 40 или больше единиц инсулина, сообщений нет.
Когда в резервуаре инсулина от 10 до 40 единиц, на дисплее отображается предупреждение, если же в резервуара меньше 10 единиц, звучит звуковой сигнал и отображается соответствующее предупреждение. Работа инсулинового насоса заключается в определении каждые 10 минут количества сахара в крови пациента и введении инсулина, если уровень сахара увеличивается (это очень упрощенное описание). Вводимое количество инсулина вычисляется согласно схе. ме 008АОЕ (Дозировка), которая приведена на рис. 9.11. Из этой схемы видно.
что на вводимую дозу влияет множество различных факторов. )Ъс 811. Хллсчя вмчкомиил дым На рис. 9.11 показано часто используемое средство метода 2, а именно дельта. схема. Если имя схемы включено в раздел описаний, то это равносильно включению всех имен данной схемы, а ее условия включаются в предикатную часть. В данном случае в схему 008АОЕ включаются имена и условия схемы (пвц))п Ривар. Если имени схемы предшествует символ Ь, то вводится новый набор величин, имена которых совпадают с именами данной схемы, но к ним добавляется символ ' (апостроф). Так обозначаются значения пе.
ременных состояний, измененные после выполнения операции. Например, если операция изменяет значение переменной ча1, то погле операции эта переменная будет обозначаться ча)'. Дельта. схема 008АОЕ вводит имена сарасйу', сцтц!а!!че бове' и т.д. 9. Формальные спецификации ПО 201 Схемы, моделирующие выходные данные инсулинового насоса, показаны на рис.
9.12. Это модели индикаторов и устройства аварийной сигнализации. Здесь также используется дельта. схема. Из схемы 018Р(.АУ видно, что индикатор б)вр)а)г2! показывает вычисленную дозу (Ме( 1о в1ппй — функция преобразования), индикатор бМр!еу1! отображает или пре. дупреждающее сообщение, или ОК. В схеме А(.АЙМ покззаны условия, когда аативизируе гся аварийная сигнализация. Она включаегсл, если уровень сахара в крови очень низкий (меньше 3) или слишком высокий (больше 90). Рис 9.12 Схемы вмходньи дпнимк Предикаты во всех У:схемах должны бытьсогласованы, т.е. не должно быть условий в одной схеме, которые противоречат предикатам в другой схеме.
Если в спецификации замечены противоречия, можно применить различные математические методы анализа Е-спецификации. Здесь я не буду их описывать. Рассматривая представленные четыре Х-схемы, вы могли заметить противоречия, которые я сознательно ввел. но которые могли бы появиться в реальной спецификации. В общей схеме инсулинового насоса !пэпйп Ригпр установлено, что индикатор бмр)ву1! должен показывать состояние резервуара инсулина. Однако в схеме 018Р(.АУ этот индикатор должен показывать уровень оэхара в крови, Здесь противоречие, которое следует разрешить при обсуждении системы с медицинскими экспертами и потенциальными пользователями. Я не делал модели поведения системы во времени (в действительности нужно учитьг вать, что датчик контролирует уровень сахара в крови каждые 10 минут).
Хотя это, конеч. но, возможно, но довольно громоздко; по.моему, неформальное описание действий более кратко и понятно, чем формальная спецификация. Основным преимуществом применения формальной спецификации является возможность выявления проблем в системных требованиях. В неформальной спецификации лег. ко упустить эти проблемы, которые все равно будут решены, но на более поздней стадии процесса разработки ПО. ~ э ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ! ~~ ~ ~ ~ ~ ~ г ~ КЛЮЧЕВЫЕ ПОНЯТИЯ ..
э. ь ' ". . ' ' ' ' .Р г > ° методы фсрмальнсй сисгилюй аицифишции дшюимют мшоды гифсргшансй аицяфиагвеь Они шиут испаиасвзться дш двшвизвциФ специфиации нефсрывльнык сисгемньц гребоввннй. Фсрмвлы- ! ные специфншции шляюгся мостом мвгду аюгемными гребоввними и сисгшнгй зрппшгурсй, Формальные 'спецификации точны и однозначны. Они устраняют 'темные' области в специфша' ' " ' ции и проблемы неоднозначного толкования гребований.' Вместе с тем формальные спецификации . трудны для понимания неспецивлисгами. ' 202 ккасть И. Требования '- ° Ь':Основным "преймупществомтформахльных, мчетойсов',бйьйлетщ У)р)зеодится'йа ранней стадий 3ззрбботв ПО,' Исйравмййе аййбенйе мзч)венений' в, зш(оцченнУю'системУь М3тоу'~$5рнмаслыш(( счпепцпфгпюп(г(3',йвнболие.'Йодш)(В~у()(я безопшхюсть,' бвйпйносгь, и."защю(еннйбть",Сйстеиы! ~собвн ,ЙааТься дпя разработки стандартов,'„".,-, .:, "'.",~~ г ф у(йшпцзфейс шуюдшйьгкм('йабо(з куюссшг сбьшгткв нви абстрбютккх , М'~~ спанив',сищемы и еще()ваяют ее в ярмапх отнпненймп(уй) ,.';"::-е,"' МвтОдЫ.фОРМаЛЬНОй СПЕцйфмацИИг ОСНОВаННЫЕ.На СййтдМНЫВ)МО()Вам~,'"" ' " ':КМтя)лат)(яеж$ ччь'.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
