This paper presents an approach to operationally evaluate a temporal specification in a distributed computing environment. First, an algorithm Compute History is proposed to allow every distributed processor to collect events executed by itself and by other processors, and to order the collected events by causality. This algorithm employs neither monitors nor a global clock to order collected events of a processor. These collected events of a processor form an execution history of a distributed computation, and they represent behaviors of all the processors during execution. Next, the semantics of operational evaluation of a temporal assertion is presented. The evaluation of a temporal assertion is an examination of events of a processor’s collected histories against the assertion. Since the histories are computed in a faulty distributed environment and the assertion denotes a program’s specification, operational evaluation ensures satisfaction of a temporal specification in the presence of faults.
Tsai, Grace; Insall, Matt; and McMillin, Bruce M., "Ensuring the Satisfaction of a Temporal Specification at Run-Time" (1993). Computer Science Technical Reports. 42.
© 1993 University of Missouri--Rolla, All rights reserved.