* Automata theoretic approach to __validity
checking__ QDDC formulae

- Visualising models and countermodels of QDDC formulae* Extension to Liveness and Branching: Logic CTL[DC]

- Validity checking

- Currently available for* Extension to Dense-time: Logic LIDL

SMV designs and CTL[DC] formulae usingctldcandsmv

Verilog designs and CTL[DC] formulae using toolctldcandVIS

Esterel designs and restricted CTL[DC] formulae usingctldc,esterelandXeveEsterel designs and CTL[DC] formulae usingctldc,esterelandVIS

-Can perform quantitative analysis of models.

- Example (properties of synchronous bus arbiter)

(subset of Interval Duration Logic (IDL))

- Status: Partial Implementation using Uppaal (not released)

Formally, words over alphabet (Pvar -> {0,1})

**Example:** <P>^[!Q]^<Q>

all sequences which begin with P true, end with Q true

and Q is not true anywhere before the endpoint.

Model:

P 1 X X X X

Q 0 0 0 0 1

Coutermodel:

P 1 X X X X

Q 1 X X X X

X denotes dont-care which can be arbitrarily substituted with 0 or 1.

**Example:** (<P>^true) &&
(slen=3) && (sdur Q = 2)

Sequence begins with P true and has step-length 3 (i.e. 4 states) and
Number of occurrences of Q in it is 2 (disregarding the end point).

A satisfying example of least length (4) is:

P
1 XX X

Q
0 1 1 X

A counter-example of least length (1) is:

P
0

Q
X

a finite state automaton

I |= D iff I in Lang(A(D))

Tool DCVALID constructs this automaton. The automaton for <P>^[!Q]^<Q>
is given below.

Each two bit column vector gives valuation of <P,Q>. Value X is
don't care (0 or 1).

This formula specifies that state sequence begins with P true and has step-length 3 (i.e. 4 states) and Number of occurrences of Q in it (disregarding the end point) is 2. The automaton for this formula is given below.

I, [b,e] |= D (see manual for definition)I |= D iff I,[0,#I-1] |= D

<A> | b=e and I,b |= A |

[A] | b<e and invariant A in [b,e) |

[[A]] | invariant A in [b,e] |

{{A}} | [P] && slen=1 |

slen >=3 | e-b >= 3 |

sdur B = 2 | #P in [b,e) = 2 |

scount B = 2 | #P in [b,e] = 2 |

D1^D2 | chop. Holds if exists m:b<=m<=e s.t. I,[b,m] |= D1 and I,[m,e] |= D2 |

D1 && D2, D1 || D2, !D | boolean combinators |

ex p. D, all p. D | state quantification |

*D | iteration (defined using ex p. D) |

pt, ext, unit | dc abbreviations |

<>D | there exists a subinterval where D holds. Defined true^D^true |

[]D | All subintervals satisfy D. Defined ! <> !D |

{A} =3=> {B} | follows (arrow operator). See manual. |

{A} <=4= {B} | tracks (arrow operator). See manual |

define N[ p1, p2, ... , pn] as D | macro definition |

N[A1 , A2 , ...., An ] | macro expansion |

* $dcvalid *spec*

- produces *output*giving

satisfying example I1 and

counter example I2

- Reports if formula is valid or
unsatisfiable

* $dcautps *spec spec.ps*

- produces a postscript file containing automaton recognising all the models of spec.* Modelchecking features are described later.

Typical Usage:

|= Sysspec => Req

* Fischer protocol

* Delay insensitive inverter using C-gate

* n-bit Adder

* 5-Synchronous Bus Arbiter

* system model M in suitable programming language

Currently SMV, Verilog and Esterel are supported.

* property D in logic CTL[DC]

CTL[DC] extension of QDDC with liveness and branching.

CTL[DC] extends CTL with past-time properties.

useful for response-time and quantitative
analysis (Examples)

Computation Tree C, node n

C, n |=
R

CTL[DC] formulae :

* R(#D1# , ... , #Dn#) where R is
CTL formula and D1, ... , Dn are QDDC formulae.

Each #D# occurs like
a proposition. It states "Past satisfies D".

* D1, ..., Dn are used like atomic propositions in CTL.

* D holds at a node of computation
tree if the unique path

from the
root to the node satisfies D.

Example: AG AF #D# means infinitely often D

TCS00-PKP-2 techincal report on CTL*[DC] with syntax and semantics.

"If Loadreq follows Storereq
then Store must be served before Load."

AG # [] (<Storereq>^[[!Storeserv]] => ! <> ( <Loadreq> ^true^<Loadserv>)
)#

"If req is continuoulsy
held high for m cycles, there will be at least k acknowledgements."

AG # [] ( ([[req]] && (slen = m-1)) => (scount ack >= k))#

Examples from model checking literature of complex properties which can be nicely stated in CTL[DC].

**Main Example:** Some complex
properties of a synchronous bus arbiter.

* CTL[DC] is particularly useful for stating bounded response/ performance
requirements.

"There are at most m
consecutive lost cycles."

AG #[] ( [[lostcycle]] => slen < m) #

We can reduce CTL[DC] modelchecking to CTL modelchecking by running synchronous observers

(monitors) in parallel with system.M |= R(D1, ... , Dn) iff M' |= R(End1, ... , Endn)

where End1, ... , Endn are fresh propositions witnessing when past satisfies D1, ... , Dn

M' is modified system model

M' behaves like M but additionally sets propositions End1, ... , Endn appropriately.

Construction of M' is based on Automata for D1, ... , Dn (see Theorem).Transformed model M' preserves FAIRNESS PROPERTIES an COUNTER EXAMPLES.

TCS00-PKP-2 techincal report on CTL[DC] modelchecking

Tool CTLDC performs the above reduction.

The reduction is performed for M in

SMV

Verilog

Esterel

CTL[DC] specification format

$ctldc prop syncarb5.smv

give reduced
verification problem propfin.smv

This can be
model checked using smv

$smv propfin.smv

-- specification AG (propobs1.ENDST & propobs2.ENDST) is true

resources used:

user time: 0.02 s, system time: 0.01 s

BDD nodes allocated: 2355

Bytes allocated: 1245184

BDD nodes representing transition relation: 296
+ 7

$ctldc prop syn5.v

give reduced
verification problem propfin.mv (blif-mv)and
prop.ctl

This can be
model checked using VIS

$vis

>read_blif_mv propfin.mv

>init_verify

> mc prop.ctl

# MC: formula passed --- AG((ENDST1=1
* ENDST2=1))

These must be written as equivalent formula !EF #!D#

Such formulae specify

Example: Synchronous Bus Arbiter in Esterel

**Arbiter
circuit** (Circuit and model by Robert de Simone. Distributed
with Xeve.)
** Esterel
model (file arbiter5-cyclic.strl)**
** Property
(file proparb)**

$ctldc proparb arbiter5-cyclic.strl

give reduced
verification problem proparbfin.strl

This can be
model checked using esterel and Xeve

$esterel -Lblif -causal proparbfin.strl

This gives file
propfin.blif

$checkblif -output { DCERR1 DCERR2 DCERR3 } proparbfin.blif

--- chkblif: Computing the FSM reachable states

--- chkblif: Output DCERR1 NEVER EMITTED

--- chkblif: Output DCERR2 NEVER EMITTED

--- chkblif: Output DCERR3 NEVER EMITTED

Synchronous Bus Arbiter in Esterel

**Arbiter
circuit**
** Esterel
model (file arbiter5-cyclic.strl)**
** Property
(file propvest) **This contains three properties.

$ctldc propvest arbiter5-cyclic.strl

give reduced
verification problem propvestfin.mv
(blif-mv format) and propvest.ctl

This can be
model checked using VIS

$vis

>read_blif_mv propvestfin.mv

>init_verify

> mc propvest.ctl

# MC: formula passed --- !(EF(ENDST1=1))

# MC: formula passed --- !(EF(ENDST2=1))

# MC: formula passed --- !(EF(ENDST3=1))

Some complex
properties

Conclusions

Solution
using CTLDC and SMV (see readme.txt)

Solution
using CTLDC and VIS (see readme.txt)

Solution using CTLDC and Esterel

Solution using CTLDC, Esterel and VIS

MAXDCLEN(D) Compute the length of longest subsequence (within all executions of the system) which satisfies D.

MINDCLEN(D) Compute the length of shortest subsequence (within all executions of the system) which satisfies D.

MAXDCLEN( (scount ack < 3) && [[req]] )

computes the maximum number of cycles for which request can remain high continuosly without getting at least three acknowledgements.

The ctldc with NuSMV computes this value as 19. Thus, if request is held high for 20 cycles, there will be at least three acknowledgements.

**Note:**

Specification MAXDCLEN(D) gives the number
of states in the longest subsequence satisfying D.
This is the length of subsequence+1. Thus, MAXDCLEN(
slen=0 ) = 1. Value MAXDCLEN(D) =0 indicates
that D is is never satisfied during any execution. Value MANDCLEN(D)
=infinity indicates that there is no finite
bound on lengths of subsequences satisfying D.

Specification MINDCLEN(D) gives the length of shortest subsequence satisfying D. This is number of states -1. Thus, MINDCLEN( slen>=0 ) = 0. Value MINDCLEN(D) =infinity indicates that D is is never satisfied during any execution.

Duration Calculus redefined on Timed words of Alur and Dill

Subset LIDL with located constraints.

Timed/hybrid automata based decision procedure.

For every formula D, an
integrator automaton A(D) accepting

timed state sequences which
are models of D.

(See Technical Report TCS-00-PKP-5
for details)

Tool support (forthcoming)

DCUPPAAL translates
LIDL formula to timed automaton in Uppaal .ta notation

Validity Checking:

A(D) analysed for reachability
of final state to find satisfiability

A(D) analysed for reachability
of non-final state to find unsatisfiability

Tools such as Uppaal or
Hytech used for reachability analysis

Model Checking Approach:

M |= D iff M ||
A(!D) cannot reach final state of A.

A(!D) is called *synchronous observer* or
*monitor*
for !D

|| is synchronous product.

We reduce modelchecking of LIDL to reachability.

Created by Paritosh Pandya May 2000 for demonstration at UNU/IIST Macau.

Last modified by Paritosh Pandya 2 October 2000.