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. ***