Содержание к диссертации
Введение
Глава 1. Проблема разработки требований к поведению программ ных систем логического управления 9
1.1. Методы разработки требований к поведению программных систем логического управления
1.2. Постановка задачи разработки функциональных требований к поведению программных систем логического управления 18
1.3. Описание контекстных требований на языке LTL 26
1.4. Пример программной системы логического управления 32
Выводы по главе 1 35
Глава 2. Выявление и формализация контекстных требований 36
2.1. Проблема выявления темпоральных требований методом схем целей 36
2.2. Модификация метода схем целей для выявления контекстных требований 40
2.3. Трансляция схем контекстных требований в LTL–формулы 47
Выводы по главе 2 54
Глава 3. Символьный алгоритм трансляции LTL–формулы в автомат Бюхи 56
3.1. Постановка задачи трансляции LTL-формулы в автомат Бюхи 57
3.2. Символьная трансляция LTL-формулы в обобщенный автомат Бюхи 67
3.3. MINCFG: алгоритм построения сокращенной ДНФ в бинарных решающих диаграммах 80
3.4. Детали реализации алгоритма SymLTL2BA 89
3.5. Тестирование и сравнительный анализ реализации SymLTL2BA 99
Выводы по главе 3 104
Глава 4. Применение метода разработки формальных контекстных требований при верификации СУЭС 106
4.1. Объединение этапов метода разработки формальных контекстных требований 107
4.2. Разработка контекстных требований к СУЭС 112
4.3. Верификация контекстных требований к СУЭС 122
Выводы по главе 4 132
Заключение 134
Список сокращений и условных обозначений 135
Словарь терминов 136
Предметный указатель 137
Список литературы
- Постановка задачи разработки функциональных требований к поведению программных систем логического управления
- Модификация метода схем целей для выявления контекстных требований
- MINCFG: алгоритм построения сокращенной ДНФ в бинарных решающих диаграммах
- Разработка контекстных требований к СУЭС
Постановка задачи разработки функциональных требований к поведению программных систем логического управления
Задачей программной системы как реагирующей, является поддержание определенных шаблонов взаимодействия с окружением. Поэтому в данной работе выдвинута гипотеза, что значительная часть функций системы связана именно с реакцией на поведение окружения. Под окружением подразумеваются другие программные компоненты, оборудование, пользователи.
То, что поведение окружения влияет на управляющую систему, было отмечено давно [3, 43, 44]. В работах [29, 55, 63] исследуется влияние поведения окружения на сложность методов проверки модели в зависимости от темпоральной логики [29, 55, 63], используемой для задания требований. Проблема поведения окружения возникает при композициональной верификации в парадигме “предположения-гарантии” (assume-guarantee) [8, 18, 38, 55, 64, 76]. Композицио-нальная верификация направлена на уменьшение размера системы, проверяемой за один шаг итерации. Для этого система разбивается на модули, каждый из которых верифицируется отдельно относительно заданного требования. Часть системы, не вошедшая в модуль, играет роль его окружения. В работах [19, 37] предложен алгоритм, позволяющий автоматически строить предположение о поведении окружения заданной модели реагирующей системы. Эти работы дали толчок исследованиям, связанным с проблемами генерации предположений о поведении окружения: символьное построение предположений [5, 7], уменьшение алфавита предположения [35, 90], замена модулей для инкрементальной разработки программ [28], минимизация предположений [15, 40], расширение гарантируемых требований до требований живости [13, 32], вероятностное обучение предположений [33] и т. п. Алгоритмы, предлагаемые в работах, приведённых выше, реализовывались в различных верификаторах Bandera, ComFoRT, JavaPathFinder, SMV, LTSA, Verilog.
Другое направление учета поведения окружения связано с проверкой корректности самих темпоральных требований. Темпоральная формула, выражающая требование, называется реализуемой (realizable) или синтезируемой [2, 77], если существует модель этой формулы, реализуемая на практике. Модель называется восприимчивой (receptiveness) [23] к требованию живости, если любое безопасное вычисление этой модели может быть продолжено трассой требования живости независимо от поведения окружения. Понятие машинной независимости или машинной замкнутости требования живости, введенное М. Абади и Л. Лэмпортом [1], есть другая формулировка этого же критерия. От критерия восприимчивости зависит композициональность модели. В некоторых работах [1, 23] требования, проверяемые относительно этих критериев, специфицируются в традиционных темпоральных логиках, таких как LTL, CTL. В работе [4] для задания требований предложена темпоральная логика альтернирующего времени Alternating–Time Temporal Logic (ATL). Она позволяет указывать в требовании конкретный модуль системы, инициировавший событие. Этот подход реализован в пакете MOCHA. В работе [86] показано, что критерии могут быть решением задачи выполнимости на квантифицированных булевых формулах. Подход был реализован в программном средстве SpecChecker.
Однако учет поведения окружения при разработке требований к поведению реагирующих систем в доступных источниках найти не удалось.
Взаимодействие системы с ее окружением в общем случае может быть самым разнообразным. Полагая, что основную роль в обеспечении согласованной работы внешних механизмов и агрегатов играет функция выполнения системой управления специфической реакции на полученное конкретное внешнее воздействие, будем рассматривать в работе только две функции программной системы логического управления, зависящие от поведения окружения: 1) функцию отклика — обеспечивать специфическую реакцию на внешнее воздействие, 2) функцию предшествования — обеспечивать отсутствие реакций в отсутствии внешнего воздействия. Будем составлять и впоследствии верифицировать требования на основе этих двух функций системы, расширенных в нескольких отношениях. Такие требования назовем контекстными.
Темпоральное отношение, соответствующее первой функции, назовем отношением отклика — система должна когда-нибудь в будущем гарантировать специфическую реакцию на конкретный запрос окружения. Темпоральное отношение, соответствующее второй функции, назовем отношением предшествования — если сейчас нет события, характеризующего реакцию системы, и оно когда-нибудь выполнится в будущем, то реакция не произойдет до тех пор, пока от окружения не поступит запрос. Чтобы сформировать контекстные требования, в которых гарантируются отношения, сопоставим им временные области или фазы поведения: начальная фаза, глобальная и регулярная фазы, финальная фаза. Они встречаются в спецификациях, например, системы управления энергоснабжением судна, системы управления бомбардировщиком A7-E [91] и др. Эти временные области аналогичны тем, что определялись в [27] под названием “scope” — область действия.
Метод разработки контекстных требований будем строить на основе метода схем целей [48]. Этот метод предоставляет развитые и относительно простые механизмы структуризации предметной области. Он позволяет выделить объекты, влияющие на выполнение требования, включая объекты окружения, определить связи между объектами и разделяемые события, обеспечивающие эти связи. Хотя метод схем целей изначально применим для статических отношений, его модификация для задания контекстных требований и будет одной из задач исследования.
Модификация метода схем целей для выявления контекстных требований
На практике требования к программным системам не удается разработать сразу, поскольку приходится структурировать большой объем слабо систематизированной информации, представленной в неформальном описании программной системы.
В целеориентированном методе выявления требований, методе схем целей М. Джексона, с каждой целью связаны объекты. Под объектами цели понимаются объекты реального мира (или представляющие их сущности в формулировке цели), взаимодействующие при реализации этой цели. Объекты цели, взаимодействуя, обмениваются, так называемыми,феноменами будущей программной системы (события, переменные, константы, отношения). Вся информация о цели компактно собирается на схеме этой цели. Для задания схем целей имеется графический язык. В начале выявления требований представление о целях системы размыто. Такая цель описывается составной схемой. Последовательно составная схема уточняется, насыщается деталями, меняется ее структура.
М. Джексоном сделано предположение, что все многообразие целей программ сводится к ограниченному набору целей-прототипов. Он сформулировал пять целей-прототипов: RBV (требуемое поведение — required behaviour), IRL (простой запрос - simple enquiry), DIS (отображение информации — information display), EWP (групповая обработка — simple workpieces), TRM (преобразование — transformation) [50]. Эти цели отражают шаблоны отношений, реализуемых программами чаще всего. Такие цели описываются поименованными элементарными схемами. Элементарные схемы имеют фиксированную структуру, они не требуют дальнейшего уточнения в данном методе. Например, элементарная схема TRM определяет цель преобразования данных на заданном входе. Схема RBV задает цель требуемого поведения. Множество целей-прототипов М. Джексон оставил открытым.
Выявление требований методом схем целей М. Джексона кратко можно сформулировать так: 1. из неформального описания системы определить цель и требование (возможно в самом общем виде), всю дальнейшую информацию вносить на схему; 2. для этой цели составить объекты, взаимодействующие при ее реализации, и интерфейсы, через которые они взаимодействуют; 3. на интерфейсах определить феномены, которыми обмениваются объекты при реализации цели (если возможно); 4. сформулировать феномены в терминах переменных (если возможно); 5. если схема (и тип цели) совпала с одной из элементарных, то формулируем развернутое требование. Иначе процедура выявления требования продолжается: схема и цель уточняются дальше (либо дополняется информация о це КД: остановиться callAnywliere(n),,-- _atFlopr(n)_&_ _, Обработка ч%, doorOpen \вызова лифта, Рис. 2.1. Схема обработки вызова лифта ли), либо цель разбивается на несколько и шаги повторяются для каждой новой цели. Продемонстрируем язык схем целей на примере.
Из этого описания объектами цели являются “Внешний домен” (пользователь, двигатель лифта, геометрия шахты и т. п.) и собственно система управления лифтом, назовем ее в этой цели “Контроллер движения лифта”. На схеме цели (рис. 2.1) объекты изображаются прямоугольниками. Главный объект схемы называется “машиной”. Машина по М. Джексону — функция будущей программной системы в соответствии с данной целью. Машина не обязана реали-зовываться как модуль системы. Машина задается на схеме прямоугольником с двумя вертикальными чертами (“Контроллер движения лифта” на рис. 2.1).
Интерфейсы объектов изображаются на схеме прямыми сплошными линиями. Феноменами нашей неформальной цели являются события “вызов лифта”, поступающий от “Внешнего домена”, события “двигаться” и “остановиться”, поступающие от “Контроллер движения лифта”. Феномены определяются на схемах надписями в формате Объект: феномен . На рис. 2.1, например, “КД: двигаться” означает, что “Контроллер движения” дает команду двигателю лифта начать движение.
Название требования, соответствующего цели, на схеме формулируется ко 39 ротко на естественном языке в овале с пунктирной границей (“Обработка вызова лифта”). Требование обработки вызова можно предварительно сформулировать так: “Если поступил вызов, то лифт когда-нибудь прибудет на данный этаж и остановится”.
Вне схемы должно быть сформулировано развернутое требование. Для этого определим некоторые переменные: п — номер этажа, с которого или на который поступил вызов, call Any w her е(п) — утверждение истинно, если вызов на этаж п поступил (с площадки или из кабины лифта), atFloor(n) — утверждение истинно, если лифт находится на этаже п, doorOpen — утверждение истинно, если дверь лифта открыта. Переменные указываются на схеме на штрихованных прямых линиях, связывающих объекты и требования.
Схема на рис. 2.1 есть по структуре элементарная схема RBV. Такая схема определят требуемое поведение системы перечислением событий. На рис. 2.1 это события — callAnywhere{n),atFlovr{n) и doorOpen.
В соответствии с целью управления развернутое требование к ограничению пропуска этажа естественно было бы задать следующим образом: Требование 2.2. “Если поступил вызов call Any wherein), то когда-нибудь в будущем лифт доедет atFloor(n) до этого этажа и откроет двери doorOpen .
В требовании 2.2 задаются темпоральные причинно-следственные отношения между событиями. Однако в методе схем М. Джексона механизмы, позволяющие устанавливать последовательность событий, отсутствуют. Такие отношения М. Джексон предлагает определять отдельно, вне схем, другими средствами, например, системой переходов [48].
MINCFG: алгоритм построения сокращенной ДНФ в бинарных решающих диаграммах
Определим процедуру выявления контекстных требований при помощи модифицированного языка схем целей. 1. Из неформального описания системы определить цель и требование (возможно, в самом общем виде), всю дальнейшую информацию вносить на схему. 2. Для этой цели составить объекты, взаимодействующие при ее реализации, и интерфейсы, через которые они взаимодействуют. 3. На интерфейсах выделить события, инициируемые объектами окружения системы при реализации цели. 4. Определить события реакции системы к найденным событиям окружения. 5. Сформулировать события в терминах переменных. 6. Если возможно сформулировать локальное отношение отклика или предшествования с полученными событиями, определив цепочки стимулов и реакций и их условия, то зафиксировать цель гарантии соответствующего отно Управляющая Машина
Элементарные схемы требований во временных фазах. шения в элементарной схеме отношения (рис. 2.2). 7. Погрузить локальное отношение между стимулом и реакцией во временную фазу, соответствующую неформальному описанию системы. Результат фиксируется в элементарной схеме временной фазы (рис. 2.3) и сформулировать соответствующее развернутое контекстное. Данная процедура выполняется для всех событий, инициируемых окружением из неформального описания. Если для какого-либо события согласно предложенной процедуре не удалось установить контекстное требование, то, возможно, техническое задание неполно или противоречиво. В этом случае необходимо выяснить семантику события с заказчиком.
Модификация метода схем такова, что для требований, отличных от контекстных, сохранена возможность использования оригинального метода схем целей. Одним из частных случаев, не описываемых ни одной из предложенных элементарных схем, будет требование с бесконечным поведением окружения. Оно должно задаваться отдельно. Для этого вида контекстных требований не предложен шаблон, поскольку поведение окружения может быть любым, описываемым LTL-формулой, т. е. нельзя установить ограниченный порядок событий.
Пример 2.2. Применим модифицированный метод схем целей к составлению требования 2.1 обработки вызовов системы управления лифтом [107] из примера 2.1.
Событие “ВД: вызов”, инициируемое пользователем как частью окружения, стимулирует систему начать обслуживание. Следовательно, оно инициирует отношение отклика как стимул. Простейшей реакцией системы будет прибытие лифта на этаж. Однако при поступлении вызова из кабины лифта эта реакция может быть уточнена: потребуем чтобы после того, как пользователь нажал кнопку этажа в кабине лифта, лифт, подъезжая к этому этажу, остановится, не проехав мимо. Это требование на естественном языке формулируется так:
Реакция системы управления на вызов из кабины (лифт находится на этаже вызова, и двери открыты) ограничена в данном случае условием, что лифт не находится на этаже вызова. Иными словами, требуемая реакция состоит в последовательности событий “лифт не на этаже вызова” до тех пор, пока наступят события “лифт на этаже вызова”, и “двери открыты”. Т. о., имеется вся информация для составления схемы отношения (рис. 2.4а). Развернутое требование локальной обработки вызова из кабины лифта будет таким: “Если поступил вызов из кабины лифта callCab{n) на этаж п, то когда-нибудь в будущем лифт будет на этом этаже atFloor (п), и двери лифта будут открыты door Open, а все время до этого лифт будет находиться вне этого этажа atFloor (n)”.
Отношение отклика должно выполняться в каждом состоянии системы, т .е. в глобальной временной фазе функционирования системы. Схема глобальной обработки вызова приведена рис. 2.4б. Развернутая формулировка получившегося контекстного требования будет такова: “Всегда, если поступил вызов из кабины лифта callCab{n) на этаж п, то когда-нибудь в будущем лифт будет на этом этаже atFloor (п), и двери лифта будут открыты door Open, а все время до этого лифт будет находиться вне этого этажа atFloor (n)”.
Предложенная модификация метода схем целей позволяет выявлять кон 47 текстные требования, которые в отсутствии метода выявить не удается. Группе студентов старших курсов из 27 человек при изучении курса “Верификация распределенных алгоритмов и систем” было предложено по неформальному техническому заданию, подобному приведенному в разделе 1.4, к системе управления лифтом составить требования к поведению системы, разработать модель системы и верифицировать ее. Не используя предложенный здесь метод, из 18 спецификаций требований студентами было сформулировано 1 контекстное требование 2.2 в 16 — одно другое контекстное требование Б.3. При этом в 11 моделях из 18, в спецификациях которых было требование 2.2, при верификации нарушалось требование 2.3, в 1 случае — требование Б.2. Из 7 моделей, в которых требование 2.3 выполнялось, в 2 нарушалось требование Б.1. Когда же аналогичная группа студентов составляла требования по модифицированному методу схем целей, то они смогли выявить все контекстные требования. Использование модифицированного метода схем целей позволяет не пропустить контекстные требования и, как следствие, исключить в разрабатываемой системе ошибки, связанные с нарушением этих требований. Кроме того, студенты отметили, что выявление требований по предложенному методу существенно упрощает процесс их составления.
Разработка контекстных требований к СУЭС
Изначально SPIN находит ошибку на глубине 368935, связанную с отсутствием обработки сообщения OnCommand (от контроллера генераторного автомата) в инициализационном режиме контроллера электростанции. В результате электростанция “зацикливалась” в инициализационном режиме, оператор терял над ней контроль.
После добавления обработки сообщения при верификации формулы (4.8) SPIN обнаружил контрпример на глубине 29915.
Последовательность действий, приводящая к ошибке, сводится к тому, что основная электростанция 2, переходя в защитный режим, отправляет запрос на резерв 5:0nReservComm на 208 шаге. Резервная электростанция 1 в неактивном защитном режиме (6) получает запрос на 4610 шаге. Электростанция 1 переводится в переходный режим (4), лампа “ДГ1 Пуск” начинает мигать. На 7192 шаге контроллер электростанции 1 отправляет команду о старте генераторного автомата OnCom. Контроллер генераторного автомата 1 в неактивном режиме (3) получает эту команду на 7568 шаге, включает генераторный автомат. На шаге 9594 к контроллеру электростанции в переходном режиме (4) приходит сообщение об отключении генераторного автомата Of f Com. Оно было послано контроллером генераторного автомата при переходе в неактивный режим на 826 шаге. Контроллер электростанции 1 по этой команде возвращается в неактивный защитный режим (4). Когда на 12674 шаге контроллер электростанции 1 получает сообщение об успешном запуске генераторного автомата OnCom, он его отбрасывает.
На рис. 4.8 приведена часть описываемого контрпримера, связанная с отправкой сообщения OnCom контроллером электростанции 1 (это второй процесс слева) на 7192 шаге контроллеру генераторного автомата 1 (третий процесс слева). Синхронизация процессов по сообщению отмечается в контрпримере SPIN красной стрелкой. На рис. 4.8 видно пересечение двух красных линий: вторая красная линия относится как раз к синхронизации по сообщению Of f Com, которое было отправлено контроллером генераторного автомата раньше. Именно это сообщение и отключит впоследствии активизацию резервного двигателя.
Данную ошибку невозможно обнаружить на стенде, т. к. там невозможно воспроизвести ситуацию с бесконечно частым отключением устройств одной из электростанций. Ее крайне трудно обнаружить и при программном тестировании, поскольку она получается при достаточно редком стечении обстоятельств. В результате такого поведения судно оказывается, фактически, без электроснабжения, и контроль над управлением может быть потерян полностью.
Разработчики, наблюдая подобное поведение ранее при ходовых испытаниях, были убеждены, что оно вызвано несанкционированным срабатыванием техники — генераторного автомата. Поэтому они включили в код программы управления многочисленные проверки состояния генераторного автомата, что не приводило к успеху. Организация специализируется на таких системах управления, и то, что сделано в этой системе управления — принятый метод разработчики подобного ПО.
На самом же деле, причиной такого поведения является чередование асинхронных процессов: в силу разницы скоростей происходила рассинхронизация переключения генераторного автомата и остальных модулей, поэтому обработка сообщений от него отсутствовала во многих режимах. Как следствие, когда СУЭС была уже готова обрабатывать сообщения от контроллера генераторного автомата, то создавалось впечатление, что автомат переключился без команды. Чтобы устранить эту ошибку, необходимо переводить модули в стабильные (непереходные) режимы, только когда подчиненные им модули и оборудование уже вышли в стабильные режимы.
Заметим, что успешная проверка выполнения требований, для которых была необходима модель СУЭС с двумя электростанциями, проходила, в основном, только в аппроксимационном режиме. В точном режиме для верификации модели не хватало памяти и глубины поиска.
В заключение заметим, что программный код СУЭС был тщательно протестирован разработчиками этой системы до того, как был передан нам. При этом при верификации каждое проверяемое контекстное требование нарушалось не единожды: общее количество ошибок 141. Т. е. ошибки, найденные при верификации, не были установлены ни во время тестирования, включавшего 841 тест, ни во время 23 стендовых испытаний. В основном, найденные ошибки были связаны с нарушениями режимов функционирования системы и легко устранялись. Однако три ошибки были критическими. Одна из них относилась к наличию реакции системы на неполное срабатывание генераторного автомата в некоторых режимах. В результате СУЭС включалась независимо от текущих действий оператора. Вторая ошибка состояла в неконтролируемом выходе СУЭС из состояния защиты. Как следствие, на оборудование мог подаваться ток при производстве на нем работ. Третья ошибка состояла в отсутствии подключения запрашиваемой резервной электростанции. При этой ошибке СУЭС теряла управление над оборудованием. Основной причиной этих ошибок было то, что разработчикам не удавалось проанализировать поведение асинхронных систем: получение события, отложенное во времени из-за чередования действий независимых модулей системы, не обрабатывалось должным образом. Сложность исправления этих ошибок составила 80% трудоемкости создания программного продукта. Параллельно и независимо с разработкой и верификацией модели проводились ходовые испытания судна, на котором была установлена исходная реализация СУЭС. При ходовых испытаниях было выявлено несколько ошибок. В частности, появилась критическая ошибка блокировки управления, когда система управления неожиданно перестала отвечать на команды и отключила энергоснабжение. В результате судно загородило фарватер.