系统可信性自动验证国家地方联合工程实验室于2016年10月获国家发改委批准立项建设。在学校及学院的关心支持下,实验室在2017年取得了一系列成绩,代表性成果总结如下:
1. 初步建成国际合作基地。
依托与英国Ulster大学合作建立的 “Advanced Machine Intelligence(先进机器智能)”联合研究中心,召开视频学术研讨会16场,教师互访6人次,联合培养研究生7名,加强系统可信性自动验证技术的研发和学术合作,增强了实验室在国际上的辐射力和影响力。
2. 持续改进应用型验证工具。
以原创的自动推理研究成果为核心,不断改进两类系统可信性自动验证工具:
(1)C程序自动验证工具Scavel C
(2)PLC程序自动验证工具Scavel PLC。
这两类工具自主可控,与传统测试工具在核心原理上存在根本区别,可以主要应用于软件验证、系统设计需求验证、安全协议验证等方面,有助于提高我国在国防军工、武器装备、航天航空、核工业、等领域的系统可信性。
通过核物理研究院、火箭研究院的合作应用测试,对比发现,Scavel C能够发现目前市场高占有率的测试工具KlockWork K10、Testbed等不能发现的缺陷,显现了其独有的作用。Scavel PLC自动验证工具的性能已达到工业级应用水平。中国工程物理研究院测评中心将实验室研发的验证工具 Scavel C列入采购计划;与中国运载火箭研究院评测中心针对PLC程序控制系统验证达成合作意向,目前正在研发专用验证系统。
3. 科研成果不断涌现。
2017年,实验室团队成员申请受理国家发明专利13项,相关软件取得计算机软件著作权登记证书1项(累计6项);新研发证明器20余个,证明了国际上其他证明器均未能证明的结论107个;新研发求解器10余个,在基准问题求解数量、求解时间等多方面已超过该领域国际最高水平竞赛SAT Competition 2016 Main Track的冠军得主MapleCOMSPS;主持协议验证系统技术方案一个,持续开展公式求解数量已经达到5亿。
4. 学术交流合作蓬勃开展。
实验室常年坚持学术报告会制度,每周三召开一次学术交流报告会,每周六召开科研学术进展汇报研讨会。一年来,实验室先后邀请海外知名专家Stephan Schulz教授(德国)、Xianyi Zeng教授(法国)、Jun Liu博士英国)、Luis Martinez教授(西班牙)、洪龙教授(南京邮电大学)等到公司短期讲学授课或学术交流;实验室成员陈树伟在国内重要学术会议上做大会报告3场;宋振明、陈树伟、何星星、徐鹏、钟晓梅等多次参加国内外学术会议;实验室成员一年来发表论文14篇,其中SCI检索4篇。
实验室学术带头人徐扬教授当选为中国逻辑学会非经典逻辑与计算专委会主任;宋振明教授当选为中国逻辑学会非经典逻辑与计算专委会秘书长;陈树伟老师担任《IEEE Trans. on Fuzzy Systems》、《Information Fusion》、《Information Sciences》、《International Journal of Computational Intelligence》等刊物的审稿人;徐鹏老师担任IEEE Access、IEEE Transactions on Cybernetics、IET Communications、IET signla processing等审稿人;陈树伟和何星星等多位老师还参与组织了ISKE2017国际学术会议;徐鹏、钟晓梅等老师还持续维护了核心期刊《The Journal of Fuzzy Mathematics》的网络版。
5.积极参与科技攻关项目和军民融合项目。
一年来徐扬、宋振明教授主持、其他多位教师参与论证、申报了“十三五”装备预研共用技术项目1项、九院技改重大专项项目1项、中央军委科技委项目1项;目前,正在与多家单位开展可信性自动验证应用类合作研究,相关验证工具正在中国工程物理研究院、中国运载火箭研究院、航天1院、航天3院、中车唐山机车车辆有限公司等单位试用和测试。
系统可信性自动验证国家地方联合工程实验室唐山分中心一期建设圆满完成,所承担的2016 -2017轨道列车网络控制系统3个可信性验证实施项目(到位经费190万)已经通过验收,正在报奖。
不含唐山分中心项目,2017年度实验室科研经费总量达到349万。其中,国家发改委批复建设项目经费200万、四川省经信委项目经费90万暂未到账。到账后,将会强有力支撑实验室的硬件升级拓建和应用系统集成等各项工作。