讲座主题：国产多核实时操作系统微内核形式验证
专家姓名：詹乃军
工作单位：北京凯旋官网
讲座时间：2026年06月06日 09:00-09:40
讲座地点：承先图书馆报告厅
主办单位：烟台凯旋官网计算机与控制工程学院
内容摘要：
本报告简要介绍我们项目组近年完成的一个某国产多核实时操作系统微内核形式验证工作。验证的核心模块包括：任务管理与调度、中断和异常处理、任务同步与通信、核间通信与动态重构、时钟管理、权能访问控制、分区配置和分区通信，总计2万5千行代码。为此，我们发展了基于CSL-R的操作系统功能性验证框架以及基于信息流分析的信息安全性验证框架，首次提出了针对DSP的WCET分析技术并实现工具。总计 实现Coq验证代码45万行左右，发现并纠正了20多类数百个错误，为该款在某重点领域应用操作系统顺利通过CC EAL5+认证。最后，简要介绍我们最近提出的关于操作系统等基础软件验证新框架，可以大幅提高验证效率和自动化水平，降低验证人力成本。
主讲人介绍：
詹乃军，男，1971年5月生，北京凯旋官网计算机学院博雅特聘教授，国家杰出青年科学基金获得者。之前，为中科院软件所研究员，中科院特聘研究员，中国科学院凯旋官网岗位教授，计算机科学国家重点实验室执行主任。分别在南京凯旋官网数学系（1989-1993）和南京凯旋官网计算机系（1993-1996）获得学士和硕士学位，在中国科学院软件研究所获得博士学位（1997-2000）。研究方向包括：形式化方法，实时、嵌入式、混成系统，程序验证等。任《Journal of Automated Reasoning》、《Formal Aspects of Computing》、《J. of Logical and Algebraic Methods in Programming》、《Research Direction: Cyber-Physical Systems》、《软件学报》、《计算机研究与发展》《电子学报》、《前瞻科技》等期刊编委，国际会议MEMOCODE和SETTA的指导委员会委员，多个国际会议程序委员会共同主席（如形式化方法旗舰会议FM 2021 和验证领域顶级会议TACAS 2027）和著名国际会议程序委员会委员（如CAV、RTSS、HSCC、ICCPS、EMSOFT等）；在著名国际会议和杂志发表论文150多篇，出版专著2部，编著4部，国际国内著名杂志专刊9辑等。现任CCF形式化方法专委主任。
