信号同步语言与Promela混合验证：GALS系统模型检查与应用

本文主要探讨了在GALS（全局异步/局部同步）系统的设计和验证过程中，如何结合Signal同步编程语言和Promela异步模型检查技术。Signal是一种用于描述同步组件的语言，而Promela则是SPIN（Software Product Line INstrumentation Notation）异步模型检查器的输入语言，它特别适用于处理异步系统。 首先，作者提出了一种方法，即从Signal模块出发，通过翻译机制将同步描述的部分转换成Promela过程，以处理GALS系统中无法在Signal中直接描述的异步部分。这一翻译过程被证明是等价的，确保了两种描述方式的正确性。这种方法的关键在于能够在异步环境中利用Promela的强大功能，特别是对于复杂通信协议的处理，如使用LTTA（Loosely Time-Triggered Architecture）的松散时间触发总线设计。 其次，通过将Signal的局部同步组件映射到Promela的全局异步模型，文章引入了一种抽象技术，即用有限的FIFO（First-In-First-Out）通道替换实际的GALS系统中的通信总线，这种抽象简化了模型，提高了SPIN进行大规模模型检查的效率和扩展性。这是在保证系统行为正确性的同时，降低了验证复杂度的重要步骤。 接着，作者证明了在Promela中表示的GALS系统模型与其硬件实现之间的迹等价性，这意味着通过在Promela中进行模型检查，可以确保设计的正确性。这一成果为基于Promela模型的GALS系统验证提供了可能性，对于复杂的嵌入式系统设计来说，这是至关重要的验证手段。 最后，作者展示了他们提出的混合验证方法在实际应用中的例子，通过验证一个中央门锁系统的GALS架构，采用LTTA的汽车系统，展示了这种方法的有效性和实用性。这表明，通过将Signal和Promela的优势相结合，可以在设计和验证GALS系统时克服时序收敛的挑战，提升整个验证流程的效率和可靠性。 总结来说，这篇文章的核心贡献在于提出了一种有效的方法，即通过混合使用Signal和Promela，解决GALS系统设计中的异步与同步部分的验证难题，从而推动了嵌入式系统特别是片上系统设计的验证技术发展。