Clock (model checking)
In
Generally, the model of a system uses many clocks. Those multiple clocks are required in order to track a bounded number of events. All of those clocks are synchronized. That means that the difference in value between two fixed clocks is constant until one of them is restarted. In the language of electronics, it means that clock's jitter is null.
Example
Let us assume that we want to modelize an elevator in a building with ten floors. Our model may have clocks , such that the value of the clock is the time someone had wait for the elevator at floor . This clock is started when someone calls the elevator on floor (and the elevator was not already called on this floor since last time it visited that floor). This clock can be turned off when the elevator arrives at floor . In this example, we actually need ten distinct clocks because we need to track ten independent events. Another clock may be used to check how much time an elevator spent at a particular floor.
A model of this elevator can then use those clocks to assert whether the elevator's program satisfies properties such as "assuming the elevator is not kept on a floor for more than fifteen seconds, then no one has to wait for the elevator for more than three minutes". In order to check whether this statement holds, it suffices to check that, in every run of the model in which the clock is always smaller than fifteen seconds, each clock is turned off before it reaches three minutes.
Definition
Formally, a set of clocks is simply a finite set[1]: 191 . Each element of a set of clock is called a clock. Intuitively, a clock is similar to a variable in first-order logic, it is an element which may be used in a logical formula and which may takes a number of differente values.
Clock valuations
A clock valuation or clock interpretation[1]: 193 over is usually defined as a function from to the set of non-negative real. Equivalently, a valuation can be considered as a point in .
The initial assignment is the constant function sending each clock to 0. Intuitively, it represents the initial time of the program, where each clocks are initialized simultaneously.
Given a clock assignment , and a real , denotes the clock assignment sending each clock to . Intuitively, it represents the valuation after which time units passed.
Given a subset of clocks, denotes the assignment similar to in which the clocks of are reset. Formally, sends each clock to 0 and each clock to .
Inactive clocks
The program
When allowing for inactive clock, a valuation may associate a clock to some special value to indicate that it is inactive. If then also equals .
Clock constraint
An atomic clock constraint is simply a term of the form , where is a clock, is a comparison operator, such as <, ≤, = ≥, or >, and is an integral constant. In our previous example, we may use the atomic clock constraints to state that the person at floor waited for less than three minutes, and to state that the elevator stayed at some floor for more than fifteen seconds. A valuation satisfies an atomic clock valuation if and only if .
A clock constraint is either a finite conjunction of atomic clock constraint or is the constant "true" (which can be considered as the empty conjunction). A valuation satisfies a clock constraint if it satisfies each atomic clock constraint .
Diagonal constraint
Depending on the context, an atomic clock constraint may also be of the form . Such a constraint is called a diagonal constraint, because defines a diagonal line in .
Allowing diagonal constraints may allow to decrease the size of a formula or of an automaton used to describe a system. However, algorithm's complexity may increase when diagonal constraints are allowed. In most system using clocks, allowing diagonal constraint does not increase the expressivity of the logic. We now explain how to encode such constraint with Boolean variable and non-diagonal constraint.
A diagonal constraint may be simulated using non-diagonal constraint as follows. When is reset, check whether holds or not. Recall this information in a Boolean variable and replace by this variable. When is reset, set to true if is < or ≤ or if is = and .
The way to encode a Boolean variable depends on the system which uses the clock. For example,
Sets defined by clock constraints
A clock constraint defines a set of valuations. Two kinds of such sets are considered in the literature.
A
Given a model , it uses a finite number of constants in its clock constraints. Let be the greatest constant used. A region is a non-empty zone in which no constraint greater than are used, and furthermore, such that it is minimal for the inclusion.
See also
Notes
- ^ .
- ^ Behrmann, Gerd; David, Alexandre; Larsen, Kim G (November 28, 2006). "A Tutorial on Uppaal 4.0" (PDF): 28.
{{cite journal}}
: Cite journal requires|journal=
(help)