English

系统可信性自动验证国家地方联合工程实验室

National-Local Joint Engineering Laboratory of System Credibility Automatic Verification 


系统可信性自动验证国家地方联合工程实验室于2016年10月获国家发改委批准立项建设,在四川省系统可信性自动验证工程实验室(由四川省发改委于2014年批准成立)的基础上升格而成。实验室围绕信息安全行业的重大需求,在原创的自动推理体系为核心基础的支撑下,形成科学有效的系统可信性自动验证技术,研发系统可信性自动验证工具及针对重要领域的专用验证系统,摆脱系统可信性自动验证技术对国外的依赖,提高我国在可信性验证领域的自主创新能力,为系统的可信运行提供科学技术保障。



实验室自主研发了程序可信性自动验证工具Scavel。该工具具有直接验证源码、验证需求设置灵活、错误定位准确、快速高效的特点,可验证C、PLC程序中的数组越界、被零除、有符号整数溢出、浮点数溢出等缺陷。Scavel已为涉及航空航天、国防军工、核工业、卫星导航、轨道交通、信息电子等领域的多个单位提供了验证服务,其效果显现了验证工具的独有能力。

实验室现在已建成形式化系统、自动推理系统、可信性自动验证三个研发平台,与英国Ulster大学共同建立了“Advanced Machine Intelligence(先进机器智能)”联合研究中心,在系统可信性验证领域培养了多名高素质科技人才。实验室研发成果居国际先进水平。 


  

National-Local Joint Engineering Laboratory of System Credibility Automatic Verification was approved by the National Development and Reform Commission in 2016. This engineering laboratory is an upgraded version of the System Credibility Automatic Verification Engineering Lab of Sichuan Province approved by Sichuan Provincial Development and Reform Commission in 2014. Around the great demand of the information security industry, the laboratory establishes the effective technology of system credibility automatic verification and researches   system credibility automatic verification tools and special verification systems for the important areas based on the original automated reasoning system, which can get rid of the dependence of the system credibility automatic verification technology on foreign countries, improve our country's independent innovation capability in the field of credibility verification, and provide the scientific and technical support for the reliable operation of the system.

The Laboratory has developed the program credibility automatic verification tool Scavel. This tool has some important properties, i.e., direct verification of the source code, flexible setting for validation requirements, accurate fault location, high efficiency and it can verify multiple defects for C and PLC program such as array bounds, divide by zero, signed integer overflow, floating point overflow, etc. Scavel has provided verification services for multiple units from aerospace, defense industry, nuclear industry, satellite navigation, rail transportation, information electronics and other fields, which shows its unique ability.

The laboratory now has built three research and development platforms, which are formal system platform, automatic reasoning system platform, credibility automatic verification platform, established the Advanced Machine Intelligence joint research center with the University of Ulster, and developed a number of highly qualified scientific and technical personnel in the field of system credibility verification. Laboratory research and development results have reached the international advanced level.