计算机工程

作者：闫倩倩, 缪炜恺

单位：华东师范大学 上海市高可信计算重点实验室, 上海 200062

关键词：形式化方法,需求规约,需求确认和验证,场景优化,轨道交通控制软件

基金：国家自然科学基金面上项目“数据驱动的机器学习软件系统的形式化需求建模工程方法”（61872144）；国家自然科学基金青年基金“嵌入式控制软件的形式化规格说明构建的工程方法”（61402178）。

针对轨道交通控制软件的形式化方法，在实际工程应用中存在形式化建模和系统级场景验证困难的问题。提出一种面向轨道交通领域的形式化建模和需求确认及验证方法。通过非形式化、半形式化到形式化规约三步演化过程，为形式化规约构建提供模板。在对需求的确认和验证中，根据形式化规范建立需求模型，导出相关图表，基于此检查领域专家关注的场景。同时制定场景描述规则，使场景可以在需求模型中正确执行。在此基础上，从特殊变量、效率、场景质量三方面对场景进行优化，更充分地验证需求的正确性。实验结果表明，对于典型车载控制软件，该方法较传统分析方法可多探测到10%的潜在缺陷，效率提升80%以上。

来源：2021年第8期

《计算机工程》期刊编辑部

查看计算机工程杂志2021年第8期