A graphical interval logic for specifying concurrent systems.
This article describes a graphical interval logic that is the foundation of a tool set supporting formal specification and verification of concurrent software systems. Experience has shown that most software engineers find standard temporal logics difficult to understand and use. The objective of this article is to enable software engineers to specify and reason about temporal properties of concurrent systems more easily by providing them with a logic that has an intuitive graphical representation and with tools that support its use. To illustrate the use of the graphical logic, the article provides some specifications for an elevator system and proves several properties of the specifications. The article also describes the tool set and the implementation.
Introduction
One of the great challenges facing today's software engineers is the development of correct programs
for real applications. Recent advances in hardware reliability and fault tolerance technology can
assure extremely low hardware failure rates for devices. Unfortunately, technologies for digital
hardware design and software engineering have not matched this advance. The use of computers
in many critical applications is now primarily limited by the reliability of system designs and
implementations.
Research partially supported by NSF grant CCR-9014382 with cooperation from DARPA. An early version of the
paper was presented at 14th Inter. Conf. Software Engineering, May 1992 (Institution of Engineers Australia, IEEE
Computer Society, Association of Computing Machinery, Institution of Radio and Electronic Engineers Australia, and
Australian Computer Society). Copyright 1995 c
by ACM, Inc. Permission to copy and distribute this document
is hereby granted provided that this notice is retained on all copies, that copies are not altered, and that ACM is
credited when the material is used to form other copyright policies
The most critical real applications often involve concurrency, which increases the difficulty of
system development and validation. Modern methods of structured programming, which are quite
effective for sequential programs, are notoriously inadequate for concurrent ones. Moreover, the
nondeterminism inherent in applications that involve concurrency and the reactive character of
those applications makes them hard to test. Aggravating these problems is the need to explore
large spaces of possible executions, which grow exponentially with the number of independent
threads of control.
Formal methods for specifying and verifying systems can, in principle, offer a greater assurance
of correctness than informal design/code checks or testing. Formal verification methods can demonstrate
that a high-level design meets formally specified correctness requirements, thereby reducing
the risk that faulty designs will be used as the basis for system development. Formal specifications
are valuable for defining interfaces between independently developed software modules and for
establishing software and interface standards. Because they provide a succinct and unambiguous
statement of system requirements, formal specifications can potentially be analyzed for consistency,
a particularly difficult and important problem for concurrent systems. Formal specifications can
also be used during the selection of test data to suggest behaviors that should be tested and, later,
to determine whether the execution of a test case is correct or erroneous. Thus, system developers
can use formal specifications throughout the system lifecycle to guide development, maintenance
and enhancement.
In practice, however, system developers seldom make significant use of formal specification and
verification methods. We believe that this is due, in large part, to the reliance of those methods
on mathematical formalisms that are difficult to understand and to use. Formal specification and
analysis methods must be made accessible to system designers and software engineers if they are to
be used in the development of real world systems. Users must be able to express the properties of
the systems about which they wish to reason as naturally as possible and to confirm mechanically
that the specifications, designs, testing criteria and sample executions have the required properties.
Temporal logics [3, 20, 22, 34] are well-suited for specifying temporal properties of concurrent
systems. Experience has shown, however, that specifications of even moderate-sized systems are
too complex to be readily understood. This complexity stems chiefly from the need to establish
the temporal context within which properties, such as bounded liveness and invariance, must hold.
Interval logics [12,33] address this problem by defining temporal intervals to represent such contexts.
For example, to express the requirement that a process that releases a lock on a database must
signal that it intends to enter the database before obtaining a new lock, an interval might be used
to represent the activity of the system from the time that the process releases the lock until it
acquires a new one; the process would then be required to signal its intension within the restricted
context represented by the interval (bounded liveness).
Stylized pictures often show complex timing relationships and dependencies more clearly than
linear textual representations of the same information. Such diagrams correspond more closely to
common conceptualizations than does linear text. Software engineers often draw timing diagrams,
like those used to denote signal levels in hardware designs, when describing and reasoning about
properties of systems. Even logicians who are fluent in temporal logic find timing diagrams helpful
to explain the meanings of temporal logic formulas and to motivate lines of reasoning (see for
example [7]). However, in the absence of a formal semantics, timing diagrams cannot be used for
rigorous analysis of system properties. Pictorial documentation is typically ad hoc and liable to
ambiguous interpretation.
This paper describes a visual temporal logic in which formulas resemble the informal timing
diagrams familiar to designers of hardware systems and to software engineers. Graphical Interval
Logic (GIL) has a formal model-theoretic semantics and is as expressive as propositional temporal
logic with Until and without Next [28]. It thus provides an intuitive and natural visual notation
in which to express system specifications without sacrificing the benefits of a formal notation. A
visual editor allows GIL specifications to be easily constructed and to be stored in and retrieved
from files. The editor also provides a visual interface to a proof checker and model generator, which
permit verification of temporal inferences.
The paper first provides an overview of GIL in Section 2. It then presents sample specifications
for an elevator system in Section 3 and shows, in Section 4, how a designer uses the specifications to
reason about properties of the system. Section 5 describes the GIL toolset and Section 6 provides
an overview of the implementation. Related work is discussed in Section 7, with conclusions and
future work presented in Section 8. The appendix provides a model-theoretic semantics for the
logic.
Graphical Interval Logic
When reasoning about temporal properties exhibited by a concurrent system during a computation,
it is convenient to regard the system as passing through a sequence of states. To model a non-terminating
computation, the state sequence must be infinite. A terminating computation can
likewise be modeled with an infinite state sequence by repeating, or stuttering, the final state. This
permits a concurrent system to be identified with the set of infinite state sequences that represent its
potential computations. GIL specifications for a system describe properties of legal state sequences.
That is, the specifications must hold at the first state of every infinite state sequence that represents
a computation of the system. We adopt a total order model of computation, rather than a partial
order model, which has some advantages for representing causality in concurrent systems [27],
because total orders are more readily abstracted into meaningful 'intervals' that can be represented
pictorially at an appropriately high level.
A GIL formula is evaluated at a state in an infinite sequence of states. Infinite state sequences,
therefore, provide the contexts within which formulas are evaluated. A formula that holds at a
state in a context describes a property of the state's future within the context, or of the infinite
tail sequence that begins with the state and extends through the end of the context. A reflexive
interpretation of the future, in which the future includes the present, allows a semantics that is
insensitive to finite stuttering. This facilitates the use of hierarchical abstraction and refinement
while reasoning about concurrency [19].
Intervals permit the specification of contexts within which properties hold. We denote an
interval by a left-closed right-open line segment: ) . An interval thus shows the individual
states in a context as points on a line segment, with the horizontal dimension showing progression
through the context (time progresses from left to right). As suggested by the representation, every
interval has an initial point (state). However, since contexts are infinite, we do not regard an
interval as having a final point.
Interval formulas are the heart of the graphical interval logic. The basic interval formula asserts
that a formula holds at the first state of a designated context (interval). Derived operators assert
that a formula holds at every point in a context or at some arbitrary point in a context. GIL
therefore also provides the usual temporal Eventually and Henceforth operators.
The logic provides two search primitives for use in specifying intervals.
ffl Search to a target formula f , represented r
f
ffl Search to the right end of the context, represented r
A search to a target formula locates the first future point at which the target holds. The dot
represents the point at which the search starts. The search fails if the target does not hold at
any future point (inclusive of the present) in the context. A search to the right end of the context
permits the specification of a tail interval.
Searches can be composed sequentially, with each successive search starting from the point, if
any, located by the previous search. For example,
f
locates the first point at which f holds and then, beginning from this point, locates the next point
at which g holds. We allow the shorthand notation r
when the target f of the first search
is a state formula, which does not involve any temporal operators. Because this shorthand produces
more compact formulas, we use it extensively in the examples below. 1 The search r
f
is
equivalent to r , provided that f holds at some future point; however, if the search r
f
fails, then r
f
also fails. A tail search, when it appears, must be the last search in a search
pattern.
The extent of an interval is specified by means of a pair of search patterns, which designate
searches for locating the left and right ends of the interval. Both searches begin from the same
point. We therefore draw them one beneath the other, with their start points horizontally aligned.
The interval determined by the searches is drawn directly beneath the searches, its left end horizontally
aligned with the point located by the first search pattern and its right end horizontally
aligned with the point located by the second search pattern. For example:
f
1 As a result, the examples are slightly less general than they might be, since a sequence of searches cannot always
be drawn on the same line. However, they are easily converted into more general examples by drawing each primitive
search on a new line.
The interval starts at the point located by the search for its left end and extends up to, but does
not include, the point located by the search for its right end. The above diagram thus represents
the interval that starts with the first point at which f holds and ends just prior to the first point at
which g holds. The interval cannot be constructed if either search fails or if the interval is empty
(i.e. the point specified by the first search pattern does not precede that specified by the second
search pattern).

Figure

conventions that simplify the representation of several common types of
intervals. The first abbreviation, in which a single search pattern specifies the extent of an interval,
is permitted when the search for the interval's left end is a prefix of the search for its right end.
Thus, the interval in the first example begins with the first point at which f holds and extends up
to, but does not include, the next point at which g holds. The interval cannot be constructed if f
does not hold at any future point, if g does not hold at any point in the future of the first point at
which f holds, or if g holds at the point located by the search to f .
The second example in Figure 1 is a special case of the first, in which the target of the first
search is true. A search to true succeeds immediately, locating the point at which the search
begins. The interval in the second example thus begins with the point at which the specification
is evaluated and extends up to the next point (exclusive) at which f holds. The interval cannot be
constructed if f does not hold at any future point or if f holds at the present point. Such intervals
are used to specify finite prefixes of larger contexts.
The triangle 4 in the third example in Figure 1 is called the point operator. As illustrated
by the example, the point operator appears directly below the point located by the final search in
a sequence of searches and constructs the tail interval that starts with the point so located. The
point operator is used to locate a point within a context and, when the point is located, assert that
a property holds over the suffix of the computation starting at that point. The point cannot be
located if any of the searches fails.
The final example shows that, by itself, an interval line represents the full context.
To assert that a formula h holds at the initial point of an interval, h is drawn left justified below
the left delimiter. For example,
f
f true
f

Figure

1: Examples of some derived intervals (left column) and their definitions (right column).
asserts that h holds at the first point of the designated interval. A formula holds vacuously at
the first point of an interval that cannot be constructed. Thus, if either f or g never holds in the
future, or if the first (future) point at which f holds does not precede the first (future) point at
which g holds, then (1) holds by default. The right brace helps, visually, to delimit the formula.
The subformulas that appear in an interval formula (e.g., f , g and h in the above formula) may be
arbitrary graphical interval logic formulas.
GIL provides the usual logical operators: - (conjunction), - (disjunction), ) (implication),
composed of subformulas that contain intervals
are drawn using a vertical layout. In vertical layout, the operands of a binary operator are left
justified, with the first operand above the second and the operator between them, and a formula
to be negated is drawn left justified below the negation sign.
f
f
f
f
f
Conjunction is the default in vertical layout, so that the operator - can be omitted in the first
example above.
Both layout and precedence rules determine the grouping of operations. GIL formulas obey a
variation of Landin's offside rule [21], which requires that every token of a formula lie in the lower
right quadrant determined by the upper left corner of the smallest rectangle that contains its first
token. The first token that does not obey this rule, called an offside token, terminates the parse of
a formula. The precedence of operators (from high to low) is: negation, conjunction, disjunction,
implication, and equivalence. Binary operators associate from left to right. Right braces delimit
interval formulas and permit explicit grouping of operations.
The weak Until operator U of propositional temporal logic (PTL) is expressed in GIL as follows.
f
(2)
The formula asserts that g holds at the first point where either f does not hold or g does hold,
unless no such point is located. In the latter case, f (as well as :g) holds at all future points. In
other words, f holds at least until g holds.
GIL provides a special syntax for invariants and eventualities. To assert that a formula holds
at every point in an interval, the formula is drawn indented directly below the interval. To assert
that a formula holds at some point within an interval, the formula is drawn left justified directly
below a diamond 3 drawn on the interval. Figure 2 shows these conventions and their definitions.
The definition (top right) of the invariant notation (top left) can be understood as follows. Since
false does not hold at any point of a context, the point formula holds precisely if the search to :f
fails, i.e. if f holds at all future points. Similarly, the formulas in the bottom row assert that f
holds at some future point.
As noted above, an interval formula holds vacuously if any search performed in locating the ends
of the interval fails or if the interval is empty. Thus, an interval formula is implicitly predicated on
locating all search targets and on locating the left end of the interval before locating the right end.
We therefore refer to the search operator and interval operator described above as weak operators.
GIL also provides strong versions of these operators, which are useful in specifications and in
expressing the negations of interval formulas. A double arrowhead denotes a strong search and
asserts that the search succeeds unless some prior weak search fails. A double line denotes a strong
interval and asserts that the point located by the search for the interval's left end strictly precedes
that located by the search for its right end unless some search fails. For instance,
false
f
f
false

Figure

2: Representation of invariants (top left) and eventualities (bottom left), and
their definitions (right column).
holds by default if the search for f fails. However, if this search succeeds, then the formula requires
that the subsequent searches for g and h succeed, that the interval is not empty (h does not hold
at the point located by the second search), and that k holds at the first state of the interval.
The dual of an interval formula is obtained by changing the senses (strong to weak and weak
to strong) of the interval modality and of the searches for the ends of the interval. This dual
relationship implies that negation can be moved into an interval formula by changing the senses of
the interval and of its searches. For instance, the negation of (3) is equivalent to
The appendix gives formal definitions for the syntax and semantics of GIL.
3 An Example Specification
We present a GIL specification for an elevator system to illustrate the ideas in the previous section.
The example includes specifications of basic safety and liveness requirements, and also of more
complex fairness requirements.
For simplicity, we consider an elevator with three floors. The specification makes use of the
following state predicates, for 3. The predicate at$n is true when the elevator is at floor n
and false when it is not. The predicate goingup models a physical switch whose setting, when
the elevator leaves a floor, determines the direction of travel: up, if goingup is true, and down, if
goingup is false. The predicate open$n is true when the doors to the elevator are open at floor n
and req$n is true when there is an outstanding request for service at floor n. Finally, when the
elevator is at the second floor, arriveup indicates whether it was going up or down when it arrived.
Specifications are read from top to bottom and left to right. By convention, we begin each
specification with a context line, which represents a legal execution of the system. The first specification
initial requirements and the remaining specifications describe system invariants.
We associate labels (shown in bold) with specifications for reference purposes below.
Init. The elevator begins operation at the first floor, all doors are closed, and there are no
requests for service.
3. The elevator is never at two different floors simultaneously.
at$n
at$m
UpFrom$1. The elevator goes up when it departs the first floor, arriving at the second floor
without first visiting any other floors.
goingup
at$3
The invariant in this formula is predicated on locating a point at which the elevator has just left
the first floor. The specification asserts that the elevator is going up at every such point and that
it reaches the second floor before either of the other floors. The strong search requires that the
elevator eventually arrives at the second floor and the strong interval requires that it does not arrive
there immediately upon leaving the first floor, but takes some time to do so.
UpFrom$2. The elevator goes up when it departs the second floor precisely if it goes directly
to the third floor.
goingup
at$3
DownFrom$2. The elevator goes down when it departs the second floor precisely if it goes
directly to the first floor.
DownFrom$3. The elevator goes down when it departs the third floor, arriving at the second
floor without first visiting any other floors.
3. The doors open at a floor only when the elevator is at the floor.
open$n
open$n
at$n
3. The elevator departs a floor only when the doors at the floor are
closed.
at$n
at$n
open$n
3. The doors open at a floor only in response to a request for service
at the floor.
req$n
open$n
req$n
3. A request for service at a floor is only canceled if the floor is being
serviced (the doors are open).
req$n
req$n
open$n
3. The doors do not remain open indefinitely, and all requests for
service at the current floor are canceled when they close.
open$n
open$n
req$n
ArriveUp. Whenever the elevator arrives at the second floor from the first floor arriveup is
true, and it remains true at least until the elevator departs the second floor.
arriveup
ArriveDown. Whenever the elevator arrives at the second floor from the third floor arriveup
is false, and it remains false at least until the elevator departs the second floor.
at$3
arriveup
ContinueUp. If the elevator is going up when it arrives at the second floor, it continues going
up when it departs the second floor precisely if someone requires service at the third floor by the
time the elevator departs.
arriveup
goingup
ContinueDown. If the elevator is going down when it arrives at the second floor, it continues
going down when it departs the second floor precisely if someone requires service at the first floor
or no one requires service at the third floor by the time the elevator departs.
arriveup
goingup
ContinueUp and ContinueDown require that, once the elevator starts traveling in a given direction,
it changes directions only if no one requires service at a floor in that direction. The disjunction in
ContinueDown permits (but does not require) the first floor to act as the 'home floor', to which
the elevator can return when it is idle.
3. If a passenger requests service at a floor by the time the
elevator reaches the floor, the elevator opens its doors before departing the floor.
at$n
at$n
req$n
open$n
at$n
3. If a passenger needs service at a floor while the elevator is
at the floor and no one needs service at another floor, then the elevator opens its doors before
departing the floor.
at$n
req$n
req$m
req$k
open$n
at$n
We use m and k in this and the remaining specifications to denote the other floors, that is, f m; k
3. If the elevator is at a floor and a passenger requires service at
a different floor, then either the doors open at the current floor or the elevator departs the floor
(without first opening the doors).
req$m req$k
at$n
open$n
at$n
at$n
open$n
3. The elevator departs a floor without first opening its doors
whenever no passenger requires service at the floor, the doors are closed, and someone needs service
at another floor.
at$n
req$n
open$n
req$m req$k
at$n
open$n
The last four specifications ensure that the elevator makes progress and that it services floors in
a timely fashion. If a passenger requests service at a floor by the time the elevator arrives there, the
appropriate ServeReqsOnArrival specification guarantees that the elevator stops at the floor before
traveling on to other floors. Similarly, the ServeNoConflict specifications ensure that the elevator
services a request if the elevator is at the floor needing service and no one is waiting for service at
another floor. However, if a passenger requires the elevator at some other floor, the appropriate
NoServeDepart specification ensures that, once the current floor is serviced, the elevator departs
the floor without servicing any additional requests for service at the current floor that may be made
in the interim. The ServeOrDepart specifications prevent the elevator from sitting idlely at a floor
if other floors require service.
For purposes of comparison, we show how UpFrom$2 and ArriveUp are expressed in PTL.
Nested until operations are required to limit the scope of subformulas to the appropriate contexts.
UpFrom$2:
ArriveUp:
Graphical Proofs of System Properties
An important benefit of formal specifications is that they can be analyzed for potential conse-
quences. Analysis can demonstrate that specifications correctly express higher-level system requirements
and can help the designer learn more about the system under development. If analysis
reveals that the specifications admit computations that violate requisite properties, the specifications
are incomplete or in error. On the other hand, when desired properties can be proved from the
specifications, the designer gains confidence that they provide a complete and accurate description
of the system to be built.
The following are examples of properties that are required of the elevator system. The first
requirement is one of many safety properties that a designer might wish to establish. The second
a minimal fairness requirement.
3. The elevator must be at a floor for its doors to be open there.
open$n
at$n
3. The elevator eventually responds to a request for service.
req$n
open$n
The specifications for a system express temporal constraints on legal computations. Thus, the
system satisfies a requirement r if the conjunction s of the specifications implies r, or, equivalently,
the implication s ) r is valid. In principal, the GIL proof checker can check the validity of this
inference. However, in practice, theorem proving requires human assistance to be computationally
Init:
SafeOpen$n:
SafeDepart$n:
Safe$n:
open$n
open$n
open$n
at$n
at$n
at$n
open$n
open$n
at$n

Figure

3: Proof of Safe$n, 3.
feasible. The designer provides this assistance in our proof method by breaking down a complex
proof into inferences that are small enough for the GIL proof checker to validate.
A major advantage of a visual logic, such as GIL, is that a proof can be represented using pictures
that show the temporal flow of the argument. The graphical representation of the timeline allows
one to align appropriate points in the picture. Such alignment helps the designer see the points at
which invariants are being instantiated, the intervals and points being aligned to establish bounded
liveness and invariance conditions, the relationships between different points and intervals, and so
on. These visual cues can be extremely helpful both for constructing proofs and for discovering
potential fallacies. This 'syntactic sugar' has no semantic content in the proofs below, although we
are investigating a technique that will permit the designer to use alignment to specify orderings of
points within a specification.
The alignment and ordering of points on a timeline has other uses as well. For instance, the
GIL toolset provides a model generation facility for producing a counterexample in the case that
an inference is invalid. The counterexample can be displayed as a sequence of states or as a timing
diagram. Aligning the states in the implication appropriately with this counterexample can help
illustrate the fallacy in the inference.
The proof of Safe$n in Figure 3 uses alignment to highlight the underlying correctness argument.
The annotations alongside the picture show the specifications used in the proof. As shown by the
annotations, Safe$n is proved from
ffl Init, which asserts that the doors are not open at floor n when the system starts up
ffl SafeOpen$n, which asserts that the elevator is at floor n when the doors first open at the
floor
ffl SafeDepart$n, which asserts that the doors have closed by the time the elevator departs the
floor
Aligning the invariant in SafeDepart$n with the point located by the search to open$n in SafeOpen$n
highlights the fact that, when the invariant is evaluated at this point, it guarantees that at$n holds
continuously from the (arbitrary) point at which open$n becomes true at least until open$n is false.
The proof of Service$n is too complex to be accomplished in a single step. Figure 4 shows the last
step in the proof. As shown by the annotations alongside the figure, the final deduction makes use
of several specifications and of the intermediate result Arrive$n, which is established independently
as another step of the proof. The reasoning illustrated by the picture can be understood as follows.
If req$n holds at a point in a computation, but becomes false at a future point, then WaitService$n
ensures that the invariant in Service$n holds at this point. To highlight this reasoning, we align
the invariants in WaitService$n and Service$n and align the points at which open$n is asserted to
hold. The remaining premises establish Service$n in the case that req$n holds continuously from
some point in a computation. We use Arrive$n to deduce that there is a future at$n-point. The
at$n-point is purposely positioned within the span of the search arrow in WaitService$n to remind
the reader that we are interested in the case where at$n is true before req$n is false. The next
three premises represent a case split. The invariant in ServeNoConflict$n establishes the invariant
in Service$n in the case that req$m and req$k are both false at the at$n-point. The invariant
in ServeOrDepart$n establishes Service$n in the case that req$m or req$k is true at the at$n-
point and at$n holds throughout the future. Finally, the invariant in ServeReqsOnArrival$n when
instantiated at the next :at$n-point, establishes the required invariant in the case that req$m or
req$k is true at the at$n-point and there is some future point at which at$n is false.

Figure

5 shows how a complex proof is split into more manageable steps by case analysis.
It represents the last step in the proof of Arrive$n. In the same style as the previous example,
WaitService$n and Safe$n establish the required invariant when req$n is false at some future
point. The remaining premises are required when req$n holds continuously from some point in
WaitService$n:
Arrive$n:
req$n
req$n
open$n
req$n
at$n
at$n
req$n
req$m
req$k
open$n
at$n
at$n
req$m req$k
open$n
at$n
at$n
open$n
at$n
at$n
req$n
open$n
at$n
req$n
open$n

Figure

4: Final deduction in the proof of Service$n,
WaitService$n:
Safe$n:
ArriveSomeFloor:
Arrive$n-At$m:
Arrive$n-At$k:
Arrive$n:
req$n
req$n
open$n
open$n
at$n
at$n
at$m
at$k
at$n
at$m
at$k
at$m
req$n
at$n
at$k
req$n
at$n
req$n
at$n

Figure

5: Final deduction in the proof of Arrive$n,
a computation. ArriveSomeFloor represents a progress requirement needed to ensure that the
elevator does not remain in transit indefinitely, but eventually arrives at some floor. This permits
the proof to be reduced to the two cases represented by Arrive$n-At$m and Arrive$n-At$k, which
assert, respectively, that the elevator eventually arrives at floor n from floor m and that it eventually
arrives at floor n from floor k.
Proofs of ArriveSomeFloor, Arrive$n-At$m and Arrive$n-At$k are required to complete the
proof of Service$n. The requirement ArriveSomeFloor follows directly from the specifications Init,
UpFrom$1, UpFrom$2, DownFrom$2 and DownFrom$3. The high-level strategy used in the proofs
of Arrive$n-At$m and Arrive$n-At$k is to first show that the specifications ensure the elevator
does not remain at a floor indefinitely if it is needed at a different floor. These 'departure results'
and UpFrom$1 ensure Arrive$2-At$1. Similarly, the departure results and DownFrom$3 imply
Arrive$2-At$3. For the proof of Arrive$1-At$2 and Arrive$1-At$3, the departure results and the
specifications are first used to show that, if the elevator is traveling down when it arrives at the
second floor, it eventually arrives at the first floor. Arrive$1-At$3 follows easily from this, the
departure results, and the specifications. Finally, we use Arrive$1-At$3, the departure results and
the specifications to show that the elevator eventually arrives at the first floor if it is traveling
up when it reaches the second one. The proofs of Arrive$3-At$2 and Arrive$3-At$1 parallel those
of Arrive$1-At$2 and Arrive$1-At$3. The departure results are established by a straightforward
(but tedious) case analysis. The full proof is given in [6] in the form of intermediate lemmas and
annotated proof trees. 2
5 The Graphical Interval Logic Toolset
We have built a prototype GIL toolset to demonstrate proof-of-concept and permit experiments with
the logic. The prototype includes a visual editor that allows specifications to be easily constructed
and to be stored in and retrieved from files, a proof checker that mechanically checks the validity
of temporal inferences, and a model generator that exhibits state sequences over which formulas
hold. This section provides a brief overview of the GIL toolset.

Figure

6 shows the appearance of the interface of the GIL editor (GILED). Formulas are edited
on a canvas, which comprises the main region of the display. The canvas in Figure 6 contains a
template for creating a new specification. The template consists of an outer context interval and
This technical report can be obtained by anonymous ftp from directory /pub at ftp.cs.ucsb.edu.

Figure

a box, automatically positioned below the start of the interval, that represents a formula that has
yet to be defined. The designer uses the mouse during editing to select formulas in the canvas and
editing operations; the box is selected (indicated by shading) in the example. Scroll bars permit
the canvas to be scrolled for viewing large formulas.
The buttons in the panel on the lower left side of the display correspond to GIL primitives.
The Text button allows a box to be replaced with a state predicate. The remaining buttons in
the lower left panel specify GIL operators that apply to appropriate formulas. First are buttons
corresponding to the four temporal operators: the interval ) , eventuality 3, invariant 2, and
point 4 operators. 3 The last five buttons correspond to the propositional operators: disjunction
-, conjunction -, negation :, implication ), and equivalence j. The buttons in the upper left
panel provide language independent editing operations. Commands to override the default layout
of formulas and commands for storing and retrieving formulas are found in the Edit and File pull-down
menus. The proof checker is invoked and models are displayed using commands provided
3 As noted in Section 2, the eventuality, invariant, and point operators are derived from the interval operator. How-
ever, they correspond to common conceptualizations that are distinguished by the graphical syntax for visualization
purposes.
in the Misc pull-down menu. Models are displayed graphically in an accompanying window (not
shown in Figure 6).
Briefly, to build the formula UpFrom$1, a designer might begin by selecting the New button, 4
which produces the template shown in Figure 6. The 2 and ) buttons can then be used to (auto-
matically) indent the box below the context line and expand it into an implication. This produces
the following template for an invariant implication.
GILED selects a box to expand next by default; however, the designer may override the default
selection at any time using the mouse.
Selecting the second box and the 4 button converts the consequent into a point formula. For
this requirement, the designer uses the mouse to position a single search arrow. GILED then produces
a point symbol and a box to represent the search target, as shown below.
The designer can continue in this fashion to produce a template with the required structure.
4 The New button in the current implementation of GILED does not automatically generate the right parenthesis.
This will be rectified in the next version of GILED.
The interval in this template is created by first expanding a box into an appropriate interval
template, using the mouse to position the interval and the search arrow. The ) button produces
search arrows and weak intervals by default, so that the designer then clicks the mouse on the
appropriate search arrow and interval to obtain their strong counterparts. To convert the above
template into UpFrom$1, the designer selects the pending boxes in turn, clicks on the Text button
and types the state predicates.
In addition to the editing operations illustrated above, GILED provides capabilities for cutting
and pasting formulas, resizing intervals and search arrows, repositioning invariants and eventuali-
ties, and so on. If a formula does not fit in the space alloted, GILED indicates an error and highlights
the oversized formula. The designer can correct the error by resizing contexts and searches and
repositioning formulas. The editor automatically resizes all affected subformulas to scale.
GILED interfaces with the GIL proof checker and model generator, allowing the designer to work
entirely with graphical formulas. Functions that access these tool components are provided in the
Misc pull-down menu under the labels Check Proof, which determines if the formula in the canvas
follows from premises designated by the designer, Prove, which checks the formula in the canvas
for validity, and Construct Models, which determines if the formula in the canvas is satisfiable.
Check Proof keeps track of the structure of each proof and checks for circular reasoning. Once
verified, a requirement need only be reverified if the designer modifies premises used (either directly
or indirectly) in the proof or if the designer wishes to modify the proof structure. In situations
where a proof fails or a formula to be proved is not valid, a counterexample can be displayed in a
separate window. Alternatively, Construct Models permits a model (infinite state sequence) that
satisfies the formula in the canvas to be displayed.
For example, to verify that Safe$1 follows from the specifications for the elevator system, the
designer would first create the requirement or, if Safe$1 was created and saved in an earlier GILED
session, load it from a file. The designer would then invoke Check Proof to begin construction of
a proof or, if Safe$1 was verified previously, to determine if the proof is up-to-date and learn the
premises used in the proof. If a current proof exists, the designer can opt to see the proof (i.e.
the implication automatically constructed by GILED to validate the inference). If a new proof is
to be attempted, GILED prompts the designer for the premises to use in the proof. In this case,
the designer would designate Init, SafeOpen$1 and SafeLeave$1 as premises. GILED would then
construct a proof similar to that shown in Figure 3 and check that it is valid. The designer can
also prove Safe$1 directly, without invoking Check Proof, by building an implication representing
the inference and invoking Prove to determine if the implication is valid.
When an attempt to verify a requirement fails, the designer can request to see a counterexample.
Consider, for example, the proof of Arrive$n shown in Figure 5. If the designer overlooks the premise
Safe$n and attempts to prove that Arrive$n follows from the other four premises, GILED generates
the counterexample shown in Figure 7. The model consists of an infinite sequence of states with the
state predicates having the values shown in the rectangles and the shaded state infinitely repeated.
(The absence of a state predicate indicates that there is no restriction on the predicate's value in
that state.) GILED displays timing diagrams beneath the state sequence to aid visualization. The
designer can also invoke Construct Models to directly generate a model that satisfies the formula
in the canvas.
req$n
at$m
open$n
at$k
open$n
at$k
at$m
at$n
open$n
req$n

Figure

7: Countermodel generated if Safe$n is omitted in the proof of Arrive$n shown
in

Figure

5.
The GIL tools can be accessed by anonymous ftp from directory /pub/gil at ftp.cs.ucsb.edu.
6 Implementation of the Toolset

Figure

8 shows the organization of the GIL tools. Rounded rectangles depict tool components
(functions) and square rectangles depict data structures manipulated by the tools. A designer
interacts with the tools through the mouse-driven interface provided by GILED. As described
above, GILED helps the designer create new graphical formulas and retrieve and modify existing
ones. It stores formulas in Unix files as abstract syntax trees with sufficient representational
information to recreate the layout specified by the designer when creating them. GILED also
provides the interface to the proof checker and model generator, both of which make use of an
intermediate representation of a formula as a semantic tableau. The procedure that constructs
the tableau requires leaner abstract syntax trees in which productions reflect the semantics, and
not merely representational variations in formula. Both the proof checker and model generator
communicate results back to GILED, which displays them to the designer. The tools run under
the X-window system and are written in Common Lisp using the Garnet graphics toolkit [25]. The
implementations of the GIL tools are discussed in [4, 16, 18].
7 Related Work
Graphical representations of computer systems have been common in software engineering practice,
but have lacked a rigorous formal basis and, thus, have tended to be illustrative and documentary
rather than an integral part of the software development process. Some notable exceptions include
the statechart visual formalism of Harel [13], a pictorial version of Milner's CCS, called IDCCS [8],
and the 8-automata of Manna and Pnueli [23]. Environments supporting the specification and
verification of concurrent systems have been built around both Statecharts [14] and IDCCS. These
languages are oriented toward the depiction of states and state transitions, whereas GIL focuses on
showing the evolution of properties in time.
Timing Diagrams [32] is a graphical notation for expressing precedence and causality relationships
between events in a computation. Like GIL, Timing Diagrams can be created using a graphical
editor and checked for validity. The semantics of Timing Diagrams are defined by translation to a
subset of temporal logic that can be decided very efficiently.
Allen's logic for expressing temporal relationships between intervals of time is the foundation
for the TIMELOGIC temporal reasoning system [15]. The logic is textual, but graphical represen-
GILED
Model Generator
Representation Level

Abstract

Trees
Semantic Level

Abstract

Trees
Procedure
Proof Checker

Figure

8: The GIL Tools.
tations are used to show relationships among intervals more clearly.
Moszkowski's Interval Temporal Logic [11] provides an interval-like ``chop'' operator C. Infor-
mally, f Cg is true of a context if there exists a point that partitions the context into a prefix
satisfying f and a suffix (subcontext) satisfying g. While the intuitive semantics of
chop are appealing, the decision problem for formulas with chop is non-elementary in the depth of
nested alternations of chop and negation. In contrast, intervals in GIL have a more operational
semantics, but do not increase the complexity of the decision problem as severely. GIL can express
a stronger version of chop, which suffices for expressing the properties of interest for the systems
we have considered.
GIL is closest to the Interval Logic (IL) of [33], from which it is largely inspired. However, there
are several presentational and semantic differences between the two logics, which we discuss briefly
below.
Both IL and GIL provide explicit construction of intervals using search operations. However,
they differ in the way that they construct intervals by the composition of searches. In IL, every
search restricts a context and intervals are obtained by nesting searches, yielding increasingly
narrower contexts. In GIL, the start and end of an interval are located independently by means
of a sequential composition of searches. Searches in IL are to intervals, rather than to states at
which formulas hold, as in GIL. There is no loss or gain in expressiveness in either approach,
but we feel that the state-based semantics of GIL are easier to define and understand. Moreover,
searching to intervals requires the introduction of event intervals, representing positive transitions
of formulas, and of "begin" and "end" operators, which are used to indicate how intervals located by
searching further restrict a context. IL permits searches into the past as well as the future. Allowing
unrestricted searches into the past makes the decision procedure for GIL non-elementary [28]. This
is a major difference from IL, where the presence of both future and past searches does not appear
to affect the complexity of the decision procedure.
Plaisted [26] demonstrated a decision procedure for IL, obtained through translation to an !-
regular expression-like language with a non-elementary decision problem. PSPACE-completeness
of IL was later established by Aaby and Narayana in [2], where they give a translation of IL to
an elementary, but non-logical, fragment of a non-elementary logic. The reduction is tedious and
unnatural, and points out the need for a simpler semantics that retains the advantages of being
able to reason within intervals. The proof checker for GIL is based on a direct automata theoretic
decision procedure for the textual interval logic described in the appendix. The complexity of the
automaton construction is 2 m where m is O(n k ) for a formula of size n and depth k of interval
nesting [29].
An experiment with a graphical representation of an IL specification for the alternating bit
protocol [24] demonstrated that a visual representation results in more intuitive and natural spec-
ifications. The leaner semantics of our logic make it more amenable than IL to a clean graphical
representation.
8 Conclusion
This paper has described a visual logic for specifying concurrent software systems that aids formal
reasoning about temporal properties of systems. Experiments with the logic have produced
graphical specifications for the sliding window protocol [17], a readers/writers database system [5],
a protocol to commit transactions on a shared database [18], and a fair mutual exclusion algorithm
[4], in addition to the elevator system. A prototype toolset supporting the analysis of GIL
specifications has been developed.
Current research is addressing issues relating to the display of GIL formulas and the specification
of temporal properties. In particular, we are experimenting with vertical spacing and scaling the
size of operator symbols to improve the visual appearance of complex formulas and make their
structure more visually evident. We are also investigating issues relating to the alignment of
formulas to reflect known constraints on the partial ordering of points. A recent extension to
GILED allows the designer to specify constraints on the ordering of points within a specification.
Heuristics for recognizing search patterns that commonly occur in specifications and that impose
an ordering on points in the specifications are being investigated. In such cases, GILED could aid
the designer by aligning points accordingly. Methods for using a counterexample to realign the
points of graphical formulas that constitute an invalid proof are also being explored. This would
assist the designer in revising and correcting the proof and specifications.
GIL is very general, and certainly admits formulas that lack the immediate visualization of
the sample specifications presented in Section 3. For example, the semantics of searching to a
formula with nested intervals is subtle and difficult to visualize, even when the search is represented
graphically. However, we have not found a need for such searches in the specifications of
the concurrent systems that we have considered. Our experiments indicate that most temporal
properties of interest for concurrent systems can be specified in a natural and visually appealing
manner using the derived operators introduced in this paper. On-going research is attempting to
identify syntactic restrictions that permit inferences to be checked more efficiently and still allow
natural specifications of concurrent systems.
A real-time extension of GIL [30,31] provides primitives for bounding the duration of intervals.
We have recently modified the GIL proof checker to validate deductions in the extended logic and are
currently experimenting with its use. We are also investigating the integration of the GIL decision
procedure with an automated reasoning system that provides decision procedures for other useful
theories, such as linear inequalities and Presburger arithmetic, and that provides better support
for the management of proofs.
The GIL toolset is a prototype. It was developed to demonstrate proof-of-concept and to
facilitate experiments with the logic and its graphical representation. Both the logic and the
display of formulas have evolved based on our experience with the tools. We expect this process of
experimentation and revision to continue as we refine the current toolset into a working environment
for specification, validation and design of concurrent software systems. A robust, user-friendly
environment will permit empirical studies needed to determine whether software designers find a
visual logic, such as GIL, easier to use than a textual logic.

Acknowledgement

. The authors would like to thank Ron Dolin for implementing several last
minute modifications to GILED to improve the appearance of formulas.



--R


Propositional temporal interval logic is PSPACE complete.
Now you may compose temporal logic specifications.
Visual specifications for temporal reasoning.
Graphical specifications for concurrent software systems.
A graphical interval logic for specifying concurrent systems.
The declarative past and imperative future.
Integrated environments for formally well-founded design and simulation of concurrent systems
Parsing two-dimensional languages
The specification of visual language syntax.
A hardware semantics based on temporal intervals.
A propositional modal logic of time intervals.
Statecharts: A visual formalism for complex systems.
STATEMATE: A working environment for the development of complex reactive systems.
The TIMELOGIC temporal reasoning system.
A tool for the interactive generation of Graphical Interval Logic formulas.

A graphical interval logic toolset for verifying concurrent systems.
What good is temporal logic?
A temporal logic of actions.
The next 700 programming languages.
Verification of concurrent programs: The temporal framework.
Specification and verification of concurrent programs by 8-automata
A graphical representation of interval logic.
Comprehensive support for graphical highly interactive user interfaces.
A low level language for obtaining decision procedures for classes of temporal logics.
Modeling concurrency with partial orders.
Interval Logics for Temporal Specification and Verification.
An automata-theoretic decision procedure for future interval logic

Really visual temporal reasoning.
Specification of system-level hardware designs using timing diagrams
An interval logic for higher-level temporal reasoning
On the relation of programs and computations to models of temporal logic.
"Future"

--TR
Modeling concurrency with partial orders
Statecharts: A visual formalism for complex systems
A graphical representation of interval logic
Garnet
A propositional modal logic of time intervals
Graphical specifications for concurrent software systems
Interval logics for temporal specification and verification
The next 700 programming languages
Integrated Environments for Formally Well-Founded Design and Simulation of Concurrent Systems
First-Order Future Interval Logic
A Hardware Semantics Based on Temporal Intervals
An Automata-Theoretic Decision Procedure for Future Interval Logic
A Real-Time Interval Logic and Its Decision Procedure
Specification and Verification of Concurrent Programs by forall-Automata
On the Relation of Programs and Computations to Models of Temporal Logic
A Graphical Interval Logic Toolset for Verifying Concurrent Systems
A Low Level Language for Obtaining Decision Procedure for Classes of temporal Logics
Propositional Temporal Interval Logic is PSPACE Complete
The Declarative Past and Imperative Future
An interval logic for higher-level temporal reasoning
Now you may compose temporal logic specifications
A Graphical Interval Logic for Specifying Concurrent Systems

--CTR
Kirsten M. Hansen , Anders P. Ravn , Victoria Stavridou, From Safety Analysis to Software Requirements, IEEE Transactions on Software Engineering, v.24 n.7, p.573-584, July 1998
George S. Avrunin , James C. Corbett , Laura K. Dillon, Analyzing Partially-Implemented Real-Time Systems, IEEE Transactions on Software Engineering, v.24 n.8, p.602-614, August 1998
Sven Jrges , Tiziana Margaria , Bernhard Steffen, FormulaBuilder: a tool for graph-based modelling and generation of formulae, Proceeding of the 28th international conference on Software engineering, May 20-28, 2006, Shanghai, China
Miguel J. Hornos , Manuel I. Capel, On-the-fly model checking from interval logic specifications, ACM SIGPLAN Notices, v.37 n.12, December 2002
Lalita Jategaonkar Jagadeesan , Adam Porter , Carlos Puchol , J. Christopher Ramming , Lawrence G. Votta, Specification-based testing of reactive software: tools and experiments: experience report, Proceedings of the 19th international conference on Software engineering, p.525-535, May 17-23, 1997, Boston, Massachusetts, United States
L. K. Dillon , Y. S. Ramakrishna, Generating oracles from your favorite temporal logic specifications, ACM SIGSOFT Software Engineering Notes, v.21 n.6, p.106-117, Nov. 1996
Laura K. Dillon , Qing Yu, Oracles for checking temporal properties of concurrent systems, ACM SIGSOFT Software Engineering Notes, v.19 n.5, p.140-153, Dec. 1994
M. Autili , P. Inverardi , P. Pelliccione, A scenario based notation for specifying temporal properties, Proceedings of the 2006 international workshop on Scenarios and state machines: models, algorithms, and tools, May 27-27, 2006, Shanghai, China
Matthew B. Dwyer , Vicki Carr , Laura Hines, Model checking graphical user interfaces using abstractions, ACM SIGSOFT Software Engineering Notes, v.22 n.6, p.244-261, Nov. 1997
Matthew B. Dwyer , George S. Avrunin , James C. Corbett, Patterns in property specifications for finite-state verification, Proceedings of the 21st international conference on Software engineering, p.411-420, May 16-22, 1999, Los Angeles, California, United States
Aaron G. Cass , Leon J. Osterweil, Design Guidance through the Controlled Application of Constraints, Proceedings of the 10th International Workshop on Software Specification and Design, p.195, November 05-07, 2000
George S. Avrunin , James C. Corbett , Laura K. Dillon, Analyzing partially-implemented real-time systems, Proceedings of the 19th international conference on Software engineering, p.228-238, May 17-23, 1997, Boston, Massachusetts, United States
Matthew B. Dwyer , George S. Avrunin , James C. Corbett, Property specification patterns for finite-state verification, Proceedings of the second workshop on Formal methods in software practice, p.7-15, March 04-05, 1998, Clearwater Beach, Florida, United States
L. E. Moser , Y. S. Ramakrishna , G. Kutty , P. M. Melliar-Smith , L. K. Dillon, A graphical environment for the design of concurrent real-time systems, ACM Transactions on Software Engineering and Methodology (TOSEM), v.6 n.1, p.31-79, Jan. 1997
Lori A. Clarke , David S. Rosenblum, A historical perspective on runtime assertion checking in software development, ACM SIGSOFT Software Engineering Notes, v.31 n.3, May 2006
P. Bellini , R. Mattolini , P. Nesi, Temporal logics for real-time system specification, ACM Computing Surveys (CSUR), v.32 n.1, p.12-42, March 2000
Riccardo Mattolini , Paolo Nesi, An Interval Logic for Real-Time System Specification, IEEE Transactions on Software Engineering, v.27 n.3, p.208-227, March 2001
Laura K. Dillon , R. E.  Kurt Stirewalt, Inference Graphs: A Computational Structure Supporting Generation of Customizable and Correct Analysis Components, IEEE Transactions on Software Engineering, v.29 n.2, p.133-150, February
Betty H. C. Cheng , Joanne M. Atlee, Research Directions in Requirements Engineering, 2007 Future of Software Engineering, p.285-303, May 23-25, 2007
concurrent systems;visual languages;timing diagrams;automated proof-checking;formal specifications;temporal logic;graphical interval logic