嵌入式软件形式化建模方法

来源：计算机工程与应用杂志2018年第8期北京时间：

作者：潘 杰1，渡边政彦2，周宽久1，梁浩然1，崔 凯1

单位：1.大连理工大学 软件学院，辽宁 大连 116620 ；2.日本CATS株式会社，日本 横滨 222-0033

摘要：随着嵌入式系统在各行各业的普及，嵌入式系统也越来越复杂，为保证嵌入式系统正确性，研究从需求分析、系统设计到系统验证、代码自动生成统一建模方法尤为重要。针对以上问题，提出采用状态变迁矩阵（STM）对嵌入式软件进行建模，通过确认STM中的每个单元格保证软件的正确性，且在需求分析阶段更容易发现需求遗漏。针对单元格处理经常出现大量的逻辑判断问题，提出采用决策表（DT）模型对复杂多条件判断分支问题进行建模。在模型建立后进行验证，最后自动生成代码。通过对紧急制动控制建模实验，说明方法的正确性。

关键词：状态变迁矩阵,决策表模型,决策树,嵌入式系统,代码自动生成