Метод формализации описания поведения систем управления в ходе проектирования программного обеспечения

Сложность проектирования современных систем управления (СУ) постоянно растет. Современный этап развития в области проектирования систем управления, в том числе программного обеспечения (ПО) СУ сложных аналитических комплексов, характеризуется тем, что ПО начинает вносить основной вклад в стоимость разработки. Процесс создания ПО СУ требует использования методов, позволяющих получить готовый результат, отвечающий ряду жестких требований.

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

Формализация спецификации является важным элементом подготовки проведения верификации ПО СУ. Форма представления требований, на которых будет строиться спецификация, должна обеспечивать возможность их автоматического анализа. В связи с этим в процессе определения требований необходимо использовать формальные методы описания. Однако в настоящее время переход к формальному описанию вызывает значительные затруднения у большинства разработчиков. Изложение функциональных требований к программному обеспечению, как правило, осуще- ствляется в повествовательной форме. Требования технического задания на разработку ПО СУ носят декларативный характер и могут рассматриваться как перечень решаемых задач, логика реализации которых должна быть изложена в дополнительных документах. Такая форма представления значительно затрудняет анализ требований [2]. Таким образом, на текущем этапе развития средств проектирования СУ задача формализации исходных данных является крайне актуальной.

ПОСТАНОВКА ЗАДАЧИ

В настоящей работе представлен метод формализации исходных данных с помощью формул темпоральной логики. Особенности применения метода проиллюстрированы на примере разработки ПО СУ для прибора "Гранат-4".

Прибор "Гранат-4" разрабатывался как автономный автоматизированный анализатор уровня активности холинэстераз плазмы и эритроцитов крови человека (каждая отдельно) для контроля безопасности условий работы персонала в условиях возможности воздействия антихолинэстеразных веществ. Принцип действия прибора состоит в фотометрическом измерении кинетических параметров ферментативных реакций, катализируемых холинэстеразами крови в растворах, приготовленных по методике проб, в течение времени, заданного программой прибора, с последующим расчетом характеристик, отнесенных к стандартным условиям, откорректированных на температуру в условиях измерения (температура контролируется встроенным датчиком).

Алгоритм работы прибора (т. е. его ПО) должен автоматически обеспечивать контроль исправности каждый раз при включении прибора, измерение характеристических параметров, расчет характеристических величин, отнесенных к стандартным условиям, занесение рассчитанных значений в память (для заданного количества проб) и автоматически исключать возможность неправильного заполнения и переполнения памяти. Под управлением с ручной 3-кнопочной клавиатуры прибор должен обеспечивать возможности выбора режима работы согласно типу пробы (плазма или кровь), изменения, при необходимости, номера пробы (автоматически должен быть предложен следующий, по нарастанию, свободный номер), выбор режима работы по вариантам: работа, просмотр, выключение. При установке режимов должна быть предусмотрена возможность сброса неправильных установок по выбору режима. Результаты измерений проб типа плазма—кровь для каждого пациента должны быть занесены в память (с одинаковыми номерами) таким образом, чтобы при их обработке (с использованием установленных в память калибровочных данных) получались значения характеристических параметров, отнесенных к стандартным условиям для конкретного пациента.

МЕТОД ФОРМАЛИЗАЦИИ

В предлагаемом методе основой описания логики работы ПО СУ является UML-формализм "прецедент" (use case). Прецедент описывает некоторый целостный фрагмент поведения системы не вдаваясь при этом в особенности внутренней структуры объекта. Набор прецедентов должен как можно более полно описывать поведение проектируемой системы управления. В предлагаемом подходе прецедент описывается с помощью условных начального и конечного состояний системы и условия перехода между ними. Следует отметить, что определение прецедентов производится вручную, все остальные шаги (включая описание структуры Крипке и темпоральных формул) выполняются автоматически в рамках средства проектирования СУ arKItect®, разрабатываемого в Международном институте передовых аэрокосмических технологий Санкт-Петербургского государственного университета аэрокосмического приборостроения.

В результате анализа требований к работе аналитического прибора "Гранат-4" были описаны следующие прецеденты, определяющие логику работы:

• 1.    Если прибор был выключен, то он переходит в режим проверки.

• 2.    Если проверка не была пройдена, прибор переходит в состояние "Неисправен".

• 3.    Если проверка прошла успешно, прибор переходит в основной режим работы.

• 4.    Из основного меню можно перейти в режимы:

  – просмотра результатов,

  – режим измерения параметра плазмы, – режим измерения параметра крови, – выключить прибор.

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

• 6.    Из режима измерения параметра прибор переходит в режим расчета параметра и далее в режим индикации результата.

• 7.    По окончании измерений прибор переходит в состояние выбора режима работы.

• 8.    В режимах измерения параметров проводится проверка возможности начать новое измерение, которая в случае отсутствия свободных ячеек памяти переводит прибор в режим просмотра результатов.

Описание представленных условий работы с помощью прецедентов определяет состояния системы и переходов между ними, далее этот набор автоматически объединяется и представляется в виде системы переходов ST (transition system). В ходе описания прецедентов работы прибора "Гранат-4" была построена система переходов со следующим набором состояний.

• S 0 :    Прибор выключен

• S 1 :    Проверка работоспособности

• S 2 :    Прибор неисправен

• S 3 :    Прибор в состоянии выбора режима работы

• S 4 :    Прибор в состоянии проверки результатов работы

• S 5 :    Просмотр результатов

• S 6 :    Проверка состояния памяти результатов вычисления параметра плазмы

• S 7 :    Измерение параметра плазмы

• S 8 :    Расчет параметра плазмы с учетом температуры воздуха

• S 9 :    Индикация рассчитанного параметра плазмы

• S 10 :    Проверка состояния памяти результатов вычисления параметра крови

• S 11 :    Измерение параметра крови

• S 12 :    Расчет параметра крови с учетом температуры воздуха

• S 13 :    Индикация рассчитанного параметра плазмы

Для дальнейшей формализации необходимо построить структуру Крипке, с помощью которой будут формализованы требования к СУ посредством формул темпоральной логики. Обычно [3] структура Крипке, соответствующая системе пе- реходов, строится путем отбрасывания действий на переходах. Это делается по той причине, что в некоторых случаях проверка требований к системе производится с игнорированием конкретных действий окружения, которые ведут к нарушению этих требований.

В рассматриваемом случае ставится задача максимально полного описания системы, и, таким образом, действия окружения следует ввести в структуру Крипке. Предлагается следующий подход к созданию структуры Крипке-M по имеющейся системе переходов ST.

• S 0 ^M = S 0 ^ST — множество начальных состояний структуры Крипке соответствует множеству начальных состояний системы переходов;

S ^M = S ^ST + R ^ST — множество состояний структуры Крипке строится следующим образом: для каждого состояния системы переходов S ^ST создается состояние структуры Крипке S ^M и для каждого перехода системы переходов R ^ST создается состояние структуры Крипке S ^M;

R M — множество переходов структуры Крипке строится в соответствии с созданными состояниями и системой переходов: для каждого R ^SP (соединяющего S ^SP 1 и S ^SP 2 ) создается переход в структуре Крипке, ведущий из S ^M 1 (созданный для S ^SP 1 ) в S ^M 2 (созданный для перехода R ^ST) и далее переход из S ^M 2 в S ^M 3 (созданный для S ^SP 2 );

AP — набор атомарных предикатов заполняется автоматически предикатами, соответствующими условиям переходов в ST (каждому уникальному переходу соответствует свой предикат, если условия повторяются, то и предикат повторяется), и атомарными предикатами, соответствующими состояниям системы (каждому состоянию соответствует свой атомарный предикат, эти наборы предикатов могут быть изменены позднее).

L ( S —> 2 ^AP) — функция пометок: т. к. каждому состоянию системы Крипке соответствует состояние или переход ST, а им соответствуют уникальные предикаты (по построению), то построение функции пометок очевидно.

При построении структуры Крипке были определены атомарные предикаты двух типов — описывающие состояния системы переходов и описывающие сами переходы. Для разграничения введем следующие обозначения:

@S — атомарный предикат (или набор, если структура Крипке была модифицирована пользователем), описывающий некое состояние системы;

q , p , ..., r — предикаты описывающие действия внешней среды (условия переходов в системе переходов); тогда основное требование, описанное в построенной структуре Крипке, — это причинноследственная связь событий — будет описана следующим образом:

G ( @S 1 ˄ p => XF ( @S 2 )) .

Если система находилась в состоянии @S 1 и возникло событие p , то в течение некоторого времени система должна перейти в состояние @S 2 . Эта запись соответствует описанию прецедента, где @S 1 и @S 2 определяют начальное и конечное состояния, а p — условие перехода между ними. Например: если прибор находится в режиме проверки ( @S 1 ) и проверка прошла успешно ( p ) то прибор переходит в состояние выбора режима работы ( @S 3 ).

По полученной структуре Крипке можно построить вычисления (трассы) перехода от одного состояния системы к другому и в дальнейшем проверить выполнимость этих трасс на реальных системах.

Построенная структура Крипке содержит формализованные проверки достижимости состояния @S :

F@S — когда-нибудь в будущем состояние @S будет достигнуто (при построении определенной трассы);

( @S 2 ) U ( @S 1 ˄@S 2 ) — состояние @S 1 будет достигнуто до достижения @S 2 (определяется по построенной трассе);

( @S 2 ˄@S 1 ) U@S 1 — состояние @S 2 не будет достигнуто раньше состояния @S 1 (определяется по построенной трассе).

Построенная система также специфицирует отсутствия события @S на определенных трассах:

G@S — состояние никогда не будет достигнуто;

F@S 1 => ( @S 2 ) U@S 1 — состояние @S 2 не наступит до состояния @S 1 ;

G ( @S 1 => G@S 2 ) — состояние @S 2 не наступит после события @S 1 .

Приведем список атомарных предикатов, выделенных для данной системы. Для упрощения схемы введем предикаты только для состояний сис- темы переходов:

q1: прибор выключен q2: прибор в состоянии проверки q3: прибор неисправен q4: прибор в состоянии выбора режима работы q5: прибор в состоянии проверки результатов q6: прибор в состоянии просмотра результатов q7: прибор в состоянии проверки памяти для значений параметра плазмы q8: прибор в состоянии измерения параметра плазмы q9: прибор в состоянии расчета параметра плазмы q10: прибор в состоянии индикации рассчитанного параметра плазмы q11: прибор в состоянии проверки памяти для значений параметра крови q12: прибор в состоянии измерения параметра крови q13: прибор в состоянии расчета параметра крови q14: прибор в состоянии индикации рассчитанного параметра крови

На рисунке представлена построенная струтура Крипке с указанием атомарных предикатов для состояний системы (атомарные предикаты, описывающие условия переходов, опущены для краткости записи). Полученная структура Крипке содержит требования к работе СУ, формализованные с помощью темпоральной логики. Запишем некоторые правила с помощью формул (полное перечисление всех темпоральных формул, описанных в данной структуре Крипке, неуместно:

этими формулами оперируют автоматические средства верификации, например Model Checking).

• 1.    G ( @S 1 ˄ q 3 => XF ( @S 2 )) — если прибор находился в состоянии проверки и оказался неработоспособен, то он переходит в состояние "неисправен".

• 2.    G ( @S 4 ˄ q 6 => XF ( @S 5 )) — если прибор находился в состоянии проверки результатов работы и проверка прошла успешно, то прибор переходит в состояние индикации рассчитанных параметров.

• 3.    G ( @S 2 => G@S 3 ) — если прибор находится в состоянии "неисправен", то он не сможет перейти в состояние "выбор режима работы".

• 4.    F@S 7 => ( @S 9 ) U@S 7 — состояние "просмотр результатов измерения параметра плазмы" не наступит, до того как будет выполнено "измерение параметра плазмы".

  

  Структура Крипке, описывающая режимы работы прибора "Гранат-4"

  
  

ВЫВОДЫ

В результате обработки комплекса исходных данных, описывающих поведение СУ, и представления их с помощью отдельных предикатов была получена спецификация — формализованное описание поведения СУ с помощью формул темпоральной логики и структуры Крипке. Такое описание может служить основой как для реализации ПО СУ, так и для анализа и исследования особенностей работы СУ с помощью методов Model Checking, формальных методов верификации или средств построения и контроля сценариев проверки. Для аналитического прибора "Гранат-4" было построено формальное описание логики работы ПО, позволившее упростить разработку и построить сценарии проверки, максимольно полно проверяющие возможные события в течение одной сессии работы с прибором.

Работа выполнена в Санкт-Петербургском государственном университете аэрокосмического приборостроения при поддержке Института аналитического приборостроения РАН (ИАП РАН)