迪捷软件受邀出席中车软件质量提升交流会

2021-08-04 15:24:48 迪捷软件 22

随着信息技术的飞速发展,软件产品已应用到社会各个领域,软件质量就是软件产品的灵魂,软件质量的保障也因此变得尤为重要。10月22日,以“形式化验证”为主题,由中车株洲电力机车有限公司举办的“2020软件质量提升交流会”在株洲市召开,浙江迪捷软件科技有限公司应邀参展并做主题报告。


迪捷软件受邀出席中车软件质量提升交流会


什么是形式化验证?


形式化方法是建立在逻辑演算、形式语言、自动机理论、程序语义、类型系统等理论基础之上,对计算系统进行描述和分析的一系列符号与技术的集合。形式化方法可指导软/硬件系统的规约、设计和验证,是改善和确保计算系统质量的重要方法。历史上,形式化方法在硬件和协议验证方面取得过巨大成功。这种技术变革对未来软件产业,尤其是安全关键领域的软件研发必将产生深刻的影响,对我国工业设计软件领域而言既是新一轮难得的机遇,同时也充满了挑战。我国在高端装备制造业的核心工具软件方面长期受制于人,能否借此新的机遇摆脱困局?迪捷软件创始人康烁先生在报告中作出了自己预判。康烁先生介绍了迪捷软件在编译器形式化验证方面的成果,我司已自主研发了一款基于Lustre的语言到C语言的可信编译器——L2C,是形式化验证的代码生成工具ModelCoder的核心技术。


MetInfo enterprise content manager system | MetInfo CMS


ModelCoder是什么

迪捷软件的形式化验证的代码生成工具ModelCoder软件研发项目正式启动于2010年9月, 目前已在国内核电领域的得到应用,我们正在抓紧研发更适应国内其他关键领域(航空、航天、轨道交通等)需求的通用可信编译器以及相关配套工具(静态分析/仿真/调试/WCET分析/图形语言等)。与Scade工具相比,ModelCoder及L2C编译器在成熟度以及源语言表达能力方面虽尚有不足,但从形式化方法应用的角度来看,二者各有千秋。Scade基于模型检查实现了较强的源程序静态分析功能,这是L2C目前尚未涉足的领域。L2C基于定理证明对完整的代码生成过程进行了形式化验证,而Scade代码生成器的可靠性保障则一直依赖于测试与过程管理等传统方法。从目前的实际效果来看,L2C产品的推进与实施,结束了Scade在合作企业(之前也是Scade客户)上的业务渗透。


MetInfo enterprise content manager system | MetInfo CMS



电话咨询
在线咨询
解决方案
QQ客服