The TTM SAMPLE

When using VERIFY we distinguish between:

To use VERIFY, all that is needed is the Prolog representation of the TTM which is quite similar to the mathematical description. A visual tool called BUILD5 has been developed, which ties together all three aspects of the TTM. BUILD allows the designer to enter the TTM visually as a TTM-CHART, uses the semantics to execute computations, and generates the required Prolog representations.

Consider the TTM-CHART of the timed transition model SAMPLE in Figure~#fig:sample#85>.

<#1315#>Figure<#1315#>: <#1316#>A TTM-CHART of the timed transition model sample<#1316#>
#figure86#

Formally the timed transition model SAMPLE is a 3-tuple

#math124#

SAMPLE = (#tex2html_wrap_indisplay1321#SAMPLE, ΘSAMPLE,#tex2html_wrap_indisplay1324#SAMPLE)

consisting of a a set of variables #math125##tex2html_wrap_inline1328#SAMPLE, an initial condition #math126#ΘSAMPLE, and a set of transitions #math127##tex2html_wrap_inline1333#SAMPLE.

The set of TTM variables is #math128##tex2html_wrap_inline1337#SAMPLE = {#tex2html_wrap_inline1338#, t, x, c, y, z} where each variable has a type given by:

#math129#
type(t) = {0, 1, 2, ... } = type(y)  
type(#tex2html_wrap_indisplay1344#) = #tex2html_wrap_indisplay1349#SAMPLE  
type(x) = {#tex2html_wrap_indisplay1353#  
type(z) = { ... , -2, -1, 0, 1, 2, ... }  

and the initial condition is:

#math130#

ΘSAMPLE = [x = #tex2html_wrap_indisplay1358#∧z = 1∧(c = 1∨c = 0)∧y = 0]

and the set of transitions is:

#math131#

#tex2html_wrap_indisplay1362#SAMPLE = {tick, a, b, d, e, f, g}

Each transition #math132#τ∈#tex2html_wrap_inline1364# is a 4-tuple #math133#τ = (eτ, hτ, lτ, uτ), where eτ is the enabling condition, hτ is the transformation function, lτ is the lower time bound and uτ is the upper time bound. 

verbatim110#

The above table of transitions is written in Prolog style in which the TTM variables are written in upper case (e.g. <#169#>Y<#169#> instead of y). Conjunction is denoted by a comma (e.g. <#170#>X=off, Z;SPMgt;0<#170#>), disjunction is denoted by a semi-colon (e.g. <#171#>X=off; Z;SPMgt;0<#171#>), and negation is denoted by <#172#>not<#172#> (e.g. <#173#>not ( X=off; Z;SPMgt;0)<#173#> ).

Enabling conditions and initial conditions are examples of <#174#>state-formulas<#174#>, i.e. boolean-valued expressions in the TTM variables that can be evaluated to true or false in a single state. RTTL formulas are built up from state formulas, e.g.

<#1371#>S1:<#1371#>
#math134##tex2html_wrap_inline1380##tex2html_wrap_inline1381# --- henceforth (i.e. in the current state and all future states), the assertion <#177#>not( X=fast, Y=3 ) <#177#> is always true.

The symbol #tex2html_wrap_inline1383# therefore stands for <#178#>henceforth<#178#>.

<#1372#>S2:<#1372#>
#math135#(#tex2html_wrap_inline1385#)→#tex2html_wrap_inline1386##tex2html_wrap_inline1387# --- in any state in which <#181#>(C=0)<#181#> becomes true, from then onwards the only transition that can occur is a tick. (The state-formula <#182#>isTick(N)<#182#> asserts that #math136#(#tex2html_wrap_inline1389# = tick), i.e. the next transition taken is the clock tick.)

<#1373#>S3:<#1373#>
#math137##tex2html_wrap_inline1391##tex2html_wrap_inline1392# --- henceforth, in any legal state, either <#185#>Z=1<#185#>, or the transition <#186#>h<#186#> occurs, or the tick transition ocurs.

<#1374#>S4:<#1374#>
#math138##tex2html_wrap_inline1394#(#tex2html_wrap_inline1395#) --- henceforth, either <#188#>Z=1<#188#>, or the tick transition occurs.

<#1375#>S5:<#1375#>
#math139##tex2html_wrap_inline1397#→#tex2html_wrap_inline1398#~#tex2html_wrap_inline1399#~#tex2html_wrap_inline1400# --- if the transition <#193#>b<#193#> occurs, then, from that state and onwards <#194#>(C;SPMgt;=5) ; Y=0<#194#> holds true up to (but not necessarily including) the state in which the transition <#195#>e<#195#> occurs. If <#196#>e<#196#> does not occur, then <#197#>(C;SPMgt;=5) ; Y=0<#197#> holds true forever (after the occurrence of <#198#>b<#198#>).

The symbol #math140##tex2html_wrap_inline1402# stands for <#200#>unless<#200#>.

<#1376#>S6:<#1376#>
#math141##tex2html_wrap_inline1404#→#tex2html_wrap_inline1405#~#tex2html_wrap_inline1406# --- if <#204#>X=idle<#204#> becomes true, then in no less than 1 clock tick, but no more than 2 clock ticks, a state is eventually reached in which either <#205#>(X = fast)<#205#>, or <#206#>(Z = -1)<#206#>.

<#1377#>S7:<#1377#>
#math142#(#tex2html_wrap_inline1408#)→#tex2html_wrap_inline1409#(#tex2html_wrap_inline1410#) --- if the TTM is <#209#>off<#209#>, then eventually it must become <#210#>idle<#210#>.

<#1378#>S8 --- Deadlock Free<#1378#>
The requirement below specifies that in every (reachable) state, some transition other than tick must be enabled.

#math143#

#tex2html_wrap_indisplay1413##tex2html_wrap_indisplay1414#eτ

(The notation eτ stands for the enabling condition of the transition τ and #math144##tex2html_wrap_inline1420##tex2html_wrap_inline1421# stands for the set of all transitions of the TTM <#218#>sample<#218#>).

VERIFY can be used to check the correctness of all the above specifications. Note that since the set of legal trajectories is suffix closed, in RTTL the validity of #tex2html_wrap_inline1423#w follows from the validity of w. Thus, in RTTL

#math145#

[p1→#tex2html_wrap_indisplay1426#p2]≡[#tex2html_wrap_indisplay1427#(p1→#tex2html_wrap_indisplay1428#p2)]

In order to check SAMPLE for the above properties, two files are needed:

<#1429#><#221#>sample.ttm<#221#><#1429#>
--- the Prolog description of the TTM SAMPLE (see Appendix~#app:ttm#222>).

<#1430#><#223#>sample.sf<#223#><#1430#>
--- the file containing the atomic state-formulas from which specifications in RTTL are constructed (see Appendix~#app:sf#224>).

Once these files are present, the RG2 reachability graph must be constructed, after which the various specifications can be checked.