Theoretical issues in the design and verification of distributed systems
Aravinda Prasad Sistla · 1983
With the rapid decrease in the cost of hardware distributed computing is finding wider application. The parallelism inherent in distributed processing makes it much more difficult to design reliable systems. Many software development techniques such as hierarchical design and exaustive testing used for large sequential programs are no longer adequate because of the high degree of nondeterminism present in parallelism. This thesis addresses the two aspects of correctness and performance in the design of distributed and concurrent systems. In chapters 2 through 5 we consider different temporal logics and their extensions, as formal systems for reasoning about concurrent programs. In chapter 2 we investigate the complexity of decision procedures for different versions of Propositional Linear Temporal Logics(PTL). We present a space efficient decision procedure for the full logic. We also present optimal decision procedures for other restricted versions of this logic. We investigate the problem of automatic verification of simple concurrent programs using correctness specifications given in PTL. PTL can not express many important correctness properties of concurrent programs. For this reason in chapter 3, we extend PTL by allowing quantifiers over propositions. We investigate the complexity of decision procedures for these logics. We show that for a weaker version of this logic, there is a tight space complexity hierarchy with the number of alternations of quantifiers, for the set of valid sentences in this logic. In chapter 4, we consider a branching time temporal logic for automatic verification of finite state concurrent processes. We present efficient algorithms for the automatic verification of finite state concurrent programs using specifications given in this logic. We show how this method can be applied to check the correctness of well known practical problems like the Alternating Bit Protocol and a solution to a mutual exclusion problem. In chapter 5, we extend linear temporal logic by introducing spatial modalities. This logic allows us to speak about temporal and spatial properties in a unified logical system. We show how this logic can be used for reasoning about many problems in fixed connection multiprocessor networks. In chapters 6,7 we investigate correctness and performance issues in the area of interprocess communication. . . . (Author's abstract exceeds stipulated maximum length. Discontinued here with permission of author.) UMI