迪捷软件受邀出席中车软件质量提升交流会
随着信息技术的飞速发展，软件产品已应用到社会各个领域，软件质量就是软件产品的灵魂，软件质量的保障也因此变得尤为重要。10月22日，以“形式化验证”为主题，由中车株洲电力机车有限公司举办的“2020软件质量提升交流会”在株洲市召开，浙江迪捷软件科技有限公司应邀参展并做主题报告。
什么是形式化验证？
形式化方法是建立在逻辑演算、形式语言、自动机理论、程序语义、类型系统等理论基础之上，对计算系统进行描述和分析的一系列符号与技术的集合。形式化方法可指导软/硬件系统的规约、设计和验证，是改善和确保计算系统质量的重要方法。历史上，形式化方法在硬件和协议验证方面取得过巨大成功。这种技术变革对未来软件产业，尤其是安全关键领域的软件研发必将产生深刻的影响，对我国工业设计软件领域而言既是新一轮难得的机遇，同时也充满了挑战。我国在高端装备制造业的核心工具软件方面长期受制于人，能否借此新的机遇摆脱困局？迪捷软件创始人康烁先生在报告中作出了自己预判。康烁先生介绍了迪捷软件在编译器形式化验证方面的成果，我司已自主研发了一款基于Lustre的语言到C语言的可信编译器——L2C，是形式化验证的代码生成工具ModelCoder的核心技术。
ModelCoder是什么
迪捷软件的形式化验证的代码生成工具ModelCoder软件研发项目正式启动于2010年9月， 目前已在国内核电领域的得到应用，我们正在抓紧研发更适应国内其他关键领域（航空、航天、轨道交通等）需求的通用可信编译器以及相关配套工具（静态分析/仿真/调试/WCET分析/图形语言等）。与Scade工具相比，ModelCoder及L2C编译器在成熟度以及源语言表达能力方面虽尚有不足，但从形式化方法应用的角度来看，二者各有千秋。Scade基于模型检查实现了较强的源程序静态分析功能，这是L2C目前尚未涉足的领域。L2C基于定理证明对完整的代码生成过程进行了形式化验证，而Scade代码生成器的可靠性保障则一直依赖于测试与过程管理等传统方法。从目前的实际效果来看，L2C产品的推进与实施，结束了Scade在合作企业（之前也是Scade客户）上的业务渗透。
