Материал: DO178 Учебное пособие_в183
Первыми языками формализации были различные варианты языка математической логики, единственный недостаток которых – малодоступность широкому кругу заказчиков ПО. Попробуйте, например, объяснить заказчику, что логическая формула:
req Activate40: Forall (a:name, rest) (
~((queuesize(waiting)+queuesize(ready)+1) <= MaxNotSuspended) &
(processor = (Activate a).rest) &
(a in_set suspended) &
(BaseTask(a) |/ ExtendedTask(a))
-> after (Activate a)
(processor = rest)
);
является точной формализацией его требования, что активизация очередной задачи не происходит, если очередь активных задач уже полна! Поэтому большое развитие получили графические языки формализации, некоторые из которых стали промышленными стандартами: MSC[27], SDL, UML, UCM[28].
Например, поведенческое требование при установлении соединения по телефону: «Если набран допустимый номер, то этому номеру посылается вызов, а если номер не допустим, то вызывающий абонент получает сигнал «занято», на языке MSC может быть выражено диаграммой, представленной на Рис. 41.
Рис. 41. Формализация установления соединения между телефонами m и n
Если телефон m находится в состоянии idle (свободен) и его трубку снимают (offhook), то в вызывающем телефоне m появляется гудок (dialtone), после чего он переходит в состояние dial, и с этого телефона происходит набор номера n. Далее возможны два варианта (альтернативы – ALT). Если номер n допустимый (valid), то ему посылается сигнал вызова (ring), после чего аналогичный сигнал посылается вызывающему телефону m, и оба телефона оказываются в отношении установления соединения (ringing). Если же номер n недопустим (~valid), то вызывающему телефону m посылается сигнал «занято» (busy), и он переходит в состоянии занято (busy).
Подобные диаграммы, отображающие другие требования, могут объединяться вместе, создавая точные описания различных сценариев поведения данной системы.
Взаимодействие функциональностей
Важной и трудной проблемой в обеспечении правильного функционирования программной системы является так называемое взаимодействие функций (feature interaction), когда несколько правильно работающих функций системы перестают работать правильно при их интеграции в единый продукт. Эта проблема часто возникает при развитии программного продукта, функциональность которого наращивается поэтапно. Поиски причин нарушения целостности такой системы при добавлении новой функциональности (корректно реализованной и работающей правильно в изоляции) могут привести к серьезным переделкам кода и оказаться чреватыми к внесению в него новых ошибок. Возможной мерой предотвращения таких «сюрпризов» может быть исследование поведения системы на ее формальной модели.
Рассмотрим простую систему телефонной связи (Plain Old Telephone System – POTS), в которой реализованы три независимые функциональности: переадресация звонка (Forward), трехсторонняя связь (3WayCall) и ожидание (CallWaiting) – Рис. 42.
Рис. 42. Простая телефонная система с дополнительными функциями
Телефоны взаимодействуют между собой через установленные каналы связи телефонной сети и могут быть в состоянии «свободен» или «занят». В системе реализована переадресация звонка (Forward) и добавляются 2 независимые функции 3WayPhone и CallWaiting, которые, как выясняется, могут взаимно влиять друг на друга. Очевидная формализация отдельных шагов этих функций приведена на Рис. 43.
Телефоны m, n, и k все на связи; Телефон k кладет трубку и переходит в состояние idle; Телефоны m и n получают dialtone. req 3WAY teardown 2: Forall(m,n,k) ( rel(m,n,3wayconnected k) -> after(onhook k)( state(k,idle) & state(m,(idle;offhook m)) & state(n,(idle;offhook n)) & 3WAY k ) ); |
|
Трехсторонняя связь – 3WayPhone |
|
Телефон n ожидает соединения с k; Телефоны k и m соединены; Телефон m отсоединяется и переходит в состояние idle; k получает сигнал “busy” от m; Телефоны n и k становятся соединенными. req CW teardown 1: Forall(m,n,k) ( rel(k,n,cw hold connect m) -> after(onhook m) (state(m,idle) & rel(k,n,(cw hold connect m;onhook m)) ) );
req CW teardown 11: Forall(m,n,k) ( rel(k,n,(cw hold connect m;onhook m)) -> after(busy k.flash k) (rel(k,n,connected) & CW(k)) ) |
|
Ожидание – CallWaiting |
|
Рис. 43. Формализация отдельных шагов 3WayPhone и CallWaiting
Пусть теперь имеется 4 телефона С1, С2, С3 и Р1, причем Р1 с функцией трехсторонней связи. Рассмотрим, сценарий, представленный на Рис. 44.
1.
|
2.
|
3.
|
4.
|
Рис. 44. Пример незапланированного взаимодействия функциональностей
1. Пары телефонов (С1, С2) и (Р1, С3) соединены и ведут независимые разговоры.
2. Телефон Р1 переводит С3 в состояние ожидания трехсторонней связи и вызывает С2.
3. Телефон С2 переводит С1 в режим ожидания, после чего устанавливается трехсторонняя связь между телефонами Р1, С2 и С3.
4. Телефон Р1 кладет трубку и переходит в состояние «свободен». В какое состояние в этом случае переходит телефон С2? С одной стороны, по правилу 3WAY teardown 2 для трехсторонней связи оба телефона С2 и С3 должны получить сигнал dialtone; с другой стороны, по правилу CW teardown 1 телефон С2 должно получить сигнал «занято».
Исправить ситуацию; т.е., убрать возникшую неоднозначность, можно лишь при дальнейшем уточнении поведения телефонов, когда присутствуют эти новые функциональности.
Интегрированная технология анализа и верификации
Рассмотрим для примера интегрированную технологию для анализа и верификации телекоммуникационных приложений [29].
Базой для применения технологий верификации является формальная модель приложения, которая строится вручную по исходным неформальным требованиям, описывающим его поведение, с применением определенных средств автоматизации. После того, как модель построена, к ней применяются различные инструментальные средства, проверяющие выполнимость определенных ее свойств (непротиворечивость, полнота и другие). В случае корректности модели автоматически создаются тестовые наборы, гарантированно покрывающие исходные требования в соответствии с заданным критерием покрытия.
Как правило, спецификация формальной модели состоит из описания среды, включающего декларацию агентов и типизированных атрибутов, переходов, и проверяемых свойств. Агенты работают параллельно, асинхронно и взаимодействуют между собой посредством чтения и изменения атрибутов. Состояние среды состоит из набора значений ее атрибутов и значений атрибутов всех действующих агентов.
Переходы между состояниями модели записываются на языке «базовых протоколов» [30]. Базовый протокол представляет собой выражение вида тройки Хоара: α → <u> β , где α – предусловие, u – процесс (действие), β – постусловие, и описывает атомарный параметризированный (имя агента – один из параметров) переход модели. Пред- и пост-условия являются формулами логики первого порядка. Постусловие также может содержать операторы присваивания.
Процесс базового протокола представляет собой линейную последовательность конструкций MSC, в терминах которых часто специфицируют телекоммуникационные приложения. Преимущество этого формализма так же в простоте и эффективности использования методов верификации – язык использует базовый набор структур данных и операций над ними, и при этом обладает достаточной выразительной мощностью для описания систем, специфицированных в таких инженерных языках, как MSC, SDL, UML .
В описываемой системе верификации осуществляется проверка таких свойств, как недетерминизм, выход за пределы допустимых значений, переполнение, обращение к неинициализированному элементу системы, а так же проверка условий безопасности, достижимости и отсутствия тупиков. Всякий раз, когда достигнуто состояние, в котором нарушается одно из перечисленных свойств, будет построена трасса, которая иллюстрирует поведение модели из ее начального состояния в текущее.
Трасса представляет собой последовательность имен переходов модели (т.е. имен базовых протоколов с их фактическими параметрами), а так же может быть построена из событий (конструкций MSC), заданных в процессной части базовых протоколов. Такие события описывают наблюдаемое поведение модели, и могут быть использованы в качестве сценарных тестовых контр-примеров.
Недетерминизм (non-determinism) в модели является не ошибкой ее поведения, а лишь сигналом для дальнейшего анализа. Важно отделить естественный недетерминизм от непреднамеренного. Некоторые системы верификации проверяют недетерминизм путем введения специальных атрибутов, значения которых выбираются недетерминировано в процессе моделирования.
Выход за пределы допустимых значений (out-of-range) – распространенная ошибка, часто являющаяся источником нарушения безопасности систем. Проверка обеспечивается путем генерации дополнительных ограничений на индексацию в пред- и пост-условиях переходов (обращение к элементу массива, параметризированному атрибуту, либо при обращении к процессу по индексу).
Переполнение (over/underflow) определяется таким образом: арифметические выражения, согласно приоритетам операций, раскладываются на эквивалентную последовательность вычислений значений бинарных операций, вводятся вспомогательные локальные переменные для хранения и дальнейшего использования результата предыдущих вычислений, и перед каждым производится проверка на возможное переполнение.
Проверка использования неинициализированного атрибута (non-initialized variable) обеспечивается посредством (неявного) введения вспомогательных атрибутов, цель которых – хранить информацию об инициализации каждого атрибута модели и генерировать дополнительные проверки таких атрибутов. Если производится присваивание, в правой части которого есть неинициализированный атрибут, то переход осуществляется, а атрибут, стоящий в левой части присваивания становится неинициализированным.
Условия безопасности (safety, liveness) выражаются формулами линейной темпоральной логики (LTL – Linear Temporal Logic). В качестве примеров можно привести такие свойства: «лифт никогда не едет с открытой дверью», «выделенный ресурс когда-нибудь освободится», и т.д.
Проверка достижимости выполняется как для целевых состояний, так и для переходов. Целевое состояние формулируется пользователем в виде LTL-формулы. При окончании работы генерируется вердикт, включающий в себя информацию о статистике выполнения переходов.
Тупиковой (deadlock) называется ситуация, из которой нет ни одного допустимого перехода.
Замкнутой (livelock) называется ситуация, из которой нет возможности достигнуть хотя бы одно состояние, достижимое из начального (initial) состояния. Другими словами, условие отсутствия livelock можно сформулировать так: каждое достижимое состояние должно быть достижимо из любого изначально достижимого состояния. Проверяется так же, как и «сильная связность» в терминах теории графов.
В качестве средства формализации требований на поведение приложений наряду с традиционными языками используются UCM-диаграммы, позволяющие представить реализацию требований в виде совокупности взаимодействующих процессов в нотации, доступной для контроля заказчиком, что позволяет сохранить соответствие семантики генерируемых поведенческих моделей семантике исходных требований.
Конечный UCM-проект представляет собой набор связанных и структурированных диаграмм, каждая из которых состоит из последовательности элементов нотации среди которых элементы описания событий, параллелизма, таймеров, прерываний и т.п. В совокупности набор диаграмм задает возможные поведения системы, описанные в требованиях. На Рис. 45 приведена одна из UCM-диаграмм для телекоммуникационного протокола CDMA.
Рис. 45. Пример UCM-нотации для протокола CDMA