互模拟准局部验证算法的扩展与实现

来源：软件学报杂志2018年第6期北京时间：

作者：郑晓琳,邓玉欣,付辰,雷国庆

单位：郑晓琳，上海市高可信计算重点实验室(华东师范大学), 上海 20006211,邓玉欣，上海市高可信计算重点实验室(华东师范大学), 上海 20006202,付辰，计算机科学国家重点实验室(中国科学院 软件研究所), 北京 10019003,雷国庆，上海市高可信计算重点实验室(华东师范大学), 上海 20006204

摘要：互模拟是并发系统分析和验证的一个重要概念.主要扩展了一种由Du和Deng提出的准局部算法，使其更加适用于一般的标记迁移系统.用Java实现扩展后的准局部算法与Fernandez和Mounier提出的局部算法.以VLTS为实验数据基准进行大量的实验，发现在大多数情况下，前者的性能比后者更好.同时，修改了算法使其能够验证模拟关系.最后，用Java实现对标记迁移系统进行转换，使算法同时可以验证弱互模拟关系.

关键词：互模拟;标记迁移系统;扩展

基金资助：国家自然科学基金（61672229，61261130589）；上海市自然科学基金（16ZR1409100）