Как было сказано в сериале "Теория большого взрыва": "Все становится лучше с Bluetooth". Повсеместно бытовые устройства приобретают дополнительный радио-модуль, что позволяет производителю обозначить их маркетинговым термином "smart" и объединять их в общую инфраструктуру, которая является одной из граней Интернета вещей. Но, любое "умное" устройство, кроме непосредственно электронной составляющей, отвечающей за основную функцию (нагревательный элемент в чайнике или утюге, двигатель в электрической зубной щетке и др.), содержит несколько важных программных компонентов, которые также надо тестировать и испытывать на безопасность, надежность и предсказуемость. В этом цикле статей мы поговорим о важных аспектах тестирования устройств интернета вещей, о темпоральной логике и конечных автоматах и о способах автоматизации проверки умных устройств.

Прежде всего, отличительной чертой тестирования умных устройств от разработки тестов программного обеспечения является тот факт, что устройство содержит в себе кроме прошивки еще и аппаратные компоненты (датчики, реле, исполняющие устройства, индикаторы и др.), которые не всегда сообщают о своем состоянии и узнать о фактическом состоянии индикатора с помощью инструментов автоматизации может быть затруднительным. Также датчики могут реагировать на изменения в окружающей среде (например, уровне освещенности, температуры и т.п.) и это сложно предусмотреть в синтетическом тесте. Еще один важный аспект тестирования (если, конечно, тест не имеет непосредственного доступа к вызову функций прошивки) состоит в том, что многие промышленные устройства предполагают управление через сеть (Bluetooth или через IP-сеть поверх Wi-Fi подключения) и нередко подключаются к облачному координатору, доступ к которому есть только у производителя. Это не представляется критичным при наличии ручных элементов управления (как, например, у кофе-машины или чайника) и мы сможем выполнить ручное тестирование (если опишем все возможные состояния и переходы между ними). Для автоматического тестирования мы будем рассматривать идеальный вариант, что мы и являемся производителем и либо знаем подробности протокола взаимодействия, либо можем встроить тесты непосредственно в прошивку.

Тесты устройства интернета вещей могут быть разделены на следующие типы:

• проверка удобства использования (usability testing) - устройство должно быть похожим на аналогичное устройство без "умных" функций и элементы управления должны быть расположены удобно и логично. Это легко достижимо для простых устройств (таких как зубная щетка или чайник), но гораздо менее очевидно для микроволновых печей, тостеров и кофе-машин, которые поддерживают большое количество режимов. Существуют компании (например, TestBirds), которые выполняют тестирование умных устройств с помощью ручных тестировщиков со всего мира. Также было проведено множество исследований по юзабитили-тестам для оборудования (особенно для носимых устройств), обобщения можно посмотреть в документах здесь или здесь.

• функциональное тестирование (functional testing): выполнение устройством заявленных функций, корректность переходов между состояниями, достижимость всех состояний (невозможность попасть в состояние или в цикл состояний, из которого нельзя выйти в основную функциональность), проверка работы устройства при выходе из строя сенсоров, подсистемы (например, радиомодуля), проверка функционирования устройства в автономном режиме (при потере подключения к сети Интернет) с локальным сохранением данных (в случае, если устройство накапливает данные, например является прибором медицинского назначения).

• проверка безопасности (security testing): шифрование данных телеметрии и управляющих команд (для исключения перехвата данных или управления устройством неавторизованным пользователем, который оказался в зоне досягаемости используемой технологии радиочастотного доступа). Устройства, которые используют Bluetooth/Wi-Fi подключение используют транспортное шифрование самой технологии, но при этом остаются в зоне риска из-за уязвимостей процесса согласования соединения и возможности атаки Man-in-the-Middle для Bluetooth, а также возможности создания поддельной точки доступа для Wi-Fi (в этом случае есть вероятность соединения с точкой доступа, которая будет находиться ближе и ответит раньше). Более подробно про векторы атак на Bluetooth можно почитать здесь, также представляет интерес атака L2Fuzz, о которой написано в этой публикации. Кроме того надо отметить, что многие устройства интернета вещей вообще не используют шифрование передаваемых данных, что открывает много возможностей для перехвата данных или удаленного исполнения команд. Также многие устройства имеют административный интерфейс, для доступа к которому либо используется простой пароль по умолчанию (который пользователи не изменяют, поскольку это нигде явно не акцентировано), либо какой-либо служебный пароль (для тестов и обслуживания на производстве или в сервисном центре). Наиболее актульный список известных атак можно посмотреть здесь, а отчет о безопасности устройств интернета вещей можно получить с сайта OneKey по этой ссылке.

• тестирование совместимости (compatibility testing) - проверка работы устройства с сетевыми устройствами разных производителей, которые поддерживают необходимые версии протоколов и профили доступа (для bluetooth). На этом этапе выявляются потенциальные проблемы с подключением устройств к хабам определенных поставщиков (актуально как для Bluetooth/Wi-Fi, так и для других протоколов передачи данных, таких как ZigBee, NFC, LoRaWan). Про возможные проблемы на этом этапе можно почитать здесь.

• тестирование на соответствие (compliance testing) - здесь проверяется корректная работа радиомодуля (использование полосы частот, совместная работа с другими устройствами в общих полосах, соблюдение протокола установки соединения и передачи данных), а также соответствие устройства требованиям, предъявляемым к такому типу устройств (как к бытовой технике, так и к медицинским приборам). Про стандарты IoT compliance можно найти информации в IEEE 2413-2019.

• тестирование обновления (update testing) - любое смарт-устройство предполагает наличие механизма обновления программного обеспечения, чаще всего "по воздуху", поскольку обычно для устройства не предоставляется специального типа подключения (например, по USB) для установки обновлений. Чаще всего для сервисных целей на устройстве доступен интерфейс Test Access Port (IEEE Std. 1149.1), который представлен коннектором JTAG для обновления микрокода и низкоуровневого тестирования функционирования управляющей электроники. Более подробно про это можно почитать здесь.

В первой части статьи мы обсудим прежде всего функциональное ручное тестирование и методы описания и формальной верификации переходов между состояниями устройства.

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

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

Для создания графического представления диаграммы состояний мы будем использовать Graphviz и консольный инструмент dot. Входными данными для dot является текстовый файл с описанием узлов и ребер графа, файл может быть создан как вручную, так и использованием языков программирования (например, Python).

Для примера возьмем обыкновенную (не умную) лампу. На первый взгляд кажется, что у нее всего два состояния - выключена и включена. Обозначим их OFF и ON соответственно и подготовим файл описания диаграммы:

digraph "Lamp" {
  ON [label="Включена"]
  OFF [label="Выключена"]
  OFF -> ON [label="Включаем"]
  ON -> OFF [label="Выключаем"]
}

Сгенерируем графическое представление диаграммы:

dot lamp1.dot -Nshape=box -Nstyle=rounded -Nfontsize=18 -Tpng -o lamp1.png

В действительности лампа может быть еще и сломана (например, в процессе тестирования можно применить необратимые повреждения) и это состояние будет терминальным (из него нельзя будет вернуться ни в одно из других состояний). Расширим нашу диаграмму:

digraph "Lamp" {
  ON [label="Включена"]
  OFF [label="Выключена"]
  BROKEN [label="Сломана"]
  OFF -> ON [label="Включаем"]
  ON -> OFF [label="Выключаем"]
  OFF -> BROKEN [label="Сломали"]
  ON -> BROKEN [label="Сломали"]
}

Перейдем теперь к умным лампам. В отличии от обычных ламп у них есть еще ненастроенное состояние, когда лампа еще не подключена к Bluetooth/Wi-Fi и не готова принимать управляющие команды. В этом состоянии лампа обычно мигает (пульсирует) и в него можно вернуться (во многих случаях методом "три раза выключить-включить"). Кроме того, при включении уже настроенной лампы они загорается, независимо от команд управляющего оборудования (но затем может быть программно выключена). Также умные лампы нередко могут изменять параметры свечения (яркость и иногда цвет) и это уже происходит по сообщению от программного обеспечения через радиоканал. Все переходы на диаграмме теперь можно условно разделить на несколько групп:

• переходы по внешнему воздействию (например, подача электроэнергии на устройство)

• переходы по информации от датчиков (например, нажатие на сенсорную кнопку, достижения порогового значения по датчику температуры, срабатывание таймера и др.)

• переходы по управляющим командам (поступающим через радиоканал от программного обеспечения, хаба умного дома или управляющего ассистента Google Home, Alexa, Siri, Алиса и др.). С точки зрения описания поведения системы такие команды тоже создают внутренние причины для перехода, но мы их будем обозначать с фигурных скобках, чтобы потом вернуться к ним при рассмотрении аспектов автоматизации.

Также здесь на диаграмме впервые появятся условные переходы (например, при включении можно перейти или в состояние ожидания инициализации или в состояние "включено" с последними настройками, условие будем указывать в квадратных скобках после триггера (причины перехода). Файл описания диаграммы станет значительно больше (поскольку есть несколько разных состояний "выключено" - выключено аппаратно (выключателем или из розетки) и выключено программно:

digraph "Lamp" {
  WAITING [label="Ожидает настройки"]
  LIGHTS_ON [label="Светит"]
  OFF [label="Выключена"]
  LIGHTS_OFF [label="Не светит"]
  BROKEN [label="Сломана"]
  LIGHTS_TUNED [label="Изменены параметры"]

  OFF -> LIGHTS_ON [label="Включаем [inited=true]"]
  OFF -> WAITING [label="Включаем [inited=false]"]
  WAITING -> LIGHTS_ON [label="Настроили"]
  LIGHTS_ON -> WAITING [label="Сброс"]
  LIGHTS_ON -> OFF [label="Выключаем"]
  WAITING -> OFF [label="Выключаем"]
  OFF -> BROKEN [label="Сломали"]
  LIGHTS_ON -> BROKEN [label="Сломали"]
  LIGHTS_OFF -> BROKEN [label="Сломали"]
  WAITING -> BROKEN [label="Сломали"]
  LIGHTS_ON -> LIGHTS_TUNED [label="Программа"]
  LIGHTS_TUNED -> LIGHTS_OFF [label="Программа"]
  LIGHTS_ON -> LIGHTS_OFF [label="Программа"]
  LIGHTS_OFF -> LIGHTS_ON [label="Программа"]
}

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

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

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

Вторая часть таблицы будет для ненастроенной лампы (обратите внимание, что здесь есть конфликтующее поведение исходного состояния+триггер в сравнении с предыдущей таблицей):

Здесь есть небольшая неточность, поскольку из таблицы можно предположить, что сломанную лампу можно перевести в режим ожидания настройки через сброс. Заменим последнюю строку:

Теперь напишем таблицу переходов для настроенной лампы:

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

Альтернативным способом представления переходов являются матрицы смежности. Для создания матрицы разместим все возможные состояния и в строках и в столбцах таблицы и на пересечении напишем необходимые для перехода действия. Тут важно, что для переходов важно направление, поэтому для определенности будем считать строки исходным состояние, а столбцы - целевым. Рассмотрим на примере первой таблицы.

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

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

Темпоральная логика является развитием модальной логики и описывает логические отношения с учетом их последовательности по временной шкале. В темпоральной логике кроме обычных логических операторов, используются еще и модальные операторы, сообщающие о выполнении логического условия (например, достижения определенного состояния) в будущем времени. Например, модальный оператор N (обозначается ) сообщает о том, что в следующем состоянии высказывание будет истинным, оператор F что в каком-нибудь состоянии высказывание будет истинным (т.е. где-то данное состояние будет достижимо), G будет истинным, если во всех будущих состояниях высказывание будет истинным (например, после того как мы сломали лампу, она будет сломана всегда). Также есть два оператора проверки переходов: A будет истинным, если на всех ветвях переходов из текущего состояния условие будет выполняться (например, из состояния "выключено" всегда можно дойти до состояния "светит", даже если лампа еще не была настроена). Второй оператор существования E проверяет, что хотя бы на одной из ветвей будет выполняться условие (например, есть ветви в которых возможно перейти в состояние "Опасность"). Обычно A и E используются совместно с N, F, G. С помощью оператора EF мы и можем выявить зацикливание состояний, что находясь в состоянии "опасность" нельзя перейти в состояние "выключена" никакими действиями. Как это можно проверить?

Для этого воспользуемся семантикой Крипке, общими правилами для модальной логики и идеями CTL (Computational Tree Logic). CTL описывается бесконечное дерево всех возможных переходов (например, в нем может быть ветвь "выключена"-"светит"-"выключена"-"светит" и так до бесконечности). Дерево начинается с начального состояния (от которого мы начинаем анализ) и тогда операторы приобретают смысл анализа потомков корня на соответствие условию (N - в ближайшем потомке условие должно выполняться, F - в одном из потомков где-то условие должно выполняться, G - во всех потомках условие будет выполнено). Для описания состояний мы будем использовать модель Крипке (семантику миров Крипке), где каждый конкретный момент времени представлен комбинацией , где S - множество возможных состояний, R - отношение переходов (матрица смежности). Между состояниями определяется путь при этом из каждого состояния существуют свое подмножество путей . Например, из состояния выключено есть варианты путей "светит" (и далее все возможные варианты и комбинации) и "сломана" (только один путь, поскольку переход из него возможен только в это же состояние). Поскольку в нашем случае система может находиться только в одном состоянии, существует ровно N миров (где N - количество состояний), а отношение достижимости является нашей матрицей смежности. Для проверки достижимости необходимо выписать все состояния (при этом при переходе в следующее состояния в список добавляются все достижимые из него состояния), при этом для исключения повторов можно маркировать пройденные состояния и исключать их из дальнейшего рассмотрения.

Определим номера для наших состояний S:

• 1 - выключена

• 2 - светит

• 3 - сломана

• 4 - опасность

• 5 - тревога

Составим список достижимых миров для каждого состояния:

• 1 : 23, затем из 2 - 4, затем из 4 - 5, все состояния достижимы (2345)

• 2: аналогично, все состояния достижимы (1345)

• 3: переходов нет, ни одно состояние недостижимо

• 4: достижимо только состояние 5

• 5: достижимо только состояние 4

Также, можно проверить, что из любого состояния можно перейти в состояние 2 в любой последовательности. Возможные варианты будущего для исходного состояния 1 (выключена): 212, 23, 3, 245, 24545, .... Как можно видеть, в возможных путях переходов между мирами (состояниями), есть варианты, где состояния 2 или 3 не будет представлено (т.е. устройство нельзя выключить или сломать).

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

После установки создадим новую модель (Model -> New -> PRISM Model), перейдем во вкладку Model и введем следующий текст:

mdp

module M1
  x : [1..5] init 1;

  [] x=1 -> 0.5:(x'=2)+0.5:(x'=3);
  [] x=2 -> 0.333:(x'=1)+0.333:(x'=4)+0.334:(x'=3);
  [] x=3 -> (x'=3);
  [] x=4 -> (x'=5);
  [] x=5 -> (x'=4);
endmodule

mdp определяется алгоритм для определения вероятности состояний (в нашем случае - это вероятностный Марковский процесс принятия решений), модуль создает независимый процесс (модули могут выполняться параллельно и даже конкурировать за ресурсы). Внутри модуля мы определяем переменную состояния (также могут использоваться константы с оператором const), и вероятности перехода в другие состояния (мы можем использовать равные вероятности перехода в любое из целевых состояний, но в действительно можно установить разные вероятности, например для оценки риска повреждения лампы при известной вероятности события из состояния включено (например, когда лампа "перегорает") и выключена (вероятность случайного повреждения). Мы только анализируем достижимость состояний, поэтому вариант с равными вероятностями здесь возможен. Обратите внимание, что сумма всех вероятностей должна быть строго равна 1 (например, в строке 7 для этого скорректировали последнюю вероятность).

Запустим симуляцию (Simulator -> New Path) и укажем 10 шагов симуляции.

Здесь мы увидим, что после нескольких итераций мы попадаем в deadlock в состоянии 3.

Изменим вероятность перехода в состояние 3:

mdp

module M1
  x : [1..5] init 1;

  [] x=1 -> 0.998:(x'=2)+0.002:(x'=3);
  [] x=2 -> 0.499:(x'=1)+0.499:(x'=4)+0.002:(x'=3);
  [] x=3 -> (x'=3);
  [] x=4 -> (x'=5);
  [] x=5 -> (x'=4);
endmodule

Перезапустим симуляцию (New path) и обнаружим цикл между состояниями 4 и 5.

Добавим обратный переход в состояние выключено из 4 и 5, чтобы избежать зацикливания. Можно выполнять переход "шаг за шагом", если установить значение Steps в 1 (в этом случае в Manual Exploration будут показаны вероятности переходов в другие состояния на каждом шаге), также можно переопределить для симуляции стартовое состояние (Simulator -> New path from state).

Если мы хотим узнать вероятность нахождения в определенном состоянии, нужно переключить модель на DTMC / CTMC (также запишем в квадратных скобках возможные причины переходов) и исключим ситуации зацикливания (из состояния 3 "Сломана" можно вернуться в состояние 1 "Выключено" через действие "repair"):

dtmc

module M1
  x : [1..5] init 1;

  [turnon] x=1 -> (x'=2);
  [turnoff] x=2 -> (x'=1);
  [broke] x=2 -> (x'=3);
  [broke] x=1 -> (x'=3);
  [alarm] x=2 -> (x'=4);
  [alarm] x=5 -> (x'=4);
  [caution] x=4 -> (x'=5);
  [broke] x=4 -> (x'=3);
  [broke] x=5 -> (x'=3);
  [repair] x=3 -> (x'=1);

endmodule

Мы также можем запустить симуляцию (и посмотреть на последовательность или возможный график изменения состояния со временем), но также нам доступна статистика обнаружить систему в определенном состоянии Model -> Compute -> Steady-state probabilities - вероятность обнаружить систему в указанном состоянии. Для определения вероятности достижения состояния нужно исключить начальное состояние из списка разрешенных для перехода (например, создать состояние 0 и единственный переход 0-1): Результатом будет отчет с оценкой вероятности обнаружить систему в том или ином состоянии, например такой:

Printing steady-state probabilities in plain text format below:
1:(1)=0.3750000339612575
2:(2)=0.18749997669780036
3:(3)=0.3124999830193713
4:(4)=0.08333335347474564
5:(5)=0.04166665284682529

Здесь важным для тестирования является критерий слишком большого значения вероятности, что свидетельствует о том, что высока вероятность (количество маршрутов) по которым можно попасть в это состояние, но мало количество возможностей покинуть его (например, при наличии возможности сохранения текущего состояния через определение перехода из него в это же состояние). Для управления вероятностными процессами здесь также можно использовать синтаксис, который был задействован для mdp):

dtmc

module M1
  x : [0..5] init 0;

  [initialize] x=0 -> (x'=1);
  [turnon] x=1 -> 0.998:(x'=2)+0.002:(x'=3);
  [turnoff] x=2 -> 0.499:(x'=1)+0.499:(x'=4)+0.002:(x'=3);
  [alarm] x=5 -> 0.499:(x'=4)+0.499:(x'=2)+0.002:(x'=3);
  [caution] x=4 -> 0.998:(x'=5)+0.002:(x'=3);
  [repair] x=3 -> 0.5:(x'=3)+0.5:(x'=1);

endmodule

Например, здесь мы имеем 50% вероятность успеха починки. После этого статистика по состояниям будет другой:

Printing steady-state probabilities in plain text format below:
1:(1)=0.1443187052655503
2:(2)=0.2852235994839987
3:(3)=0.003984063745019921
4:(4)=0.2835202742447253
5:(5)=0.28295335726070586

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

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

А сейчас хочу пригласить всех желающих на бесплатный урок по теме: "Тестирование API с Postman для начинающих", который пройдет уже 24 августа.

• Записаться на бесплатный урок