|
ИСТИНА |
Войти в систему Регистрация |
ИСТИНА ИНХС РАН |
||
О задаче верификации для одного класса автоматов реального временстатья
- Авторы: Винарский Е.М., Захаров В.А.
- Сборник: Материалы XIII Международного семинара «Дискретная математика и ее приложения» имени академика О. Б. Лупанова (Москва, МГУ, 17–22 июня 2019 г.)
- Год издания: 2019
- Место издания: Изд-во механико-математического факультета МГУ
- Первая страница: 257
- Последняя страница: 260
- Аннотация: Конечные автоматы Мили, представляющие собой простейшую математическую модель преобразования потоковых данных, широко используются во многих областях информатики. Но для некоторых приложений большое значение имеют не только значения обрабатываемых данных и порядок их следования, но также интервалы времени, которые отделяют события, присходящие по ходу вычисления автомата. Такие свойства уже не описывается явно средствами классической теории конечных автоматов; для моделирования течения времени автомат дополняется специальной вещественной переменной. Таким образом, воникает модель машин с конечным числом состояний, обрабатывающей потоки данных в реальном времени (TFSMs). Изучение задач тестирования и минимизации для этой модели вычислений проводилось в последние годы во многих работах. Однако задача верификации для TFSMs еще ожидает исследования, и в данной статье мы предлагаем один подход к ее решению. Целью наших исследований является задача проверки выполнимости некоторых поведенческих свойств TFSMs, зависящих не только от соответствий между последовательностями входных сигналов и выходных сигналов, но также от времени их поступления и времени, затраченного на их обработку. Основным результатом исследований является Теорема. Существует алгоритм решения задачи верификации консервативных машин с конечным числом состояний, работающих в реальном времени, относительно спецификаций, представленных формулами Reg-LTL. Решение рассматриваемой задачи было получено нами при помощи табличного метода.
- Добавил в систему: Захаров Владимир Анатольевич