• A
  • A
  • A
  • АБB
  • АБB
  • АБB
  • А
  • А
  • А
  • А
  • А
Обычная версия сайта

Глава

О задаче верификации для одного класса автоматов реального времени

Захаров В. А., Винарский Е. М.

Конечные автоматы Мили, представляющие собой простейшую математическую модель преобразования потоковых данных, широко используются во многих областях информатики. Но для некоторых приложений большое значение имеют не только значения обрабатываемых данных и порядок их следования, но также интервалы времени, которые отделяют события, присходящие по ходу вычисления автомата. Такие свойства уже не описывается явно средствами классической теории конечных автоматов; для моделирования течения времени автомат дополняется специальной вещественной переменной. Таким образом, воникает модель машин с конечным числом состояний, обрабатывающей потоки данных в реальном времени (TFSMs). Целью наших исследований является задача проверки выполнимости некоторых поведенческих свойств TFSMs, зависящих не только от соответствий между последовательностями входных сигналов и выходных сигналов, но также от времени их поступления и времени, затраченного на их обработку. Для формального описания  мы предлагаем использовать новое расширение LP-RLTL темпоральной логики линейного времени LTL. В основу LP-RLTL положены идеи, предложенные и развитые авторами ранее для решения задачи верификации последовательных реагирующих систем.