

                         Verus 0.9 - Reference Manual
                         ============================

Srgio Vale Aguiar Campos
March 1997


1 Overview
==========

Verus allows the formal specification and verification of real-time
and other time critical systems. It can also be applied to several
types of untimed software and hardware applications. The system being
verified is specified in the Verus language and then compiled into a
state-transition graph. Algorithms derived from symbolic model
checking are used to compute quantitative information about the model
[1]. A CTL symbolic model checker is also provided to assist in the
verification [2]. The Verus language has been especially designed to
allow a straightforward description of the temporal characteristics of
programs. The information produced allows the user to check the
temporal correctness of the model: schedulability of the tasks of the
system can be determined by computing their response time; reaction
times to events and several other parameters of the system can also be
analyzed by this method. This information provides insight into the
behavior of the system and in many cases it can help identify
inefficiencies and suggest optimizations to the design. The same
algorithms can then be used to analyze the performance of the modified
design. The evaluation of how the optimizations affect the design can
be done before the actual implementation. This can significantly
reduce development costs.


The Verus Language

The main goal of the Verus language is to allow engineers and
designers to describe real-time systems easily and efficiently. It is
an imperative language with a syntax resembling that of C. Special
primitives are provided to express of timing aspects such as
deadlines, priorities, and time delays. The available data types are
integer and boolean. Nondeterminism is supported, which allows partial
specifications to be described.

Note: Some of the special primitives are not available in the current
version.


CTL and RTCTL Model Checking

Computation Tree Logic, CTL, is the temporal logic used in our
verification system [3,4]. In Verus it is possible to verify
properties expressed as CTL formulas.  In CTL it is possible to
express properties such as "p will eventually occur", or "p will never
be asserted". However, it is not possible to express bounded
properties such as "p will occur in less than 10ms" directly. RTCTL
model checking overcomes this restriction by allowing bounds on all
CTL operators to be specified [5].  Verus can then be used to check
the correctness of the system using CTL, and time bounded properties
using RTCTL.


Quantitative Algorithms

Most verification algorithms assume that timing constraints are given
explicitly in some notation like temporal logic. Typically, the
designer provides a constraint on response time for some operation,
and the verifier automatically determines if it is satisfied or
not. Unfortunately, these techniques do not provide any information
about how much a system deviates from its expected performance,
although this information can be extremely useful in fine-tuning the
behavior of the system.

Verus uses algorithms that determine the minimum and maximum length of
all paths leading from a set of starting states to a set of final
states. It also uses algorithms that calculate the minimum and the
maximum number of times a specified condition can hold on a path from
a set of starting states to a set of final states [1].  Our algorithms
provide insight into how well a system works, rather than just
determining whether it works at all. They enable a designer to
determine the timing characteristics of a complex system given the
timing parameters of its components. This information is especially
useful in the early phases of system design, when it can be used to
establish how changes in a parameter affect the global behavior of the
system.


1.1 Example: A Producer/Consumer Program
----------------------------------------

This section provides an overview of the language by presenting a
simple real-time program. This program implements a solution for the
producer-consumer problem by bounding the time delays of its
processes. No synchronization is necessary if the time delays of
producer and consumer are defined properly. We start by declaring the
program global variables.

	1	  int p, c;
	2	  boolean produce, consume;

The code for the producer process is shown below. Variable p is a
pointer to the buffer in which data is stored. The producer
initializes its pointer p to 0 and the produce variable to false. It
then enters a nonterminating loop in which items are produced at a
certain rate. Line 8 introduces a time delay of 3 units, after which
an item will be produced. Line 9 marks the production of an item by
asserting produce. In line 10 the pointer is updated
appropriately. Line 11 makes sure that the event produce is
observed. It is needed because the state of a Verus program can only
be observed at wait statements. If a wait is not introduced in line
11, line 12 would cancel the effect of the assertion of produce before
it can be observed. This behavior is discussed in detail later.


	3	producer()
	4	{
	5	  p = 0;
	6	  produce = false;
	7	  while(true) {
	8	    wait(3);
	9	    produce = true;
	10	    p = p+1;
	11	    wait(1);
	12	    produce = false;
	13	  };
	14	}

                   Figure 1. Producer code


Wait Statements

An important feature of Verus is illustrated in line 8. In Verus time
passes only on wait statements. Lines 5, 6 and 7 execute in time zero
and time elapses only after the loop condition has been tested. This
feature allows a more accurate control of time, and eliminates the
possibility of implicit delays influencing the results of the
verification. It also generates models with fewer states, since
contiguous statements are collapsed into one transition. Notice that
this significantly affects the behavior of the program. For example, a
block of code not containing the wait statement executes atomically.

Note: Line 8 introduces a 3 time unit wait in the program. The current
version of Verus only supports unit waits. Line 8 must be replaced by
three unit waits in the actual program.


Nondeterminism

To illustrate another characteristic of Verus, let's assume that the
producer is not required to actually produce an item after 3 time
units, but may instead leave the value of p unchanged. This can be
modelled in Verus by changing line 10 to:

	10	    p = select{p, p+1};

The select statement introduces a nondeterministic choice in the
program. The value of p after executing select can be either p or p+1
(addition in Verus is defined modulo the maximum value for the
variable). These choices can characterize the fact that the producer
may produce an item, but it may also not produce it. This way we can
model both possibilities without having to specify all the details
that are actually needed to decide between these two options. Besides
hiding unnecessary details, nondeterminism can be used to verify
partial specifications. Whenever the value of a variable hasn't been
determined by the design, nondeterministic con- structs can specify
all possible values the variable could take. This approximates the
behavior of the actual system by exploring all possibilities. As the
design process evolves, the values can be restricted until the correct
behavior is determined.  Nondeterminism encourages the use of
automated verification in earlier phases of the design. Components of
the system can be validated before all modules have been specified. In
this way errors can be uncovered before propagating to components
added later in the design.


	15	consumer()
	16	{
	17	  c = 0;
	18	  consume = false;
	19	  while (true) {
	20	    wait(1);
	21	    if (p != c) {
	22	      wait(1);
	23	      consume = true;
	24	      c = c + 1;
	25	      wait(1);
	26	      consume = false;
	27	    };
	28	  };
	29	}

                      Figure 2. Consumer code


The consumer process is very similar to the producer. The basic
differences are that it waits for less time before consuming, and that
it only consumes if p and c have different values (p == c signals an
empty buffer). Notice that the producer does not check if the buffer
is full before inserting another item. The time delays of both
processes guarantee that an overflow will never occur.


Process Instantiation and Communication

Multiple processes can be defined in Verus. Each function defined is
instantiated as a concurrent process. Function declaration
instantiates concurrent processes that execute the code for that
function.

Processes communicate using global variables. Global variables can be
read and written by any process at any time. Racing conditions occur
when multiple processes write conflicting values simultaneously to the
same variable. They are identified by the verifier as deadend states
(see section 2.1, "Local and Global variables" on page 7), and
counterexamples are printed that show how such states can be reached.

Process instantiation in Verus follows a synchronous model. All
processes execute in lock step, with one step in any process
corresponding to one step in the other processes.


Specifications

Specifications follow the code as seen below. They must be the at the
end of the program, and must be global, that is, they must not be
inside any process. The specifications below compute the minimum and
maximum time between producing an item and consuming it, as well as
checking that a produce is always followed by a consume.


	30	spec MIN[produce, consume];
	31	     MAX[produce, consume];
	32	     AG(produce -> AF consume);

                     Figure 3. Producer/consumer main function


2 Syntax and Semantics
======================

This section describes the syntax of Verus in detail. The description
of the semantics presented in this document is very informal and is
intended only to provide an intuition about how Verus programs
behave. A more formal treatment of the semantics of Verus can be found
in [1].

The syntax presented is abstract and unnecessary details have been
omitted for clarity. In particular, lists are not formally defined.
The name of an entity followed by the keyword _list is used to specify
a list of entities of the type given. For example a list of
identifiers is denoted simply by identifier_list. Unless otherwise
specified, all lists are separated by spaces, tabs or newlines.


2.1 Variables in Verus
----------------------

Variables in Verus are declared similarly to C:

declaration ::=	type_spec identifier_list ; |
                extern type_spec identifier_list ;
type_spec ::= boolean | int

Variables can be boolean or fixed-width integers. This guarantees that
the model will be finite-state. The default integer width is 8
bits. The default is changed as a compile time option (by changing the
value of the constant DEFAULT_INT_SIZE in integer.h). Integer
variables are internally encoded in binary and represented by an array
of boolean variables.


Internal and External Variables

There are two types of variables in Verus, internal and external. In
both cases, there is no default value for variables in Verus. Unless
assigned a specific value, the value of a variable is chosen
nondeterministically from all possible values (true or false for
booleans and 0..2width-1 for integers). The two types differ, however,
regarding the rules that control when their value can change. The
value of an internal variable changes only when assignments are
executed. External variables on the other hand model the interaction
of the model with the environment. They correspond to inputs from the
outside world, and the program has no control over their
value. Assignments to external variables are not allowed and their
value can change nondeterministically at any transition of the
model. The declaration of external variables is preceded by the extern
keyword. Internal variables are declared without this keyword.


Local and Global variables

Global variables can be read and written by any process. A special
technique called BDD marking is used to keep track of which process is
writing to the variable at any time. Race conditions may occur if two
or more processes write to the variable at the same time. Verus
identifies these conditions as states without outgoing transition.
This is because race conditions create a conflict in the transition
relation, eliminating transitions from that state. Verus checks
automatically for deadend states, and a counterexample showing how
this can happen is printed when race conditions are identified.

Local variables can only be read and written by the process in which
they are declared.

Note: In the current version local variables cannot be passed as
parameters to other processes. Shared variables must be global, even
if they are written by only one process.

Any combination of local/global and internal/external variables is
allowed.  Notice, however, that the external characteristic of
variables is always global, i.e., they represent events in the
environment that are not modelled in the system.  There is no
difference in the behavior of global or local external variables,
except for scoping.


Wait Counters

A special variable for each process is automatically created by the
Verus compiler to keep track of control flow information, the wait
counter _wc. The variable name._wc has the value n iff the execution
of process name is at the nth wait statement of process name in the
source code. This variable can be used in specifications to verify
properties of the control flow of the program. However, no assignments
are allowed to wait counters.


2.2 Verus Statements
--------------------

The basic types of statements implemented in Verus are assignments,
conditionals and loops. It is possible to write any Verus program
using only these types of statements. More complex constructs can be
implemented by using combinations of the basic ones.

statement ::= compound_statement |
              expression_statement |
              selection_statement |
              iteration_statement |
              wait_statement
compound_statement ::= { statement_list }

Assignments and Conditionals

expression_statement ::= ; | assignment_expr ;
selection_statement ::= if ( expr ) statement else statement |
                        if ( expr ) statement

Expression and selection statements are self-explanatory.


Wait Statements 

wait_statement ::= wait (1)

Note: In the current version of Verus longer waits have to be modelled
by a sequence of unit waits.

Wait statements determine how time passes in Verus: Time only passes
when a wait statement is executed. The execution of statements between
two waits occurs in time zero. As a consequence, the state of the
program can only be observed by other processes when execution reaches
the next wait. However, assignments take effect immediately. For
example, in the program fragment below the value of b in line 6 is 1:


	1	a = 0;
	2	wait(1);
	3	a = 1;
	4	b = a;
	5	a = 0;
	6	wait(1);

                    Figure 4. The effects of assignments


Notice that the zero time execution of non-wait statements may have
non intuitive effects. For example, in the example above even though
the value of b is set to 1 because of the value of a, the fact that a
has become 1 is never observed by other processes because there is no
wait statement before a changes value again.


Loops

iteration_statement ::= while ( expr ) statement

Another non intuitive behavior appears with while statements. The
behavior of a program fragment without waits cannot be observed. In
the same way, the behavior of a while loop without waits cannot be
observed. Even worse, if the while loop allows for an unbounded number
of iterations, this infinite behavior also cannot be observed.
Consequently, the program reaches a deadend state since its behavior
can no longer be seen. The last state that can be observed is at the
wait just before the loop. Because of this all Verus loops must
execute a wait at least once. Unbounded loops without waits are
identified by the compiler as a deadend state. A counterexample is
printed to show how it can be reached.

Note: In the current version there no explicit message about loops
without waits. However such situations are identified as deadend
states. In some rare cases it is also possible that the compiler does
not terminate compila- tion because of this problem. If any of these
behaviors occur, the user is advised to look for potential paths
through loops in which no wait is exe- cuted.


2.3 Verus Expressions
---------------------

assignment_expression ::= identifier = expression | 
                          identifier = select { expression_list }

expression ::= boolean_expression | 
               relation_expression | 
               integer_expression

boolean_expression ::= expression || expression | 
                       expression && expression | 
                       ! expression | 
                       primary_expression

primary_expression ::= ( expression ) |
                       identifier |
                       constant

Only boolean expressions are defined as primitives. Integers variables
and operations are defined in terms of booleans using binary
encoding. The select expression allows for a nondeterministic choice
of values. The value returned is one of the possible values listed,
chosen nondeterministically. Expression lists are separated by commas.

relation_expression ::= expression = = expression |
                        expression != expression |
                        expression < expression |
                        expression > expression |
                        expression <= expression |
                        expression >= expression 

integer_expression ::=  expression + expression |
                        expression - expression

These expressions are translated by the Verus compiler into boolean
operations.


2.4 Functions and Processes
---------------------------

function_definition ::=
	identifier ( identifier_list ) declaration_list compound_statement

Identifier lists are separated by commas.

Functions are instantiated as processes, and correspond to the basic
execution unit of Verus programs. Each function is instantiated as a
concurrent process. Processes execute synchronously.


2.5 Specifications
------------------


Quantitative Expressions

spec ::= ctl_formula ; |
         min (expression, expression); | 
         max (expression, expression); |
         mincount(expression, expression, expression); |
         maxcount(expression, expression, expression);

Specifications can be CTL formulas or quantitative expressions. The
min/max specifications determine the minimum and maximum lengths of
all paths between its first and second arguments. The
mincount/maxcount specifications determine the minimum and maximum
number of occurrences of the middle argument on all paths between the
first and last arguments.


CTL Formulas

ctl_formula ::= expression |
                EX expression |
                AX expression |
                EF time_bounds expression |
                AF time_bounds expression |
                EG time_bounds expression |
                AG time_bounds expression |
                E[expression U time_bounds expression] |
                A[expression U time_bounds expression]

time_bounds ::= null | constant..constant

If time bounds are specified, then RTCTL model checking is performed,
otherwise standard CTL model checking is used. There is no fairness
for CTL formulas in Verus. However, this is not a major restriction
because only synchronous composition of processes is allowed. Fairness
is significantly more important for non synchronous systems.

Note: The current version of the model checker does not produce
counterexamples. It does allow a more restricted counterexample
option, as described next.


Example Paths

Another type of specification is introduced in Verus, to provide a
restricted counterexample facility. If a specification has the form
EXAMPLE ctl_formula; it will produce a counterexample from an initial
state to a state in which ctl_formula holds.

3 Runtime Options
=================

There are many runtime options that affect the behavior of the
verifier significantly. The user is advised to learn and experiment
with them because it is very uncommon that a non trivial example can
be verified without any of these options.


3.1 Dynamic Variable Reordering: -r
-----------------------------------

The -r flag will turn on the dynamic variable reordering feature of
the BDD library. Reordering variables is essential in virtually all
interesting models, as it very often means the difference between
being able to verify the system or not.  Because reordering can take a
long time, this flag is better used to generate an ordering file
(explained below). Reordering in Verus is applied after compiling the
source program, but before creating the global transition relation. It
is turned off before verification starts.


3.2 Ordering Files: -i <filename> and -o <filename>
---------------------------------------------------

By using `-o filename' it is possible to save the current BDD order in
the file filename. This file will contain all BDD variables created by
the compiler in the order in which they have been used at the time the
-o option was used. The file can be edited and manually reordered.
Even though not frequently used, manual reordering can sometimes be
very useful. The `-i filename' option reads the ordering filename and
uses that order in the verification.


3.3 Lazy Parallel Composition: -l
---------------------------------

For each function compiled Verus creates a transition relation that
determines transitions between states in the corresponding
process. After all functions are compiled it is necessary to compose
all individual transition relations into a global transition relation
that corresponds to the behavior of the global system. Verus provides
two different ways in which this can be done.

The default behavior is to apply the standard parallel composition
algorithm to create the global transition relation.

The -l option applies the lazy parallel composition algorithm
described in [1].

There are applications for each option. The standard composition
algorithm generates a global transition relation by conjuncting all
functions. However, the size of the BDD representing this relation
grows exponentially with the number of processes. This is, in fact,
the major cause for state explosion during verification. The other
option does not create the global transition relation, but instead
uses the individual transition relations for each function during
verification. This options typically use less memory, but each step in
the verification is more complex since it has to handle multiple
transition relations instead of a single one. The best choice of
option for each system can only be determined case by case, and most
easily by experimentation.


3.4 BDD Cache Size: -c <cachesize>
----------------------------------

One of the critical aspects of using BDDs for verification is the use
of a BDD cache. If some operation is performed more than once, the
second time can be much faster if the result has been stored in the
cache the first time. Verus implements an internal cache to take
advantage of this fact. Many intermediate BDDs are created during
compilation and verification. When these BDDs are no longer needed,
they are deleted. But Verus does not delete them immediately. Instead,
they are stored in the cache in the hope of being reused by later
operations. When the cache is full it is flushed by deleting all of
its contents.

By changing the size of the cache the user can adjust, to some extent,
the amount of memory and time used for verification. A larger cache
will speed up verification (more nodes are reused), but more memory
will be used. A smaller cache has the opposite effect. The default
size of the cache is 500 BDD nodes, and only experimentation can
determine what is the best size for each application.


3.5 Verbose Mode: -v, -V
------------------------

Two verbose modes are provided. With -v each iteration of the verifier
is shown with the size and number of states in the current set of
states. With -V one state of the current set of states being
considered will be printed.


3.6 Short Counterexamples: -s
-----------------------------

A counterexample is a sequence of states, and each state is an
assignment of values to the variables. If the number of variables in
the model is large, the output becomes cluttered and difficult to
follow. The short counterexample option is used to print only the
values of the wait counters of each process. This allows the user to
follow the program without printing the value of all variables.


4 BDDs and The State Explosion Problem
--------------------------------------

The behavior of BDDs is highly dependent on the variable ordering
used. The size of the BDD for a given function can vary from linear to
exponential in the number of variables depending on the variable
ordering used. Because of this it is vital to be able to determine a
good variable ordering during verification. Unfortunately, computing
the optimal variable ordering is an exponential problem. There are,
however, several techniques for determining good variable orderings
that work extremely well in practice. Some of these techniques are
discussed in this section.


Dynamic Variable Reordering and its Limitations

Verus uses the algorithm implemented in the BDD library for
automatically reordering variables. The algorithm basically tries many
different positions for each variable until it finds the ordering
which generates the smaller number of BDD nodes. It does not find the
optimal ordering, only a better ordering than the initial one. Because
of this, an efficient approach to reordering is to apply the algorithm
multiple times reducing the number of BDD nodes generated at each
step. This is the approach taken by Verus. Once the number of nodes
does not change reordering stops and the verification starts.

The dynamic reordering algorithm works very well in practice, but it
has some inherent limitations. An important one originates from the
fact that the algorithm changes the position of one single variable at
a time. Sometimes many variables have to be changed at the same time
to achieve better results, but this cannot be done directly by the
reordering algorithm.


Incremental Reordering

The quality of the variable ordering determined by the dynamic
reordering algorithm depends on several factors, the most significant
one being the initial ordering used. If an extremely inefficient
ordering is used initially, the algorithm is frequently unable to
improve it significantly. Moreover, the algorithm works bet- ter on
smaller models, since there are not many configurations to be
tried. These two facts lead to a very efficient way of applying
dynamic reordering, incrementally.

Ideally, reordering should be applied very often during model
construction. If the model has few variables, the reordering algorithm
is usually able to find a good ordering, regardless of the initial
ordering. Once a good ordering is found, it is easier to improve on
it. If, on the other hand, reordering is only applied at the end, the
initial ordering is likely to be inefficient, and the final one will
probably be as well.

In some cases it is not possible to apply reordering during the coding
phase, for example if the code has already been written when
verification starts. In this case an alternative approach is to
"disable" parts of the code by commenting out complex expressions and
data structures. After disabling most of the code it is possible to
construct a small model and to perform reordering on it. Once an
initial ordering is found, we can incrementally "enable" the code
again and apply reordering on the intermediate results.


Manual Reordering

In most cases dynamic reordering is sufficient for
verification. However, it may be necessary to use manual reordering
once in a while, mostly to overcome problems with the dynamic
reordering algorithm. Manual reordering is mostly a trial-and-error
process but it can improve the ordering significantly. There are some
factors that must be kept in mind while reordering variables:

 Control Variables First: Control variables should be put before
  variables whose value depend on them in the ordering file. This is
  one of the simplest yet more efficient reordering heuristics.

 Variable Friendliness: It is often the case that the value of some
  variable in a program is directly dependent on the value of another
  one. The most common example is the variables that determine the
  value of program variables in the current and in the next state. The
  value in the next state is usually strongly related to the value in
  the current state. These variables should be kept together in the
  variable ordering.

 Variable Clustering: It is often the case that during manual
  reordering we notice that some variables should be kept together in
  the ordering. In this case we can speed up the reordering process
  without sacrificing BDD size by not introducing any more variables
  between them. This takes advantage of their interdependency and at
  the same time it minimizes the number of slots to try other
  variables.

 Rules are meant to be Broken: These rules work well in practice, but
  they must not be followed blindly. Sometimes non intuitive changes
  can have significant effects. It does pay off to break the rules
  from time to time and try something different, such as simply moving
  clusters of variables at random.

 Patience: This is probably the most important rule. Good orderings
  usually are not found easily, and spending time reordering is very
  beneficial.


5 References
============

[1] Srgio Campos. A Quantitative Approach to the Formal Verification
of Real-Time Systems. Ph.D. thesis, SCS, Carnegie Mellon University,
1996.

[2] J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and
J. Hwang. Symbolic model checking: 1020 states and beyond. In
Proceedings of the 5th Symposium on Logics in Computer Science, 1990.

[3] E. M. Clarke and E. A. Emerson. Synthesis of synchronization
skeletons for branching time temporal logic. In Logic of Programs:
Workshop, Yorktown Heights, NY, May 1981. LNCS 131, Springer-Verlag,
1981.

[4] E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic
verification of finite-state concurrent systems using temporal logic
specifications. ACM TOPLAS, 8(2):244-263, 1986.

[5] E. A. Emerson, A. K. Mok, A. P. Sistla, and
J. Srinivasan. Quantitative temporal reasoning. In Lecture Notes in
Computer Science, Computer-Aided Verification. Springer-Verlag,
1990.


Appendices


A Compiling Verus
=================

Verus has been originally compiled under Linux. Using a similar setup
simplifies installation by avoiding most compatibility problems.

In order to compile Verus, some Unix utilities are used, mainly gcc,
lex, yacc and make. Incompatibilities may arise from using different
programs. While gcc and make are usually trouble free, lex and yacc
may cause problems. It seems that in particular lex is very sensitive
to different versions. Whenever possible the use of flex (linux
version of lex) and bison (linux version of yacc) is recommended.

Verus uses the BDD library that is distributed with it. The BDD
library must be installed before compiling Verus.

The default environment in which Verus is compiled maintains the
source files in the directory ~/src/verus, and the object files in
directory ~/obj/verus. If the default environment is used, typing
mk<enter> should suffice to compile it.  If a different directory
structure is used the makefile must be changed.

B Special Timing Constructs
===========================

The Verus language provides special constructs to allow a
straightforward description of the timing characteristics of the
real-time system being verified. However, these constructs are not
supported by the current version. They are, however, simple to
manually translate to the supported subset of the language. This
section describes these constructs and how they can be used.


Periodic Execution

To illustrate how the special constructs can be used, we discuss some
extensions to the producer/consumer program described previously. The
first extension comes from realizing that both processes will always
execute, even when no data exists. For example, even if the producer
does not generate items, the consumer will execute. This can be
avoided using periodic execution, where execution is scheduled at
specific points in time. It can be specified in Verus very easily.
The producer process can be made into a periodic process executing
once every 10 time units as seen in figure 5.

The periodic statement has four parameters, the last being the code
that will be executed periodically. The first parameter is the
start_time, which specifies how many time units the periodic code will
idle before starting its execution for the first time. In this example
it will start immediately. The second parameter is the period. In this
case the statements following periodic will execute once every 10 time
units. The third parameter defines a deadline. It states that the
execution must finish in less than 10 time units or an exception will
be raised (exception handling is discussed below). Execution may take
longer than the sum of the waits because of synchronization with other
processes.


	1	producer()
	2	{
	3	  boolean produce;
	4	
	5	  p = 0;
	6	  produce = false;
	7	  periodic(0, 10, 10) {
	8	    wait(3);
	9	    produce = true;
	10	    p = p+1;
	11	    wait(1);
	12	    produce = false;
	13	  };
	14	}

                        Figure 5. Periodic producer


Deadlines

Verus also allows the definition of deadlines independent of
periodicity. For example, we can specify that producer will be an
aperiodic process, but that it must finish each iteration in less than
10 time units:


	1	producer()
	2	{
	3	  boolean produce;
	4	
	5	  p = 0;
	6	  produce = false;
	7	  while(true) {
	8	    deadline(10) {
	9	      wait(3);
	10	      produce = true;
	11	      p = p+1;
	12	      wait(1);
	13	      produce = false;
	14	    };
	15	  };
	16	}

                        Figure 6. Aperiodic producer


Exceptions

Exception handling is used to control abnormal situations. The only
exception currently defined in Verus is a missed deadline. It occurs
when the code inside a deadline or a periodic statement does not
finish within the specified time.  An exception handler must be
specified for the exception to take effect. If no exception handlers
are defined, the exception is ignored. Whenever a deadline is missed
the code designated as handler is executed. After the execution of the
exception handler the rest of the code inside the deadline scope is
ignored. Control is then passed to the statement following the
deadline statement. This could be the next instantiation of a periodic
process when the exception occurs inside a periodic statement or the
code after a deadline statement.


	1	producer()
	2	{
	3	  boolean produce;
	4	
	5	  handler {
	6	    error = 1;
	7	  } for {
	8	    p = 0;
	9	    produce = false;
	10	    periodic(0, 10, 10) {
	11	      wait(3);
	12	      produce = true;
	13	      p = p+1;
	14	      wait(1);
	15	      produce = false;
	16	    };
	17	  };
	18	}

                       Figure 7. Exception handling


Figure 7 shows the typical exception handling mechanism. Whenever a
deadline is missed an error flag is asserted. The verification
procedure can then check to see if the error condition is reachable.
In some other applications, however, a different behavior may be the
desired one. For example, a multimedia program might choose to ignore
some image frame that hasn't arrived, provided the last n arrived.  An
exception handler to model this behavior can be easily written:
whenever an exception occurs, the handler would record the number of
the frame missed. If the current missed frame is at least n frames
apart from the previous one, no error would be issued. Otherwise an
error condition would be asserted.


Translating Timing Constructs - Deadline

The deadline statement is translated into the Verus core language by
creating an integer variable timer. At the deadline keyword an
assignment timer = 0 is inserted. Within the scope of the deadline,
each wait(1) statement is preceded by timer = timer + 1; and by a
check if (timer >= deadline) error_code, where the exception handler
defines error_code.


Translating Timing Constructs - Periodic

The periodic statement is handled in a similar way. The difference is
that an infinite loop is inserted enclosing the periodic statement,
and once the periodic statement has finished executing, a loop is
inserted to enforce the periodicity:

		while (timer < period) {
		  timer = timer + 1;
		  wait(1);
		};

A similar loop is inserted before the main loop at the beginning of
the periodic statement to account for the initial offset.


Translating Timing Constructs - Exception Handling

The first compound statement in the statement is the exception
handler, and the second is the scope of the handler. The exception
handling statement handler S1 for S2 is translated by substituting the
error_code created by deadline statements in S2 for: S1 else {. The
compound statement S1 is executed in case of a missed deadline, and
the else clause guarantees that the rest of the deadline statement is
skipped in case of a missed deadline. The { after the else is closed
at the end of the deadline statement.

For example, the periodic producer described in the previous chapter
is translated into the core language as seen below:


	1	producer()
	2	{
	3	  boolean produce;
	4	  int timer;
	5	
	6	  p = 0;
	7	  produce = false;
	8	  while (true) {
	9	    timer = 0;
	10	    timer = timer + 3;
	11	    if (timer > 10) {
	12	      error = 1;
	13	    } else {
	14	      wait(3);
	15	      produce = true;
	16	      p = p+1;
	17	      timer = timer + 1;
	18	      if (timer > 10) {
	19	        error = 1;
	20	      } else {
	21	        wait(1);
	22	        produce = false;
	23	      };
	24	    };
	25	    while (timer < 10) {
	26	      timer = timer + 1;
	27	      wait(1);
	28	    };
	29	  };
	30	}

               Figure 8. Periodic producer in the core language
