微内核操作系统互斥量模块功能正确性的形式化验证
Formal Verification of Functional Correctness for Mutexes in Microkernel作者机构：首都师范大学信息工程学院北京100048 电子系统可靠性技术北京市重点实验室(首都师范大学)北京100048 北京成像理论与技术高精尖创新中心(首都师范大学)北京100048 上海交通大学约翰霍普克罗夫特计算机科学中心上海200030
出 版 物：《软件学报》 (Journal of Software)
年 卷 期：2024年第35卷第9期
页 面：4179-4192页
核心收录：
学科分类：08[工学] 0835[工学-软件工程] 081202[工学-计算机软件与理论] 0812[工学-计算机科学与技术（可授工学、理学学位）]
基 金：国家自然科学基金(62002246 62272322 62272323 62372311 62372312 61902240)
主 题：互斥量 功能正确性 形式化验证 定理证明 Coq定理证明器
摘 要：操作系统在许多安全攸关领域为软件系统提供关键性底层支撑,操作系统中一个微小的错误或漏洞都可能引起整个软件系统的重大故障,造成巨大经济损失或危及人身安全.为了减少此类安全事故的发生,对操作系统正确性进行验证十分必要.传统测试手段无法穷尽系统中的所有潜在错误,因而操作系统验证有必要使用具有严格数学理论基础的形式化方法.在操作系统中,互斥量可协调多任务对资源的访问,是一种常用的任务同步方式,其功能正确性对于保障多任务应用的正确性十分关键.基于定理证明方法,在交互式定理证明器Coq中对某抢占式微内核操作系统的互斥量模块进行代码级形式化建模,给出其接口函数的形式化规范,并实现这些接口函数的功能正确性验证.
维普期刊数据库
同方期刊数据库