关于SCOOP程序的验证

本文聚焦于SCOOP背景下程序验证工具箱的开发——SCOOP是一种优雅的并发模型，最近基于重写逻辑(RL)和Maude形式化。SCOOP在Eiffel中实现，其实用性也在机器人编程领域从实践角度得到展示。我们的贡献在于设计和集成一个别名分析器和一个Coffman死锁检测器，置于SCOOP同一基于RL的语义框架之下。这使得能够“免费”使用Maude重写引擎及其LTL模型检查器，以执行感兴趣的分析。我们讨论了我们的方法在模型检查死锁方面的局限性，并提供了状态爆炸问题的解决方案。后者主要由SCOOP形式化的规模引起，该形式化结合了真实并发模型的所有方面。在别名方面，我们提出了先前引入的基于程序表达式的别名演算的扩展，到无界程序执行环境如无限循环和递归调用。此外，我们设计了相应的可执行规范，易于在SCOOP形式化之上实现。我们扩展的一个重要性质是，在非并发设置中，相应的别名表达式可以根据正则表达式的概念进行过度近似。这进一步使我们能够推导出一种总是终止并提供“可能别名”信息的可靠过度近似的算法，其中可靠性意味着无假阴性。