Specifying Timing Properties of Reactive Systems with TLC

Chuchang Liu Mehmet A. Orgun

Department of Computing

Macquarie University

NSW 2109, Australia

E-mail: 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 explicit-clock approach. The first approach introduces one or more time-bounded 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 explicit-clock 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 linear-time 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.