В проверке моделей , подполе информатики , часы - это математический объект, используемый для моделирования времени. Точнее, часы измеряют, сколько времени прошло с тех пор, как произошло определенное событие, в этом смысле часы - это более точно абстракция секундомера . В модели некоторой конкретной программы значение часов может быть либо временем, прошедшим с момента запуска программы, либо временем, прошедшим с того момента, как в программе произошло определенное событие. Эти часы используются в определении синхронизированного автомата , сигнального автомата , временной пропозициональной временной логики и временной логики часов . Они также используются в таких программах, как UPPAAL.которые реализуют синхронизированные автоматы. [1]
Как правило, в модели системы используется много часов. Эти несколько часов необходимы для отслеживания ограниченного количества событий. Все эти часы синхронизированы. Это означает, что разница в значениях между двумя фиксированными часами остается постоянной, пока один из них не будет перезапущен. На языке электроники это означает, что джиттер часов равен нулю.
Пример
Допустим, мы хотим смоделировать лифт в десятиэтажном здании. Наша модель может иметь часы , так что значение часов это время, когда кто-то ждал лифта на этаже . Эти часы запускаются, когда кто-то вызывает лифт на этаже(и лифт на этом этаже еще не вызывали с момента последнего посещения этого этажа). Эти часы можно выключить, когда лифт поднимается на этаж.. В этом примере нам действительно нужно десять разных часов, потому что нам нужно отслеживать десять независимых событий. Еще часы может использоваться для проверки того, сколько времени лифт провел на определенном этаже.
Затем модель этого лифта может использовать эти часы, чтобы проверить, удовлетворяет ли программа лифта таким свойствам, как «если предположить, что лифт не удерживается на этаже более пятнадцати секунд, тогда никто не должен ждать лифт более трех минут. ". Чтобы проверить, выполняется ли это утверждение, достаточно проверить, что при каждом запуске модели, в которой часы всегда меньше пятнадцати секунд, каждые часы выключается до того, как дойдет до трех минут.
Определение
Формально набор часов - это просто конечный набор [1] : 191 . Каждый элемент набора часов называется часами. Интуитивно часы похожи на переменную в логике первого порядка , это элемент, который можно использовать в логической формуле и который может принимать несколько разных значений.
Оценка часов
Оценка часов или интерпретация часов [1] : 193 над обычно определяется как функция от к множеству неотрицательных вещественных. Точно так же оценка может рассматриваться как точка в.
Первоначальное задание - это постоянная функция, отправляющая каждые часы в 0. Интуитивно она представляет начальное время программы, когда все часы инициализируются одновременно.
Учитывая назначение часов , и настоящий , обозначает назначение часов, отправляющих каждые часы к . Интуитивно он представляет собой оценку после которого единицы времени прошли.
Учитывая подмножество часов, обозначает присвоение, подобное в котором часы сброшены. Формально, отправляет каждые часы до 0 и каждые часы к .
Неактивные часы
Программа UPPAAL вводит понятие неактивных часов . [2] Часы неактивны в какое-то время, если нет возможности в будущем, в которой значение часов проверяется без предварительного сброса. В нашем примере выше часы считается неактивным, когда лифт поднимается на этаж , и остается неактивным, пока кто-нибудь не вызовет лифт на этаже .
При разрешении неактивных часов оценка может связывать часы с особой ценностью чтобы указать, что он неактивен. Если тогда также равно .
Ограничение часов
Атомные часы ограничение просто член вида, где это часы, является оператором сравнения, например <, ≤, = ≥ или>, и - интегральная постоянная. В нашем предыдущем примере мы можем использовать ограничения атомных часов заявить, что человек на этаже ждал меньше трех минут и заявить, что лифт простоял на каком-то этаже более пятнадцати секунд. Оценка удовлетворяет оценке атомных часов если и только если .
Часы ограничение либо конечное соединение атомных часов ограничения или константа «истина» (который можно рассматривать как пустые вместе). Оценка удовлетворяет ограничение по времени если он удовлетворяет каждому ограничению атомных часов .
Диагональное ограничение
В зависимости от контекста ограничение атомных часов также может иметь вид . Такое ограничение называется диагональным, поскольку определяет диагональную линию в .
Разрешение диагональных ограничений может позволить уменьшить размер формулы или автомата, используемого для описания системы. Однако сложность алгоритма может возрасти, если разрешены диагональные ограничения. В большинстве систем, использующих часы, разрешение диагонального ограничения не увеличивает выразительность логики. Теперь мы объясним, как кодировать такое ограничение с помощью логической переменной и недиагонального ограничения.
Диагональное ограничение можно смоделировать с использованием недиагонального ограничения следующим образом. Когда сброшен, проверьте, есть ли держит или нет. Напомним эту информацию в логической переменной и заменить по этой переменной. Когда сброшен, установлен к истине, если <или ≤ или если is = и .
Способ кодирования логической переменной зависит от системы, которая использует часы. Например, UPPAAL напрямую поддерживает логические переменные. Временные автоматы и сигнальные автоматы могут кодировать логическое значение в своих местоположениях. Во временной логике часов по синхронизированным словам, логическая переменная может быть закодирована с использованием новых часов., значение которого равно 0 тогда и только тогда, когда ложно. Это, сбрасывается, пока предполагается ложным. В временной пропозициональной временной логике формула, который перезапускается а затем оценивает , можно заменить формулой , где а также копии формул , где заменяются константами true и false соответственно.
Наборы, определяемые ограничениями часов
Ограничение часов определяет набор оценок. В литературе рассматриваются два вида таких наборов.
Зона представляет собой непустое множество оценок , удовлетворяющие тактовое ограничение. Ограничения по зонам и часам реализуются с помощью матрицы границ разностей .
Учитывая модель , он использует конечное число констант в своих ограничениях времени. Позволятьбыть самой большой используемой постоянной. Область является непустой зоной , в которой нет ограничений больше используются, причем такие, что он минимален для включения.
Смотрите также
Заметки
- ^ a b c Алур, Раджив; Дилл, Дэвид Л. (25 апреля 1994 г.). «Теория временных автоматов» (PDF) . Теоретическая информатика . 126 (2): 183–235. DOI : 10.1016 / 0304-3975 (94) 90010-8 .
- ^ Берманн, Герд; Давид, Александр; Ларсен, Ким Джи (28 ноября 2006 г.). «Учебник по Uppaal 4.0» (PDF) : 28. Цитировать журнал требует
|journal=
( помощь )