并发进程的互模拟语义理论  

作　　者：邓玉欣 

机构地区：[1]华东师范大学 [2]上海市高可信计算重点实验室 [3]中国计算机学会形式化方法专业委员会

出　　处：《中国科技成果》2025年第5期58-58,共1页China Science and Technology Achievements

摘　　要：计算机软件已经成为国计民生的基础设施.如何保障计算系统的可信性是软件领域面临的重要挑战,以多核、并发、分布、异构和智能交互等为主要特征的系统已成为当今计算系统发展的主流.并发现象以其固有的复杂性增加了软件可信性保障的困难.由图灵奖得主C.A.R Hoare和R.Milner等人提出的进程演算,因其概念简洁、可用的数学工具丰富,得到了广泛的研究,并成功应用于并发系统的规范、分析、设计和验证.概率进程演算在传统进程演算中加入概率选择操作,以描述和分析不确定环境下的概率行为,例如在强化学习、智能决策、无人驾驶等应用中的常见行为.关于概率选择与不确定选择之间的交互是形式化验证研究中的难题.利用互模拟关系对并发进程的行为等价性和相似性进行验证是一个需要重点研究的验证技术.

关 键 词：互模拟 形式化验证 行为相似性 并发进程 

分 类 号：TP311.5[自动化与计算机技术—计算机软件与理论]