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