Examples of complex properties from VIS Literature

Paritosh Pandya July 2000
Technical Note TN-2000-02

VIS technology transfer course [1]
POLIS distribution [5]

From Session 7 of VIS technology transfer course (see [2])

"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.

Some more examples

Lab 6 Problem 6 (see [3])
Specify the property "If A is holding the bus and B is requesting, then it is not possible for A to release control of the bus and get it back, before B gets control of the bus" in CTL. This is called Request Opportunity.  ... WARNING: The CTL specification of this property is non-trivial.

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.


[1] VIS technology transfer course, Unversity of Berkeley, May 1996.
(available on Web at http://www-cad.eecs.Berkeley.EDU/Respep/Research/vis/visttc.html)

[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.