Formal Methods in Concurrent and Distributed Systems

点击翻译按钮获取中文摘要

With the widespread use of distributed and concurrent systems and with the increase in the complexity of software for such systems, it becomes important to develop various methods for ensuring the quality of concurrent software systems. This project explores various methods for automated and semi-automated analysis and verification of concurrent and distributed systems. In particular, the research seeks methods based on temporal logic model checking for verification of concurrent systems. Although model checking has been applied fairly successfully for verification of quite a few real-life systems, its applicability to a wider class of practical systems has been hampered by the state explosion problem (i.e. the enormous increase in the size of the state space). In this research, symmetry based techniques are used to overcome the state explosion problem. In particular, symmetry is exploited for verification of liveness properties of real-life concurrent and distributed software systems. The effectiveness of symmetry-based methods for model checking requires efficient solutions to the orbit problem. A solution to the orbit requires checking if two given global states are equivalent under the symmetry. An efficient solution to this problem facilitates the construction of the quotient structure by collapsing each set of equivalent states into a single state. The project investigates various efficient algorithms for the orbit problem for many of the symmetries that occur in practical systems. It is implementing an on-line model checking system that exploits symmetry by simultaneously constructing reduced global state graph (i.e. the quotient structure) and exploring the partially generated quotient structure for existence of certain fair strongly connected components containing an incorrect computation. ***