软件学报

作者：张林雁，李希萌，施智平，关永，曹钦翔，张倩颖

单位：张林雁，首都师范大学 信息工程学院, 北京 10004811,李希萌，首都师范大学 信息工程学院, 北京 100048;电子系统可靠性技术北京市重点实验室(首都师范大学), 北京 10004802,施智平，首都师范大学 信息工程学院, 北京 100048;电子系统可靠性技术北京市重点实验室(首都师范大学), 北京 10004803,关永，首都师范大学 信息工程学院, 北京 100048;北京成像理论与技术高精尖创新中心(首都师范大学), 北京 10004804,曹钦翔，上海交通大学 约翰霍普克罗夫特计算机科学中心, 上海 20003005,张倩颖，首都师范大学 信息工程学院, 北京 100048;北京成像理论与技术高精尖创新中心(首都师范大学), 北京 10004806

关键词：互斥量;功能正确性;形式化验证;定理证明;Coq定理证明器

基金：国家自然科学基金(62002246, 62272322, 62272323, 62372311, 62372312, 61902240)

操作系统在许多安全攸关领域为软件系统提供关键性底层支撑, 操作系统中一个微小的错误或漏洞都可能引起整个软件系统的重大故障, 造成巨大经济损失或危及人身安全. 为了减少此类安全事故的发生, 对操作系统正确性进行验证十分必要. 传统测试手段无法穷尽系统中的所有潜在错误, 因而操作系统验证有必要使用具有严格数学理论基础的形式化方法. 在操作系统中, 互斥量可协调多任务对资源的访问, 是一种常用的任务同步方式, 其功能正确性对于保障多任务应用的正确性十分关键. 基于定理证明方法, 在交互式定理证明器Coq中对某抢占式微内核操作系统的互斥量模块进行代码级形式化建模, 给出其接口函数的形式化规范, 并实现这些接口函数的功能正确性验证.

来源：2024年第9期

《软件学报》期刊编辑部

查看软件学报杂志2024年第9期