Что такое формальная верификация

SDC протокол и автоматизированное тестирование

Рассмотрим типичные требования, предъявляемые к устройствам, общающимся по SDC протоколу, и способы их верификации при использовании автоматизированного тестирования.

Требования по тестированию статических данных MDIB:

• All HANDLEs SHALL be unique within one MDIB sequence of a SERVICE PROVIDER
• A HANDLE SHALL consist of characters that match only valid Unicode codes greater than U+0020, except for U+FFFD (replacement character)

Для проверки этих требований можно использовать простые алгоритмы. Например, для уникальности HANDLE можно собрать все HANDLE в объект List, преобразовать их в Set и проверить наличие дублирующихся объектов.

Дополнительные требования:

• A SERVICE PROVIDER SHOULD describe all offered remote invocation capabilities using the pm:ScoDescriptor structure in pm:MdsDescriptor/pm:Sco

Это требование означает, что все операции должны быть описаны в структуре ScoDescriptor.

Таким образом, автоматизированное тестирование технических характеристик устройства, работающего по SDC протоколу, можно провести с помощью программной симуляции поведения устройства. Важно учитывать как статические, так и динамические требования для полного тестирования продукта.

## Работа с сервисными сообщениями

В предыдущих примерах мы работали с объектом MDIB, хранящим дескрипторы и стейты из xml файла MDIB. Теперь нам нужно работать с сервисными сообщениями, обновляющими информацию. Для этого используем ObservableProperties из библиотеки sdc11.

С помощью ObservableProperties мы можем выполнять действия при получении определенного типа сообщений. Например, можем просто сохранить сообщение в список при получении необходимого типа.

### Проверка требований

Требование гласит, что каждая присутствующая тревога (физиологическая или техническая) должна быть отражена в списке присутствующих тревог.

Обычно списки PresentPhysiologicalAlarmConditions и PresentTechnicalAlarmConditions представлены только в одной AlertSystem, например, в AlertSystem, являющемся дочерним элементом MDS.

### Проверка других требований

* AlertConditionDescriptor/Priority обновляется только если AlertConditionState/Presence = false и все связанные AlertSignalState/Presence Off или Ack.

Для проверки этого требования используем сообщения msg:DescriptorModificationReport, который хранит изменения в атрибутах дескриптора объекта.

Создадем алгоритм проверки на основе DescriptorModificationReport.

### Практика

Существуют сценарии, где используются SAT-солверы (задача выполнимости булевых формул).

## Тестирование и аудит

Тестирование программного кода — это наука со множеством подходов и практик. Современные языки программирования поддерживают автоматизированные тесты и модульные и интеграционные тесты.

Дейкстра писал: “Тестирование программ может быть эффективным средством нахождения ошибок, но не доказывает их отсутствие”.

Формальная верификация дает возможность доказать отсутствие определенных ошибок в коде.

Аудит также не дает стопроцентной гарантии отсутствия ошибок в коде.

Дополнительные сведения в протоколе испытаний

Помимо обязательных, в протокол испытаний часто включают дополнительные сведения. Их перечень зависит от характеристики и специфики конкретного товара. Обычно она включает:

• Техническое описание устройства или продукции
• Сведения о процедуре тестирования
• Результаты измерений и испытаний
• Объяснения конструкции устройства
• Информацию о безопасности продукции

Акт отбора образцов

В дополнение к протоколу испытаний оформляется акт отбора образцов. В нем указываются следующие сведения:

• Количество отобранных образцов
• Место и дата отбора образцов
• Способы отбора образцов
• Этикетирование образцов

Библиотека sdc11073

Так как SDC протокол — это открытый стандарт взаимодействия медицинских устройств, существуют пакеты для работы с ним на разных языках программирования. Мы в целях автоматизированного тестирования используем пакет, находящийся в открытом доступе на github и написанный на языке программирования Python. Подробно на его реализации и работе останавливаться не будем, но рассмотрим основные моменты, которые нам могут пригодиться в дальнейших примерах.

Итак, пакет sdc11 073 — это полноценная реализация SDC протокола, написанная на Python. Он позволяет вам создать как SDC устройство, которое будет являться провайдером данных, так и SDC клиент, являющийся потребителем данных.

Также эта реализация создает объектно‑ориентированную модель MDIB на основе получаемого xml файла, что очень сильно упрощает обработку и тестирование данных MDIB. Так создается объект класс MDIB, который включает в себя дескрипторы и стейты для каждого элемента в текущем MDIB с использованием типов данных, описанных в BICEPS.

Протокол испытаний

Протокол испытаний должен включать в себя:

1. Цель проведения испытаний
2. Описание методики испытаний
3. Состав испытуемых образцов
4. Результаты испытаний и их анализ
5. Выводы по проведенным испытаниям

После оформления протокол испытаний подписывается непосредственно испытателем лаборатории, проводившим испытания.

Пример испытаний на примере трубопроводной арматуры

Наглядно, на примере трубопроводной арматуры (продукция – кран шаровой) показан порядок проведения испытаний, который включает в себя проведение проверок и определение показателей безопасности, в соответствии с предъявляемыми к данной продукции требованиями.

Требования к испытаниям

Изначально нужно опираться на выбранную схему сертификации или декларирования. В одних случаях испытания требуется проводить только в аккредитованной лаборатории, которая подтвердила свой статус в системе ФГИС Росаккредитации, в других же допускается привлекать сторонние неаккредитованные центры.

Нормативные документы в области испытаний

В отношении различных групп продукции на территории ЕАЭС разработаны и действуют нормативные документы, в частности ГОСТы (как национальные, так и межгосударственные), которые содержат требования к проведению, как самим конкретным видам продукции, так и методам испытаний.

Основные стандарты, относящиеся к области испытаний продукции:

• ГОСТ 16504-81 Система государственных испытаний продукции. Испытания и контроль качества продукции. Основные термины и определения (актуализирован в 2021 г.)

Формальная верификация

Теперь о формальной верификации. Положим, наша задача подвергнуть формальной верификации некий программный код. Опишем один из возможных способов (сценариев) работы.

Шаги формальной верификации:

1. Перевести код на язык интерактивного программного средства доказательства теорем, например, Coq или Isabelle.

2. Написать и доказать Леммы (Теоремы) для каждой функции.

3. Леммы должны отражать суть функции, описывать ее поведение и доказывать корректность работы для всех возможных входных параметров.

4. В случае невозможности доказать что-то, это может указывать на баг, ошибку или уязвимость, которые нужно сообщить программистам.

Примеры технологий для формальной верификации:

• Coq
• Isabelle

Ссылки на автоматические переводчики кода на язык пруверов можно найти в вышеуказанной статье.