增强版Timed CSP与封闭时间自动机的等价性与表达力分析

"该研究探讨了Timed CSP（时间化通信顺序进程）的一个增强版本，并将其与封闭的时间自动机等价关系进行了深入研究。作者指出，增强的Timed CSP等价于具有封闭不变量和时钟约束的封闭时间自动机。这一发现揭示了新版本的Timed CSP具有更强的表达能力，能够捕捉到时间系统中最常见的规范，并且可以利用细化检查进行数字分析。通过这种方式，使用模型检查器FDR可以验证包括分支时间活性属性在内的关键时间规范，如无时间停止自由和常数可用性。文章强调，在密集时间建模范式下，使用实现框架表达规范并进行满意度验证的方法并不常见，而Timed CSP的离散精化技术为模型检查提供了新的可能性，尽管原始版本的Timed CSP在表达力上存在局限。" 在实时系统的形式化分析中，通常采用时间自动机作为实现形式主义，并使用时间逻辑来表述规范，然后通过模型检查来验证实现是否符合规范。Reed和Roscoe的Timed CSP提供了一种基于细化的方法，但其表达能力有限，例如，表达“进程P不能执行事件a”这样的规范需要复杂的证明。 文章介绍了一个增强的Timed CSP版本，它克服了这些限制，使得规范的表达和验证更为直接。这种增强的Timed CSP等价于封闭时间自动机，允许使用封闭的不变量和时钟约束。这种等价性意味着可以通过Timed CSP来表示和验证各种时间规范，包括那些涉及时间限制的行为属性。 此外，作者指出，由于新版本的Timed CSP能够与模型检查器FDR集成，因此可以有效地验证分支时间活性属性，比如系统在任何时候都不会停止运行（时间停止自由）以及服务始终可用（常数可用性）等重要属性。这标志着在密集时间建模范式下，通过使用增强的Timed CSP和模型检查技术，可以更高效地进行形式验证。 这项研究由美国海军研究办公室(ONR)和国家科学基金会(NSF)资助，并在2002年由Elsevier Science B.V.出版，遵循CC BY-NC-ND许可证。文章的作者来自杜兰大学和卡内基梅隆大学，他们在时间系统的形式化分析和模型检查方面做出了贡献，展示了如何改进Timed CSP以提高其在实时系统验证中的效用。