Temporal logic models for distributed systems.

Abstract

Since the beginning of the 1980's, the way the computer systems are conceived has changed dramatically. This is a direct result of the appearance, on a large scale, of personal computers and engineering workstations. As a result, networks of independent systems have appeared. This thesis presents a formal specification framework that can be used in the design of distributed systems. The abstract models that are presented are based on a systemic view of distributed systems and discrete event systems. Two base abstract models called deterministic discrete event systems (DDES) and discrete event automaton (DEA) are presented. For the DEA the series and parallel compositions as well as feedback connection are defined. Universal algebra is employed to study the parallel composition of DEAs. From the DDES/DEA an abstract model for distributed systems is obtained. Subsequently, linear time temporal logic is modified for use with the abstract chosen model of distributed systems. The logic is described in three aspects: syntax, semantics and axiomatics. The syntax is modified by the addition of two operators. The semantics of the logic is given over the abstract models. Five axioms are added to the axiomatic system for the two new operators. A programming language called TLL, based on the theoretical framework, links the theory with practice. The syntax and semantics of the programming language are presented. Finally an example of modeling in the framework is given.