Сборники трудов ИСП РАН


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

Твардовский А.С. (ТГУ, Томск, Россия)
Евтушенко Н.В. (ИСП РАН, Москва, Россия; ВШЭ, Москва, Россия)

Аннотация

Конечно-автоматные методы широко используются при синтезе проверяющих тестов с гарантированной полнотой для дискретных систем. Поскольку поведение современных информационных и управляющих систем часто зависит от времени, классическая модель конечного автомата расширяется введением временных переменных. Более того, опциональность в спецификациях реальных систем побуждает к исследованиям в области синтеза тестов для недетерминированных автоматов. В настоящей работе мы адаптируем классические конечно автоматные методы синтеза тестов к недетерминированным автоматам с временными ограничениями и таймаутами (временным автоматам). Показывается, что в отличие от классических конечных автоматов, проверка отношений конформности между временными автоматами не может быть сведена к проверке соответствия между переходами, что нарушает основной принцип конечно автоматных методов синтеза тестов. Соответственно, предложенный подход и модель неисправности основаны на конечно автоматной абстракции автомата-спецификации, которая используется для описания поведения временного автомата. Область неисправности содержит временные автоматы с известной верхней границей числа состояний конечно автоматных абстракций и позволяет избежать явного перечисления множества тестируемых реализаций. Мы исследуем свойства конечно автоматных абстракций недетерминированных временных автоматов и показываем, что использование такой абстракции позволяет адаптировать классические методы к синтезу тестов с гарантированной полнотой для временных автоматов. Предложенный метод синтеза тестов позволяет строить полные проверяющие тесты для полностью определённых возможно недетерминированных автоматов с таймаутами и временными ограничениями для тестирования реализаций, поведение которых описывается детерминированными временными автоматами.

Ключевые слова

конечный автомат; таймаут; временные ограничения; недетерминированные временные автоматы; синтез тестов с гарантированной полнотой

Издание

Труды Института системного программирования РАН, том 31, вып. 4, 2019, стр. 175-188.

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

DOI: 10.15514/ISPRAS-2019-31(4)-12

Для цитирования

Твардовский А.С., Евтушенко Н.В. Синтез тестов с гарантированной полнотой для недетерминированных автоматов с таймаутами и временными ограничениями на основе конечно автоматных абстракций. Труды Института системного программирования РАН, том 31, вып. 4, 2019, стр. 175-188. DOI: 10.15514/ISPRAS-2019-31(4)-12.

Полный текст статьи в формате pdf (на английском) Вернуться к содержанию тома