Системная Информатика, № 17

Скачать

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

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

О некоторых свойствах временных машин с конечным числом состояний

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

Применение одного расширения CTL* для спецификации и верификации последовательных реагирующих систем

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

Рассуждения о программируемых логических контроллерах

Мы рассматриваем формальную проверку программного обеспечения управления критическими системами, то есть обеспечение отсутствия ошибок проектирования в системе по отношению к требованиям. Системы управления обычно основаны на промышленных контроллерах, также известных как программируемые логические контроллеры (ПЛК). Специфической особенностью ПЛК является цикл сканирования: 1) считываются входы, 2) изменяются состояния ПЛК и 3)...