представление о времени существенно для спецификации систем,
критичных ко времени. В соответствии с общепринятым
определением, системы, критичные ко времени – это такие системы,
в которых корректность зависит не только от логического результата
вычисления, но также и от времени, за которое результаты получены.
Системы, критичные ко времени, должны удовлетворять не только
требованиям функциональной корректности, но и требованиям
своевременности. Такие системы обычно характеризуются
количественными временными свойствами, относящимися к
наступлению событий.
Пример системы, критичной ко времени, – это железнодорожный
переезд: если обнаружено приближение поезда, переезд должен быть
закрыт в течение определенного времени с целью блокировки
автомобильного и пешеходного трафика перед тем, как поезд
достигнет переезда. Коммуникационные протоколы – другой пример
системы, критичной ко времени: после передачи данных повторная
передача должна быть запущена, если подтверждение не получено в
течение определенного времени. Третий пример системы, критичной
ко времени – это аппарат лучевой терапии, благодаря которому
пациенты получают высокую дозу радиации в течение ограниченного
периода времени. Даже небольшое превышение этого периода опасно
и может привести к смерти пациента.
Количественная временная информация существенна не только для
систем, критичных ко времени, но также является необходимой
составной частью в задачах анализа и спецификации аспектов
производительности систем. Типичное предложение, относящееся к
производительности, такое, как «выполнение задания происходит в
течение 30 секунд», может быть сформулировано, только если
имеется возможность измерять прошедшее время.
Количественное задание времени в темпоральной логике
В этом разделе рассматривается расширение ветвящейся
темпоральной логики количественными представлениями о времени.
Выше было показано, что линейная и ветвящаяся темпоральная
логика интерпретируются в терминах моделей, где главную роль
играет понятие состояния. Наиболее важное изменение при переходе
к количественным временным характеристикам является возможность
измерять время. Можно спросить, каким образом понятие времени
включается в модель, базирующуюся на состояниях, и каковы
взаимоотношения между состояниями и временем. При включении
временных характеристик в модель должны быть рассмотрены
несколько аспектов: