一、研究目标

针对嵌入式操作系统行为交互复杂、代码量大导致的形式化建模困难、形式化验证效率低和验证不充分的问题，突破复杂系统的组合建模验证和自动化验证等关键技术，研发相应的形式化验证工具。在保证验证质量的前提下，降低操作系统的验证复杂度、提高验证效率，为操作系统从行为属性端到设计实现端的整体自动形式化验证奠定技术基础。

二、主要研究内容

（1）开展嵌入式操作系统关键模块组合建模验证技术研究，解决复杂验证目标因不变量集聚而导致的验证复杂度高、验证不充分问题；

（2）开展嵌入式操作系统关键模块自动形式化验证技术研究，解决关键系统模块自动化验证中存在的并发随机行为难仿真、需求属性难度量等痛点问题，实现系统任意行为的精确描述仿真和高效自动化验证。

（3）开展嵌入式操作系统多线程并发行为的形式化建模与验证技术研究，验证并发场景下系统易出现的死锁、内存资源泄露等安全问题。

三、指标

（1）实现嵌入式操作系统关键模块抽象行为形式化建模，支持嵌入式系统随机交互事件行为仿真；

（2）提供需求与设计实现的一致性自动化验证，支持定性属性自动形式化验证（如，自动判定系统满足特定需求规范的概率是否大于或等于某一阈值），支持定量属性形式化验证（如，自动统计出系统满足特定需求规范的概率）；

（3）支持嵌入式操作系统关键模块的死锁、资源泄露等高危漏洞挖掘；

（4）支持自动化参数探索的批量属性形式化验证、验证结果统计及可视化。

四、线下对接方式

本课题采用线下对接报名。

联系人：姚蕊

联系电话：182*****767/010-********