"Monitor is a module that watches for bad behaviours.
Why use monitors?
Some properties are hard or impossible to state in CTL. Example:
Store-Load order. Let X be a memory location.
"If load_req X follws store_req X, then the store must be serviced before the load."
CTL[DC]
is a highly expressive extension of CTL which allows most properties to
be written in
a simple and natural fashion. CTL[DC]
TOOL SET automatically generates monitors (synchronous
observers) for checking the property. The monitors are generated
in a wide variety of notations including SMV, BLIF-MV and ESTEREL.
For details see the DCVALID
page.
For example, the above property can be written in CTL[DC] as
AG # ! <>
(<store_req(X)>^[[ ! store_service(X)]] &&
<> ( <load_req(X)>^true^<load_service(X)>)
)
#
Informally, this means thare must be no fragement of behaviour which
begins with store_req(X) and has ! store_service(X) throughout and
has load_req(X) followed by load_service(X) somewhere within it.
Some explanation: Formula D between #D# is a QDDC (Quantified Discrete-time Duration Calculus) formula which is a form of interval temporal logic. It specifies a set of finite sequence of states (like regular expressions). Formula #D# holds at a node of a computation tree if the PAST of the node (state sequence from root to the current node) satisfies D.
Details of logic QDDC can be found in dcvalid.doc.
In brief, modality []D says that for all subsequences
formula D, whereas <>D says that for some subseqence D holds.
Formula [[P]] means proposition P is invariantly true throughout the sequence.
Formula <P> holds for a single state sequence where P is true. D1^D2
fuses sequence s1 satisfying D1 to sequence s2 satisfying D2 provided
the last state of s1 is same as first state of s2 (as in sequential
composition of program statements S1;S2).
QDDC also has measurement formulae. Construct slen=m
specifies a sequence spanning m+1 states. Construct sdur
P = m specifies a sequence with m occurrences of proposition P within
it. Boolean combinators &&, ||, !, =>, <=> are available.
The CTL[DC] formulation of this property is quite natural and simple.
AG #[] ( <Ahold & Breq> ^[[!Bhold]]
=> ! <> <!Ahold>^(slen=1)^<Ahold> ) #
Informally, this states that for ANY fragment (subsequence) of the
behaviour
which begins with Ahold and Breq and which has Bhold false throughout
there will be no subfragment with state !Ahold immediately followed
by state Ahold.
Lab 8 Bonus problem 8 (see [4])
"If A requests the bus and the bus is free, then
A gets control of the bus within 5 clock cycles unless B or C request the
bus in the mean-time."
AG # [] ( (<Areq && Busfree> ^ [[! Breq && !Creq]] &&
slen=4) => <> <Agrant> ) #
Informally, for all fragments of behaviour which begin with Areq
and Busfree, have length 4 (i.e. span 5 states) and do not have any occurrence
of Breq or Creq in them will have some occurrence of Agrant within it .
POLIS Formal-Verification Example (see Balarin et al [5]).
A shock absorber controller: The following property is required to
be verified.
P1.1: If speed sensors indicate impossibly
high speed at least three times and no RESET events occur, then ERRPAR
will be generated.
This can be stated in CTL[DC] as follows. We assume availability of
a signal called IMPHIGH standing for impossibly high speed and also
signals ERRPAR, RESET.
AG # [] ( ( scount IMPHIGH >=3 ) && [[ !
RESET ]] => <> <ERRPAR> ) #
The following simpler property is verified in polis tutorial by manually constructing a BLIF_MV monitor for it.
P1.1' If four SPEEDSENS events occur between
two CLOCK500 events (while there is no RESET) then ERRPAR event is generated.
This can be stated in CTL[DC] as follows.
AG # [] ( ( <CLOCK500>^ slen=1^
((scount SPEEDSENS = 4 ) && [! CLOCK500] && [[ !RESET]]
)
)
=> <> <ERRPAR>
)
#
Informally, this states that for any fragment
of behaviour starting with <CLOCK500> and having no CLOCK500 afterwords,
if there is no RESET throughout the fragment and number of SPEEDSENS during
the fragement are 4 then there must be an ERRPAR event somewhere.
The English specification is very ambiguous.
(1) if RESET occurs simultaneously with CLOCK500
followed by four SPEEDSENS should ERRPAR be generated? (our formula
says yes.)
(2) If fourth SPEEDSENS occurs simultaneously
with another CLOCK500 should there be ERRPAR?
(our fomula says
yes).
(3) If a SPEEDSENS occurs simultaneously
with first CLOCK500 should this be counted?
(our formula says
no).
(2) What if RESET occurs simultaneously with
fourth SPEEDSENS?
(our specification
says ERRPAR is not required.)
CTL[DC] gives full control to the user to specify all the variants of the above property.
[2] Serdar Tasiran, Session 7, VIS technology transfer course [1].
[3] Rajamani Sundar, Lab Session 6, VIS technology transfer course [1].
[4] Serdar Tasiran, Lab session 8, VIS technology transfer course [1].
[5] Balarin et al, Formal Verification with POLIS Co-design environment
for control-dominated embedded systems - A tutorial, December 1996.