Efficient verification of concurrent and distributed infinite-state systems

并发分布式无限状态系统的高效验证

• 批准号: RGPIN-2019-06039
• 负责人: Blondin, Michael
• 金额: $ 1.68万
• 依托单位: Université de Sherbrooke
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2021
• 资助国家: 加拿大
• 起止时间: 2021-01-01 至 2022-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=738671
• 关键词: Efficient; verification; concurrent; distributed; infinite

Concurrent and distributed systems are becoming more widespread as advances are made on multiprocessor architectures, cheap low-power devices, and natural computing. It is challenging to develop such systems in a reliable way, especially in the context of critical systems whose malfunction can, e.g., endanger lives, harm the environment, damage expensive equipment, or leak private data. Algorithmic verification is a powerful method that can be used to tackle this task. It involves abstracting concurrent or distributed systems into mathematical models which can then be analyzed exhaustively, rigorously and automatically. Most concurrent and distributed systems of practical use have infinitely many configurations. Unfortunately, central verification problems for infinite-state systems suffer from tremendously high computational complexity. Despite this, there has been important progress on the algorithmic verification of infinite-state systems. However, current techniques based on exact algorithms seem to have reached a ceiling, and hence new insights are needed to scale further. I intend to break this ceiling by developing a novel and unified theoretical framework of low complexity infinite-state systems (LCIS). This will be achieved incrementally by (a) studying relaxations of extended Petri nets, a prominent class of LCIS; (b) by demonstrating the applicability and efficiency of the theory to the verification of crowd systems, an emerging paradigm of distributed computing; and (c) by laying the foundations of an abstract LCIS framework inspired by the theory of well-structured transition systems.

随着多处理器体系结构、廉价低功耗设备和自然计算的进步，并发和分布式系统正变得越来越广泛。以可靠的方式开发这种系统是具有挑战性的，特别是在关键系统的背景下，其故障可能会危及生命、损害环境、损坏昂贵的设备或泄露私人数据。算法验证是一种强大的方法，可以用来解决这一任务。它涉及将并发或分布式系统抽象为数学模型，然后可以对这些模型进行详尽、严格和自动的分析。大多数实际使用的并发和分布式系统都有无限多的配置。不幸的是，无限状态系统的中央验证问题存在极高的计算复杂性。尽管如此，在无限状态系统的算法验证方面已经取得了重要进展。然而，目前基于精确算法的技术似乎已经达到了上限，因此需要新的见解来进一步扩展。我打算通过发展一个新的和统一的低复杂性无限状态系统(LCIS)的理论框架来打破这一限制。这将通过以下方式逐步实现：(A)研究扩展的Petri网的松弛；(B)通过展示该理论对人群系统的验证的适用性和效率，这是一种新兴的分布式计算范例；以及(C)通过为受结构良好的过渡系统理论启发的抽象的LCIS框架奠定基础。