Design Verification Patterns - Formal Methods and Hybrid Real-Time Systems - page 402

where STOP is the deadlocked process, SKIP is the terminating process, ce → P

communicates event ce and continues as P , P P is external choice, P P is

non-deterministic choice, P P is parallel composition, and P ; P is sequential

composition. As usual, recursive definition of processes is allowed.

Duration Calculus. Duration Calculus formalizes dynamic systems properties.
The basis is the well-known time-domain model , where a system is described by a
collection of states which are functions of time (the non-negative real numbers).
The state names are here the variables in a given schema, which clearly vary
over time.
A behaviour of a system is thus an assignment of state functions to the names
of elementary states, An observation of a behavior is a restriction of such an
assignment to a bounded interval; it can be illustrated by a timing diagram.
Boolean values and thus the value of state predicates are by convention repre-
sented by 0 ( false )and1( true ).
For a given observation interval [ b, e ]ofapredicate P ,the duration , denoted

P is simply the integral e
b

P ( t ) dt ; it measures the fraction of time P holds in

the interval.
Duration terms are built from durations, logical variables and real numbers
and closed under arithmetic operators and arithmetic relations. Duration for-
mulas D are built from duration terms of Boolean type and closed under propo-
sitional connectives, the Interval Temporal Logic [22] ”chop” connective, and
quantification over rigid variables and variables of duration terms.
A duration formula D holds in [ b, e ] if it evaluates to true. For the predicate
P , it is obvious that it holds (almost everywhere) in the interval, just when the

duration P is equal to the length of the interval. The length is the duration of

the constant function 1 ( 1). This duration is often used, so it is abbreviated
( ), pronounced 'the length'. The property that P holdsisthusgivenbythe

atomic formula P = . This holds trivially for a point interval, so we consider
proper intervals of a positive length. These two properties are combined in the
abbreviation

== ( P = )

P ∧ ( > 0)

read as ' P holds'.
Given formulas D and E , the binary ”chop” connective can combine them to
D ; E which holds on [ b, e ] when there exists a m such that D holds on [ b, m ]and
E holds on [ m, e ]. A simple example is the valid equivalence

.
With CSP, we include event based reasoning by defining that for an event ce ,
the formula

P = P ; P

ce holds exactly when the event occurs at the beginning of the
interval. Thus we can specify an interval where ce does not occur in the open
interval by the counterexample formula

↑

ce == ¬ ( > 0;( ↑ ce ); > 0))