关键词：可缩放模型；模型检测；安全性；活性
摘 要：This dissertation offers new capabilities of bit-level liveness verification in general and an in-depth formal analysis of communication fabrics with the objective of their scalable bit-level response verification. We show that the operations of industrially relevant hardware systems (communication fabrics in our case studies) can naturally give rise to a well-founded ordering in their state spaces. We provide an algebraic analysis of a set of industrially relevant communication fabrics. The analysis offers a rigorous mathematical justification of the Chatterjee-Kishinevsky invariants and their connection to the underlying network topology.