
Specifying Timing Properties of Reactive Systems with TLC
Chuchang Liu Mehmet A. Orgun
Department of Computing
Macquarie University
NSW 2109, Australia
Email: fcliu,[email protected]
Abstract
Reactive systems usually contain several parallel processes, which are running concurrently. Therefore, it is essential to study and analyse each process based on its local time. Because of the introduction of local clocks, the temporal logic TLC is particularly suitable for the specification of those systems such as reactive systems, where granularity of time is needed. In this paper, we discuss the formal specification of reactive systems based on TLC. We in particular present a method to describe timing properties of reactive systems using TLC. In this logic, a system and its corresponding properties are represented as formulas, and the properties can be therefore directly reasoned about from the specification of the system.
Keywords Temporal logic, clocks, reactive systems, formal specification, local reasoning.
1 Introduction
Temporal logic has been widely used as a formalism for reasoning about time [13], program specification and verification [1, 10, 11], modeling temporal databases [2] and simulation applications [8, 9, 14]. There are also several suggestions for extending the expressive power of temporal logic for specifying timing properties of reactive systems [3]. These attempts can be roughly classified into two approaches { the bounded operator approach and the explicitclock approach. The first approach introduces one or more timebounded versions for each temporal operator, such as sometime 3 and always 2. The second approach uses a time variable t as the current time at each state.
For example, when we consider the requirement of a timed response of q to p within at most 2 time units, in the bounded operator approach, it can be specified by the formula
p ! 3<=2q,
Proceedings of the 20th Australasian Computer Science Conference, Sydney, Australia, February 5{7 1997.
while in the explicitclock approach, it is represented by the formula
(p ^ t = T ) ! 3(q ^ t <= T + 2),
where T is the rigid variable used to record the time at which p is true.
These approaches are all based on lineartime
temporal logics in which all predicates are usually
defined on a global time, for example, the sequence
of natural numbers < ; 1; 2; : : : >.
In some applications, such as distributed computations
[8], ecological modeling [12] and temporal
databases [2], one may find that it is necessary to
consider local time" or provide local clocks; some
events occur at irregular intervals, and it seems
unnatural to force them all onto a prescribed notion
of time. In particular, for reactive systems, it is
essential to study and analyse each process based
on its local time" or its local clock. When considering
the execution of transformational programs,
we find that such an execution can be viewed as
consisting of three consecutive activities: the environment
prepares an input, the program performs
its computation until it terminates and the environment
uses the output generated by the program
[11].
In reactive programming, if a program is not fast enough, it may miss some deadlines or fail to respond to important events. Thus, for a reactive system, it is important to describe the situation in which the program and its environment act concurrently, rather than sequentially. Reactive systems usually contain several parallel processes, which are running concurrently. From the point of view of each process, the rest of the program can be viewed as an environment that continuously interacts with the process. Therefore, for describing such a system naturally, it is necessary to introduce the notion of granularity of time.
Liu and Orgun [7, 8] recently proposed a temporal logic with clocks called TLC, which can be used to deal with granularity of time. In this logic, formulas are allowed to be defined on local clocks which are subsequences of the global clock.