%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                                                   %
% Documentation for VERIFY - a real-time verifier                   %
%                            by J.S. Ostroff - jonathan@cs.yorku.ca %
%                                                                   %
%  Run latex on this file THREE times                               %
%                                                                   %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\documentstyle[12pt]{article} 
\pagestyle{headings}

%% Definitions
\def\true{{\it true}}
\def\false{{\it false}}
\def\Implies{\Rightarrow}
\def\implies{\rightarrow}
\def\andd{\wedge}
\def\orr{\vee}
\def\fe{\forall}
\def\te{\exists}
\def\n{{\bf n}}
\def\hn{\Box}
\def\ev{\Diamond}
%% End Definitions

\title{VERIFY - a verifier for real-time systems} \author{Jonathan S.
Ostroff\thanks{Jonathan Ostroff is with the Department of Computer
Science, York University 4700 Keele Street, North York, Ontario,
Canada, M3J 1P3. Email: jonathan@cs.yorku.ca.  This work is supported
by the Natural Sciences and Engineering Research Council of Canada}}
\date{June 1, 1992}
 


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{document}
\maketitle
\begin{abstract}
VERIFY is a tool for checking finite state real-time systems in
the temporal logic RTTL. Each process in the system to be verified
is declared, in Prolog, as a transition system with lower and upper
time bounds on each transition (0 and $\infty$ if the bounds are
unknown). The processes can be composed in parallel to form more
complex systems of concurrent processes. To check an RTTL
property (such as freedom from deadlock or a real time response
property), VERIFY generates a state reachability graph, and
checks the RTTL property over the reachability graph. The
processes may have data variables so that various data types and
operations on data can be accommodated. If the property does not
hold, the state (or sequence of states) for which the property fails
to hold is provided. This information is useful in debugging the
design.

VERIFY is part of a toolset that is being developed at York
University (Canada) for the design of real-time safety critical
systems. The TTM/RTTL framework forms the underlying
theoretical basis for the tools.  TTMs are timed transition
systems, and RTTL stands for real-time temporal logic.

Another tool called BUILD is currently under development. BUILD is a
visual specification tool for constructing complex systems as
hierarchical TTMs. BUILD also allows for the execution of the TTMs,
as well as producing the input Prolog descriptions of the systems
as Prolog code suitable for input to VERIFY.

\end{abstract}
\tableofcontents
\newpage

\section{Getting Started}
%%%%%%%%%%%%%%%%%%%%%%%%%

This document describes a Prolog program called VERIFY to verify
the correctness of real-time reactive systems. The references in
\cite{Ost90a,Ost92a} describe the TTM/RTTL framework that is used to
model and check real-time systems.

VERIFY was written in Quintus
Prolog\footnote{Quintus Prolog is a copyright of Quintus Computer
Systems, Inc.} Version 3.0, and has been tested on both SUN and DEC
workstations. VERIFY should work on any platform that supports Quintus
Prolog Version 3.0 (hereafter referred to as QP)\footnote{There
is also a QOF file avialable for Quintus Prolog 2.5.1}.

The program was written as a prototype for use on small systems with
a couple of hundred states, although it has also been used on systems
with about 10,000 states. It should not be relied on as the sole check
of correctness of safety critical software.

\subsection{VERIFY}
%%%%%%%%%%%
VERIFY implements the decision procedures described
in \cite{Ost90a} for automatically checking a small but important class
of properties for any finite state TTM (timed transition model). The
procedures are linear in the size of the system state reachability
graph. Real-time temporal logic (RTTL) is used for specifying the
properties to be verified.

The following steps are involved in verifying a given property.
\begin{enumerate}

\item (Modelling step) Given a system composed of a set of interacting
real-time discrete event processes, construct the corresponding TTM
$M$. TTMs can be composed in parallel, e.g. $M= M_1\| M_2\| M_3$, where
$M_1$ may itself be the parallel composition of many TTMs. 

\item Compute the reachability graph $G_M$ of $M$ using the RG2
procedure described in \cite{Ost90a}. The RG2 procedure ensures
that only those states that are actually reachable are computed
--- lower and upper time bounds on events may constrain the TTM to
fewer states than events with no bounds on them.

\item Specify a formula $w$ in RTTL that describes the behaviour that
$M$ must satisfy.

\item Apply the appropriate decision procedure for $w$. All decision
procedures perform an analysis of the RG2 reachability graph $G_M$.

\end{enumerate}

\subsection{Quintus Prolog}
%%%%%%%%%%%

There are three ways to run VERIFY under QP:

\begin{description}

\item[On terminals:] VERIFY can be run in a fashion similar to a line
editor, or under GNU Emacs (or Unipress Emacs). Running under Emacs
allows the user to examine input files in one window, while executing
commands in another window. Sessions can be saved on file, and
previous commands can be repeated by appealing to command histories.

\item[X11 --- QUI:] The Quintus User Interface (QUI) is based on the
X11 windowing system and the use of the mouse. VERIFY can also be
run under QUI.  

\end{description}

QP allows a program to be saved in a compiled
form called a QOF file (Quintus Object Format). QOF files contain a
machine independent representation of both compiled and dynamic Prolog
procedures. This means that QOF files are completely portable between
different platforms running Quintus Prolog. 

VERIFY is made available in QOF format at no charge to researchers.
The author retains the copyright to the VERIFY software. No changes
may be made to the software without the written permission of the
author.


\subsection{Installing VERIFY} \label{start}
%%%%%%%%%%%

The file {\tt verify31.tar.Z} must be obtained by anonymous
ftp
\footnote{ 
If you are using Quintus Prolog 2.5, then ftp the file {\tt
verify251.tar.Z}.
When using this version of prolog, the file
{\tt dynam.ttm} must be available if the {\tt compose} procedure is
used.  Also the lines beginning with the {\tt multifile} and 
{\tt dynamic} declarations 
%\begin{verbatim}
%:- multifile map/3, type/3,initialcondition/2, en/3, h/4, lohi/4.
%:- dynamic map/3, type/3, initialcondition/2, en/3, h/4, lohi/4.
%\end{verbatim} 
in the {.ttm} files must be commented out.  } 
from the {\tt pub/AUTOMATE} directory on the server {\tt nexus.yorku.ca}. Then,
uncompress and restore all the required files by executing:

\begin{verbatim}
uncompress verify31.tar.Z
tar -xvf verify31.tar
\end{verbatim}

This will create a directory {\tt verify} which will contain the QOF
file {\tt verify31}, as well as various examples.

\subsection{Invoking VERIFY}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%

VERIFY can be started up under the assumption that (a) Quintus Prolog
3.0 is installed, and (b) the {\tt verify} directory has been
properly installed as described in Section~\ref{start}.

There are three ways to get started. Either invoke the QOF file {\tt
verify} from the Unix command line:
\small\begin{verbatim}
unix prompt>  ./verify
% loading file ...

VERIFY Version 1.0 May 7, 1992
 Copyright Jonathan Ostroff, York University.
 email : jonathan@cs.yorku.ca 


                Type "routines" for a list of available routines.



Quintus Prolog Release 3.1.1 (Sun-4, SunOS 4.1)
Copyright (C) 1990, Quintus Corporation.  All rights reserved.
2100 Geng Road, Palo Alto, California U.S.A. (415) 813-3800

| ?-
\end{verbatim}\normalsize

Alternatively, Quintus Prolog can be invoked under Emacs. First
execute the command {\tt \% prolog +} to run Emacs. At the Prolog
prompt in the Emacs window, VERIFY can be invoked by executing the
Prolog command {\tt restore(verify).} (Help for either prolog or
emacs can be obtained by executing the prolog command {\tt manual.}).

A third possibility is to call {\tt qui} from the Unix command line to
invoke the X11 interface QUI (QUI can usually be invoked by executing
{\tt % qui &} from the Unix command line). VERIFY can then be invoked by
doing the Prolog procedure  {\tt restore(verify).} as before.

The Prolog command ``{\tt routines.}'' will provide a list of all the
VERIFY procedures that can be invoked.

\small\begin{verbatim}
| ?- routines.


        Graph Routines          rg2(TTM). 
        ---------------         compose([TTM1...TTMn], NewTTM).

        Display Routines :      statistics(TTM).
        ----------------        graph(TTM).
                                uniqueStates(TTM).
                                allStates(TTM).
                                initialStates(TTM).

        Verification Routines:  henceForth(TTM, Property1, Property2,
        ----------------------                Answer, Location).

                                unless(TTM, Property1, Property2, Property3, 
                                              Answer, Location).
                                eventually(TTM, StateFormula1, StateFormula2, 
                                              Answer, Location).
                                rtrfRG2(TTM, InitialStateFormulaNumber,
                                              FinalStateFormulaNumber,
                                              MinLo, MaxHi).
                                          MaxHi).


        Predicates :            prop(TTM, Property, [StateContents,
        ----------                                   NextTransition]).
                                sf(TTM, Property, StateContents).


        If RoutineName is not unified, the descriptions of all the routines 
will be displayed.

yes
| ?- 
\end{verbatim}\normalsize

In addition, some routines are available for examining the files in
the current directory, or changing to a new directory in the Unix file
system.

\begin{description}

\item[{\tt cd(directory).} ---] changes the current directory to be
{\tt directory}. For example, cd(..) moves up one level, and
cd(sensor) changes the current directory to the subdirectory {\tt
sensor}.

\item[{\tt pwd.} ---] returns the path of the current directory.

\item[Other commands ---] Other commands include: {\tt cat(filename),
date, ls(directory), ls-l(directory), ls-l(directory),
ls-a(directory)} and {\tt ls-al(directory)}.

\end{description}

Although VERIFY is up and running, nothing can be verified until two
files are created:

\begin{description}
\item[{\tt sample.ttm}] --- this is the file containg the Prolog code
describing the real-time system as a TTM called {\tt sample}.

\item[{\tt sample.sf}] --- this file contains state-formulas that are
used to specify the property to be verified.

\end{description}

\section{An example}
%%%%%%%%%%%%%%%%%%%%

In this section, we will use an example TTM called SAMPLE to
illustrate the workings of the verifier. SAMPLE is a single simple
TTM, i.e. it is not the parallel composition of many TTMs. 

An example involving the parallel composition of processes, and using
shared variables, may be found in \cite{Ost92a}. VERIFY has a {\tt
compose} command which allows for TTMs to be composed in parallel. It
allows for the possibility of both (a) shared variables, and (b) shared
transitions. Thus, both asynchronous and synchronous communication can
be modelled. Concurrent and nondeterministic behaviour can also be
represented. TTMs can model most features of real-time programs, Petri
Nets, Statecharts and Communicating Sequential Processes. In
particular, TTMs have data variables that can be used to represent
program variables, arrays, records and other data structures. 

\subsection{The TTM SAMPLE}
%%%%%%%%%%%%%%%%%%%%%%%%%%%

When using VERIFY we distinguish between:

\begin{itemize}

\item The formal mathematical  description of a TTM. 

(A TTM $M$ is a 3-tuple $M = \{ {\cal V}, \Theta, {\cal T} \}$ where
$\cal V$ is a variables set, $\Theta$ is an initial condition, and
$\cal T$ is the set of all transitions. A precise operational
semantics describes all {\em legal trajectories\/} that the TTM can
execute.)

\item The visual presentation of TTMs via TTM-CHARTS (a modified form of
statecharts) --- other visual methods can just as easily be used, e.g
Petri Nets.

\item the Prolog representation of the TTM $M$ in a file called {\tt
m.ttm}.

\end{itemize}

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 BUILD\footnote{BUILD has not yet been made publicly
avialable as it is still being tested.} 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~\ref{fig:sample}. 

\begin{figure} 
{\tt    \setlength{\unitlength}{0.92pt}
\begin{picture}(506,410)
              \put(66,297){\begin{picture}(72,38)
\thicklines       \put(22,15){off}
                  \put(36,19){\oval(72,38)}
                  \end{picture}}
              \put(326,297){\begin{picture}(72,38)
\thicklines       \put(21,14){idle}
                  \put(36,19){\oval(72,38)}
                  \end{picture}}
              \put(329,142){\begin{picture}(72,38)
\thicklines       \put(20,15){slow}
                  \put(36,19){\oval(72,38)}
                  \end{picture}}
              \put(65,134){\begin{picture}(72,38)
\thicklines       \put(21,13){fast}
                  \put(36,19){\oval(72,38)}
                  \end{picture}}
\thicklines   \put(136,318){\vector(1,0){189}}
              \put(360,299){\vector(0,-1){118}}
              \put(328,160){\vector(-1,0){191}}
              \put(97,172){\vector(0,1){126}}
              \put(331,171){\vector(-3,2){199}}
              \put(146,327){${\bf a}[0,\infty]:  ~c>0~ \implies  [c:c+1]$}
              \put(330,306){\vector(-3,-2){202}}
              \put(332,228){\begin{picture}(110,26)
\thicklines       \put(0,16){${\bf b}[1,1]:$}
                  \put(0,2){$c\geq 2 ~\implies~  [y: 3+c, c:c+3]$}
                  \end{picture}}
\thicklines   \put(286,282){${\bf d}$}
              \put(47,77){definition of {\bf d}:  ${\bf d}[0,\infty]:~ c<2 ~\implies~ []$}
              \put(172,283){$\bf f$}
              \put(46,63){definition of {\bf f}:  ${\bf f}[2,3]: z>0 \andd y\leq 5~\implies~
[c:0]$}
              \put(149,143){${\bf e}[1,2]: y\geq 5 \andd z>0 ~\implies~  [y:y-1]$}
              \put(36,233){${\bf g}[0,0]:  y<5 ~\implies~ [c:0]$}
              \put(401,162){\line(1,0){46}}
              \put(448,162){\line(0,-1){65}}
              \put(449,98){\vector(-3,2){66}}
              \put(403,130){${\bf h}[1,1]: [z:-z]$ }
\thinlines    \put(422,384){SAMPLE(x)}
              \put(80,18){\bf INITIALLY:  
$[ x={\tt off} \andd z=1 \andd ( c=1 \orr c=0) \andd y=0]$}
              \put(253,205){\oval(486,390)}
\end{picture}} 
\caption{A
TTM-CHART of the timed transition model sample} \label{fig:sample}
\end{figure}

Formally the timed transition model SAMPLE is a 3-tuple 
\[ SAMPLE = ({\cal V}_{SAMPLE}, \Theta_{SAMPLE}, {\cal T}_{SAMPLE})\]
consisting of a a set of variables ${\cal V}_{SAMPLE}$,
an initial condition
$\Theta_{SAMPLE}$, and a set of transitions ${\cal T}_{SAMPLE}$.

The set of TTM variables is ${\cal V}_{SAMPLE} =
\{ {\bf n},t,x,c,y,z \} $ where each
variable has a type given by:
\begin{eqnarray*}
type(t) &=& \{0,1,2, \cdots\} = type(y)\\
type({\bf n}) &=& {\cal T}_{SAMPLE} \\
type(x) &=& \{ \tt off, idle, slow, fast \} \\
type(z) &=& \{ \cdots, -2, -1, 0, 1, 2, \cdots \}
\end{eqnarray*}
and the  initial condition is:
\[\Theta_{SAMPLE} = 
[x={\tt off} \andd z=1 \andd ( c=1 \orr c=0) \andd y=0] \]
and the set of transitions is:
\[ {\cal T}_{SAMPLE} =  \{tick, a, b, d, e, f,g\}\]

Each transition $\tau\in {\cal T}$ is a 4-tuple
$\tau =(e_{\tau}, h_{\tau}, l_{\tau},
u_{\tau})$, where $e_{\tau}$ is the enabling condition,
$h_{\tau}$ is the transformation
function, $l_{\tau}$ is the lower time bound and $u_{\tau}$ is the upper time
bound.

\begin{verbatim}
Tran  Guard:               Function:             Low  Upper:
----  ------               ---------             ---  ------
a     (X=off,(C>0))        [X:idle,C:C+1]        0    infinity
b     (X=idle,(C>=2))      [X:slow,Y:3+C,C:C+3]  1    1     
d     (X=idle,(C<2))       [X:fast]              0    infinity
e     (X=slow,(Y>=5,Z>0))  [X:fast,Y:Y-1]        1    2     
f     (X=slow,(Z>0,Y=<5))  [X:off,C:0]           2    3     
g     (X=fast,(Y<5))       [X:off,C:0]           0    0     
h     (X=slow)             [X:slow,Z:-Z]         1    1    
\end{verbatim}

The above table of transitions is written in Prolog style in which the
TTM variables are written in upper case (e.g. {\tt Y} instead of $y$).
Conjunction is denoted by a comma (e.g. {\tt X=off, Z>0}), disjunction
is denoted by a semi-colon (e.g. {\tt X=off; Z>0}), and negation is
denoted by {\tt not} (e.g. {\tt not ( X=off; Z>0)} ).

Enabling conditions and initial conditions are examples of {\em
state-formulas\/}, 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.

\begin{description}

\item[S1:] $\hn{\tt not( X=fast, Y=3 ) }$ --- henceforth (i.e. in
the current state and all future states), the assertion {\tt not(
X=fast, Y=3 ) } is always true. 

The symbol $\hn$ therefore stands for {\em henceforth\/}.

\item[S2:] $({\tt C=0}) \implies \hn{\tt isTick(N)}$ --- in any state
in which {\tt (C=0)} becomes true, from then onwards the only
transition that can occur is a tick. (The state-formula {\tt
isTick(N)} asserts that $({\rm\bf n}=tick)$, i.e. the next
transition taken is the clock tick.)

\item[S3:] $\hn {\tt ( Z=1 ; N=h ; isTick(N) )} $ --- henceforth,
in any legal state, either {\tt Z=1}, or the transition {\tt h} occurs,
or the tick transition ocurs.

\item[S4:] $\hn({\tt Z=1; isTick(N) })$ --- henceforth, either {\tt
Z=1}, or the tick transition occurs.

\item[S5:] ${\tt (N=b)} \implies {\tt (C>=5 ; Y=0)} ~{\bf U}~ {\tt
(N=e)}$ --- if the transition {\tt b} occurs, then, from that state
and onwards {\tt (C>=5) ; Y=0} holds true up to (but not necessarily
including) the state in which the transition {\tt e} occurs. If
{\tt e} does not occur, then {\tt (C>=5) ; Y=0} holds true forever
(after the occurrence of {\tt b}).

The symbol ${\rm\bf U}$ stands for {\em unless\/}.


\item[S6:] ${\tt (X=idle)} \implies \ev_{[1,2]}~ {\tt (X=fast ; Z = -1)}$ ---
if {\tt X=idle} 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 {\tt (X = fast)}, or {\tt (Z = -1)}.

\item[S7:] $({\tt X=off}) \implies \ev ({\tt X=idle})$ --- if the TTM
is {\tt off}, then eventually it must become {\tt idle}.

\item[S8 --- Deadlock Free] 
The requirement below specifies that in every (reachable)
state, some transition other than $tick$ must be enabled.
\[ \hn \bigvee_{\tau \in{\cal T}_{\tt sample} \andd 
{\rm\bf n}\neq tick}e_{\tau} \] (The notation $e_{\tau}$ stands for
the enabling condition of the transition $\tau$ and ${\cal T}_{\tt
sample}$ stands for the set of all transitions of the TTM {\tt
sample}).

\end{description}

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 $\hn w$ follows from the
validity of $w$. Thus, in RTTL 
\[ [p_1\implies \ev p_2] \equiv [\hn(p_1\implies\ev p_2)] \]

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

\begin{description}
\item[{\tt sample.ttm}] --- the Prolog description of the TTM SAMPLE
(see Appendix~\ref{app:ttm}).

\item[{\tt sample.sf}] --- the file containing the atomic
state-formulas from which specifications in RTTL are constructed
(see Appendix~\ref{app:sf}).

\end{description}

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

\subsection{Construction of the RG2 reachability graph}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

The RG2 reachability graph is constructed using the {\tt sample.ttm}
file as follows:

\small\begin{verbatim}
%%%  Make sure the current directory contains the sample.ttm file.
| ?- ls.
sample.sf  sample.ttm
yes
%%% Use "cd(directory)" to change to the correct directory if
%%% necessary.
%%%
%%% Construct the rg2 reachability graph.
| ?- rg2(sample).
...
yes
%%% Obtain the number of states and edges in the graph.
| ?- statistics(sample).
...
	Statistics for TTM :  sample

		Unique States = 7
		Total States  = 10
		Total Edges   = 12
yes
%%% Obtain the state contents as well as state names.
| ?- uniqueStates(sample).
 State		State
	Number		Contents [X,C,Y,Z]
	======		========
	0	<=>	[off,1,0,1]
	1	<=>	[off,0,0,1]
	2	<=>	[idle,2,0,1]
	3	<=>	[slow,5,5,1]
	4	<=>	[fast,5,4,1]
	5	<=>	[slow,5,5,-1]
	6	<=>	[off,0,4,1]
There are 7 unique states for TTM sample.
yes
| ?- allStates(sample).
...
	      State	     History
	      Number	     Number
	      ======	     ======

                0              0
                1              1
                2              2
                2              3
                3              4
                3              5
                4              6
                5              7
                6              1
                5              8
There are 10 states for TTM sample.
yes
%%% Thus a state numbered 2-8 means state number 2 with transition 
%%% history 8. State 2-5 has the same values of [X,X,Y,Z] as state
%%% 2-8, the only difference being the transition histories.

%%% Now examine the reachability graph.
| ?- graph(sample).
Source          Destination
State   Event   State
======  =====   ===========
		    	[tick,1]
	0-0		-------->	0-0

      			a
	0-0		-------->	2-2

			    [tick,1]
	1-1		-------->	1-1

		    	[tick,1]
	2-2		-------->	2-3

	      		b
	2-3		-------->	3-4

	   	 	[tick,1]
	3-4		-------->	3-5

		      	e
	3-5		-------->	4-6

	      		h
	3-5		-------->	5-7

      			g
	4-6		-------->	6-1

	   		[tick,1]
	5-7		-------->	5-8

		   	[tick,1]
	6-1		-------->	6-1

	      		h
	5-8		-------->	3-4

There are 12 edges for TTM sample.
yes
| ?- 
\end{verbatim}\normalsize

\subsection{Verifying RTTL specifications}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Once the reachability graph is generated, the VERIFY procedures
listed below may be used to check RTTL specifications. The notation
$p, p_1, p_2, p_3, \cdots$ stands for state-formulas (atomic
properties of RTTL declared in the {\tt sample.sf} file).

\begin{description}

\item[Safety properties:] Two safety properties can be checked, viz.
invariance ($p_1 \implies \hn p_2$) and {\em unless} properties 
($p_1 \implies p_2 {\bf U} p_3$).

For safety properties, use the {\tt prop(sample,p,[[X,C,Y,Z],N])}
style in {\tt sample.sf} for specifying an atomic property $p$. The
variable {\tt N} is used to specify event occurrences whereas the
variables {\tt X,C,Y} and {\tt Z} are used to specify activity and
data values.

\begin{description}
\item[{\tt henceForth(sample,p1,p2,Answer,Location)}] --- is used
to check the invariance property $p_1\implies \hn p_2$. 

To check $\hn p$, invoke:\\ 
{\tt henceForth(sample,initial,p,Answer,Location)}.


\item[{\tt unless(sample,p1,p2,p3,Answer,Location})] --- is used to
check the property $p_1\implies p_2 {\bf\rm U} p_3$.

To check $p_1 {\bf\rm U} p_2$, invoke the VERIFY
procedure:\\
{\tt unless(sample,initial,p1,p2,Answer,Location)}.

\end{description}

\item[Bounded response and liveness properties:] The bounded response
time property ($p_1 \implies \ev_{[l,u]} p_2$), and the liveness
property ($p_1 \implies \ev p_2$) can be checked using the VERIFY
query {\tt rtrfRG2(sample,p1,p2,Lo,Hi)}. The {\tt rtrfRG2} name
stands for Real-Time Response First (occurrence of $p_2$ after
$p_1$) using a check of the RG2 graph.

Use the {\tt sf(sample, p, [X,C,Y,Z])} style in {\tt sample.sf} for
specifyingatomic properties such as  $p$ (or $p_1, p_2$). The next
transition variable, e.g. $({\rm\bf n} = {\tt g})$, cannot be used
for response or liveness properties in the current version of VERIFY.

\begin{description}
\item[{\tt rtrfRG2(sample,p1,p2,Lo,Hi)}] --- is used to check the
property given by the RTTL formula $p_1 \implies \ev_{[l,u]} p_2$. 

The {\tt rtrfRG2} query checks the minimal
and maximal times of the {\em first\/} occurrence of $p_2$ after
$p_1$. Thus, the property really being checked is: 
\[ p_1 \implies (\neg p_2 {\cal U}_{[l,u]} p2) \]
where ${\cal U}$ is the {\em until\/} operator, i.e. if $p_1$
becomes true, then eventually within $l$ to $u$ ticks $p_2$ must
occur, and $\neg p_2$ is true until then.
Note that
\begin{eqnarray*}
p_1 \implies (\neg p_2 {\cal U}_{[l,u]} p2)
&\equiv& p_1\implies \ev p_2 \mbox{~~~for some finite $l$ and $u$}\\
&\Implies& p_1 \implies \ev_{[l,u]} p_2
\end{eqnarray*}

The procedure {\tt rtrfRG2} either (a) returns finite values for
{\tt Lo} and {\tt Hi}, or (b) returns an uninstantiated value for
{\tt Lo} and {\tt Hi}.

In case (b), both $p_1 \implies \ev_{[l,u]} p_2$ and $p_1 \implies \ev
p_2$ are invalid.

In case (a), the liveness property $p_1 \implies \ev
p_2$ is valid. The real-time response property
$p_1 \implies \ev_{[l,u]} p_2$ is valid if
${\tt Lo} \leq l \leq u\leq {\tt Hi}$. The values returned for
{\tt Lo} and {\tt Hi} apply to the first occurrence of $p_2$ after
$p_1$.

\end{description}
\end{description}

\subsubsection{Checking safety properties S1 to S5, and S8}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Recall that safety properties (henceforth and unless) are checked with
reference to the {\tt prop} declarations in {\tt sample.sf}. For
example, to check property S5 below, the following atomic {\tt prop}
decalarations are made in {\tt sample.sf}:

\begin{verbatim}
prop(sample, 5, [[X,C,Y,Z], N]) :-
    N=b.
prop(sample, 6, [[X,C,Y,Z], N]) :-
    (C >= 5) ; (Y = 0).
prop(sample, 7, [[X,C,Y,Z], N]) :-
    N=e.
\end{verbatim}

\begin{verbatim}
%%% Checking S1
| ?- henceForth(sample, initial, 1, Answer, Location).
...
The present application of henceForth produced a true result.
The result holds for all the states tested.
Answer = true,
Location = all <Press CR>

%%% Checking S2
| ?- henceForth(sample, 3, 4, Answer, Location).
...
The present application of henceForth produced a true result.
The result holds for all the states tested.
Answer = true,
Location = all 

%%% Checking S3
| ?- henceForth(sample, initial, 2, Answer, Location).
...
The present application of henceForth produced a true result.
The result holds for all the states tested.
Answer = true,
Location = all

%%% Checking S4
| ?- henceForth(sample, initial, -3, Answer, Location).
...
The present application of henceForth produced a false result.
The result failed for State Number "5" with History Number "8"
via Transition "h" to State Number "3" with History Number "4".
The State Contents are:
                    [slow,5,5,-1]
Answer = false,
Location = [[5,8],[slow,5,5,-1],h,[3,4]]
%%% In the state 5-8, Z = -1 and N = h. Hence S5 is falsified
%%% in this state.
%%% Knowing the failing state can help the designer debug the TTM.
%%% Press ";" for additional failing states.

%%% Checking S5
| ?- unless(sample, 5, 6 ,7, A ,L).
...
Send results to sample.output file (type "y." or "n.") ? y.
sending results to sample.output file...
A = true,
L = all

%%% Checking deadlock freedom S8
| ?- henceForth(sample, initial, enabled, A, L)
   The present application of henceForth produced a false result.
   The result failed for State Number "1" with History Number "1".
   The State Contents are:

                    [off,0,0,1]



A = false,
L = [[1,1],[off,0,0,1]] ;


   The present application of henceForth produced a false result.
   The result failed for State Number "6" with History Number "1".
   The State Contents are:

                    [off,0,4,1]



A = false,
L = [[6,1],[off,0,4,1]] ;


   The present application of henceForth produced a true result.
   The result holds for all the states tested.


A = true,
L = all

%%% The TTM sample deadlocks at the above two states.

\end{verbatim}

All the above properties are valid except for S4 and S8.  VERIFY
produces a failing state for S4 and S8 (pressing ``;'' returns all the
other failing states). These failing states can help the designer
debug the TTM design.

\subsubsection{Checking real-time response properties S6 and S7}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Recall that real-time response and liveness properties must be checked
by declaring the atomic properties using {\tt sf} declarations in
{sample.sf}.

\small\begin{verbatim}
%%%% Checking property S6
| ?- rtrfRG2(sample, 3, 2, Lo, Hi).
...
Send results to sample.output file (type "y." or "n.") ? y.
sending results to sample.output file...
Lo = 1,
Hi = 2
| ?-
%%% Checking property S7
| ?- rtrfRG2(sample, 4, 3, Lo, Hi).
...
Send results to sample.output file (type "y." or "n.") ? y.
sending results to sample.output file...
Lo = _12771,
Hi = _12788
\end{verbatim}\normalsize

The property S7 is thus invalid. The file {\tt sample.output} contains
the failing legal trajectories.

\section{Composing TTMs}
%%%%%%%%%%%%%%%%%%%%%%%%

See \cite{Ost92a} for a process control example where:

\[ SUD = SENSOR \| FILTER \| ALARM \]

This example is stored in the directory {\tt examples/sensor}.

The three TTMs (sensor, filter and alarm) can be created individually
and the {\tt compose} command of VERIFY can be used to run them
together:

\small
\begin{verbatim}
| ?- compose([sensor,filter,alarm], sud).
...
There are variables in the TTMs to be  composed which are not
unique to a particular TTM.  Should all these variables be
considered to be shared variables?  Answering Y. will treat
all like variables as shared variables.  Answering N. will
show each non-unique variable and ask whether or not it
should be considered a shared variable. ( Y. / N. ) : Y.

The composed TTM will be found in the file - sud.ttm
yes
| ?-
\end{verbatim}\normalsize

The TTMs found in the directory {\tt examples/textbook-examples} are
the TTMs used in Chapter 7 of \cite{Ost89a}.

\section{Acknowledgements}
%%%%%%%%%%%%%%%%%%%%%%%%%%

John Dangov and Olaf von Breman wrote the original software as
part of an undergraduate project in the Department of Computer
Science at York University. Don Laws improved the eficiency of the
software and removed bugs that had crept into the original code.

\appendix

\section{The Prolog file {\tt sample.ttm}} \label{app:ttm}

\small\begin{verbatim}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                                                         %
%                                                                         %
%                 Quintus Prolog Code for TTM: "sample"                   %
%                                                                         %
%                                                                         %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%
%  Multifile and Dynamic declarations:
%
%
:- multifile map/3, type/3, initialcondition/2, en/3, h/4, lohi/4.
:- dynamic map/3, type/3, initialcondition/2, en/3, h/4, lohi/4.
%
%
%  Mapping and Types:
%
%
map(sample, [x,c,y,z], [X,C,Y,Z]) :-
        type(x, X),
        type(c, C),
        type(y, Y),
        type(z, Z). 
type(sample, x, X) :- 
        (X=fast; X=slow; X=idle; X=off). 
type(sample, c, C) :- 
        C >= 0. 
type(sample, y, Y) :- 
        Y >= 0. 
type(sample, z, Z) :- 
        Z >= 0; Z < 0. 
%
%
%  Initial Condition:
%
%
initialcondition(sample, [off, 1, 0, 1]). 
initialcondition(sample, [off, 0, 0, 1]). 
%
%
%  Enabling Conditions:
%
%
en(sample, tick, [X,C,Y,Z]). 
en(sample, a, [X,C,Y,Z]) :- 
        (X=off,
         C>0).
en(sample, b, [X,C,Y,Z]) :- 
        (X=idle,
         C>=2).
en(sample, d, [X,C,Y,Z]) :- 
        (X=idle,
         C<2).
en(sample, e, [X,C,Y,Z]) :- 
        (X=slow,
         (Y>=5,
          Z>0)).
en(sample, f, [X,C,Y,Z]) :- 
        (X=slow,
         (Z>0,
          Y=<5)).
en(sample, g, [X,C,Y,Z]) :- 
        (X=fast,
         Y<5).
en(sample, h, [X,C,Y,Z]) :- 
        X=slow.
%
%
%  Transformation Functions:
%
%
h(sample, tick, [X,C,Y,Z], [X,C,Y,Z]). 
h(sample, a, [X,C,Y,Z], [idle,Cnew,Y,Z]) :-
     Cnew is C+1.
h(sample, b, [X,C,Y,Z], [slow,Cnew,Ynew,Z]) :-
     Cnew is C+3,
     Ynew is 3+C.
h(sample, d, [X,C,Y,Z], [fast,C,Y,Z]). 
h(sample, e, [X,C,Y,Z], [fast,C,Ynew,Z]) :-
     Ynew is Y-1.
h(sample, f, [X,C,Y,Z], [off,Cnew,Y,Z]) :-
     Cnew is 0.
h(sample, g, [X,C,Y,Z], [off,Cnew,Y,Z]) :-
     Cnew is 0.
h(sample, h, [X,C,Y,Z], [slow,C,Y,Znew]) :-
     Znew is -Z.
%
%
%  Lower and Upper Bounds:
%
%
lohi(sample, tick, 0, infinity). 
lohi(sample, a, 0, infinity). 
lohi(sample, b, 1, 1). 
lohi(sample, d, 0, infinity). 
lohi(sample, e, 1, 2). 
lohi(sample, f, 2, 3). 
lohi(sample, g, 0, 0). 
lohi(sample, h, 1, 1). 

\end{verbatim}\normalsize


\section{The Prolog file {\tt sample.sf}} \label{app:sf}
\small\begin{verbatim}
:- multifile prop/3, sf/3.
:- dynamic prop/3, sf/3.

prop(sample, 1, [[X,C,Y,Z], N]) :-
     not ( X=fast , Y=3 ).
prop(sample, 2, [[X,C,Y,Z], N]) :-
    ( Z=1 ; N=h; isTick(N) ).
prop(sample, 3, [[X,C,Y,Z], N]) :-
    C=0.
prop(sample, 4, [[X,C,Y,Z], N]) :-
    isTick(N).
prop(sample, 5, [[X,C,Y,Z], N]) :-
    N=b.
prop(sample, 6, [[X,C,Y,Z], N]) :-
    (C >= 5) ; (Y = 0).
prop(sample, 7, [[X,C,Y,Z], N]) :-
    N=e.
prop(sample, 8, [[X,C,Y,Z], N]) :-
    Y>=4.
prop(sample, 9, [[X,C,Y,Z], N]) :-
    Y=4.
prop(sample, -1, [[X,C,Y,Z], N]) :-
     (Y=3);N=g.
prop(sample, -2, [[X,C,Y,Z], N]) :-
     (Y=3); isTick(N).
prop(sample, -3, [[X,C,Y,Z], N]) :-
     Z=1; isTick(N).
prop(sample, -4, [[X,C,Y,Z], N]) :-
    not ( Z=1; isTick(N) ).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%% state-formula "enabled" to check for deadlock
?-consult('sample.ttm').
prop(sample, enabled, [[X,C,Y,Z], N]) :-
       en(sample,Transition, [X,C,Y,Z]), not (Transition = tick).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

sf(sample, 1, [X,C,Y,Z]) :-
    X=slow.
sf(sample, 2, [X,C,Y,Z]) :-
    X=fast ; Z= -1.
sf(sample, 3, [X,C,Y,Z]) :-
    X=idle.
sf(sample, 4, [X,C,Y,Z]) :-
    X=off.

\end{verbatim}\normalsize




\section{Additional Notes}
\subsection{Files in different directories}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

In VERIFY routines such as {\tt rg2(sample)} the TTM {\tt sample} refers to a
file that is in the current directory. 

If the file is in a different directory, then the file name must be single
quoted, e.g:\\
{\tt rg2('./example/sample')}\\
{\tt restore('../verify')}


\subsection{Compiling, saving and restoring VERIFY}\label{app:compiling}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

To start Quintus Prolog (in an Emacs window)
\small\begin{verbatim}
unix prompt> % prolog +
Quintus Prolog Release 3.1.1 (Sun-4, SunOS 4.1)
Copyright (C) 1990, Quintus Corporation.  All rights reserved.
2100 Geng Road, Palo Alto, California U.S.A. (415) 813-3800
| ?
\end{verbatim}\normalsize

In order to compile {\tt verify.pl} to obtain a compiled version of the code
called {\tt verify}, the following procedure is invoked:
\small\begin{verbatim}
| ?- compile(newverify).
...
% verify.pl compiled in module user, 23.483 sec 193,596 bytes
yes
| ?- 
\end{verbatim}\normalsize

The state can now be saved as A QOF file.
\small\begin{verbatim}
| ?- save_program(verify, start).
% Saving QOF file ...
yes
| ?-
\end{verbatim}\normalsize
The second argument of {\tt save\_program}, i.e. {\tt start}, determines
which Prolog prdicate is called on entry into the saved state.


\section{Archiving the files}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Assuming all files are in a directory VERIFY, do

\begin{verbatim}
tar -cvf verify.tar VERIFY
compress verify.tar
\end{verbatim}

to create the archive file {\tt verify.tar.Z}. This file can then be
placed in {\tt ~ftp/AUTOMATE} on {\tt nexus}.

\nocite{Ost89a,Ost90b,OW90,Ost91a,Ost91b,Ost92b}

%\bibliography{paper}\bibliographystyle{alpha}

\begin{thebibliography}{Ost92b}

\bibitem[Ost89]{Ost89a}
J.S. Ostroff.
\newblock {\em Temporal Logic for Real-Time Systems}.
\newblock Advanced Software Development Series. Research Studies Press Limited
  (distributed by John Wiley and Sons), England, 1989.

\bibitem[Ost90a]{Ost90a}
J.S. Ostroff.
\newblock Deciding properties of timed transition models.
\newblock {\em IEEE Transactions on Parallel and Distributed Systems},
  1(2):170--183, April 1990.

\bibitem[Ost90b]{Ost90b}
J.S. Ostroff.
\newblock A logic for real-time discrete event processes.
\newblock {\em IEEE Control Systems Magzine}, June 1990.

\bibitem[Ost91a]{Ost91b}
J.S. Ostroff.
\newblock Constraint logic programming for reasoning about discrete event
  processes.
\newblock {\em The Journal of Logic Programming}, Volume II, numbers 3
and 4, October/November 1991.


\bibitem[Ost91b]{Ost91a}
J.S. Ostroff.
\newblock Systematic development of real-time discrete event systems.
\newblock In {\em Proceedings of the ECC91 European Control Conference}, pages
  522--533, Paris, France, July 1991. Hermes Press.

\bibitem[Ost92a]{Ost92b}
J.S. Ostroff.
\newblock Verification of safety critical systems using {TTM/RTTL}.
\newblock In {\em Proceedings of the REX Workshop 
`` Real-Time: Theory in Practice''},
LNCS 600, Springer-Verlag, 1992.
\newblock (In Press).

\bibitem[Ost92b]{Ost92a}
J.S. Ostroff.
\newblock A verifier for real-time properties.
\newblock {\em The Journal of Real-Time Systems}, 4, pages 5--35, 1992.

\bibitem[OW90]{OW90}
J.S. Ostroff and W.M. Wonham.
\newblock A framework for real-time discrete event control.
\newblock {\em IEEE Transactions on Automatic Control}, April 1990.

\end{thebibliography}



\end{document}