Reloj (comprobación del modelo)
En la comprobación de modelos , un subcampo de la informática , un reloj es un objeto matemático que se utiliza para modelar el tiempo. Más precisamente, un reloj mide cuánto tiempo pasó desde que ocurrió un evento en particular, en este sentido, un reloj es más precisamente una abstracción de un cronómetro . En un modelo de algún programa en particular, el valor del reloj puede ser el tiempo desde que se inició el programa o el tiempo desde que ocurrió un evento particular en el programa. Esos relojes se utilizan en la definición de autómata cronometrado, autómata de señales , lógica temporal proposicional cronometrada y lógica temporal de reloj . También se utilizan en programas como UPPAALque implementan autómatas cronometrados. [1]
Generalmente, el modelo de un sistema utiliza muchos relojes. Esos relojes múltiples son necesarios para rastrear un número limitado de eventos. Todos esos relojes están sincronizados. Eso significa que la diferencia de valor entre dos relojes fijos es constante hasta que uno de ellos se reinicia. En el lenguaje de la electrónica, significa que el jitter del reloj es nulo.
Supongamos que queremos modelizar un ascensor en un edificio de diez plantas. Nuestro modelo puede tener relojes , de modo que el valor del reloj sea el tiempo que alguien tuvo que esperar el ascensor en el piso . Este reloj se pone en marcha cuando alguien llama al ascensor en el piso (y el ascensor no ha sido llamado a este piso desde la última vez que visitó ese piso). Este reloj se puede apagar cuando el ascensor llega al piso . En este ejemplo, en realidad necesitamos diez relojes distintos porque necesitamos rastrear diez eventos independientes. Se puede usar otro reloj para verificar cuánto tiempo pasó un ascensor en un piso en particular.
Un modelo de este ascensor puede usar esos relojes para afirmar si el programa del ascensor satisface propiedades tales como "suponiendo que el ascensor no se mantiene en un piso durante más de quince segundos, entonces nadie tiene que esperar el ascensor durante más de tres minutos". ". Para comprobar si esta afirmación se cumple, basta comprobar que, en cada ejecución del modelo en el que el reloj es siempre inferior a quince segundos, cada reloj se apaga antes de llegar a los tres minutos.
Formalmente, un conjunto de relojes es simplemente un conjunto finito [1] : 191 . Cada elemento de un conjunto de reloj se llama reloj. Intuitivamente, un reloj es similar a una variable en lógica de primer orden , es un elemento que se puede utilizar en una fórmula lógica y que puede tomar varios valores diferentes.
