Computer Engineering and Applications ›› 2018, Vol. 54 ›› Issue (8): 61-71.DOI: 10.3778/j.issn.1002-8331.1701-0259

Previous Articles     Next Articles

Formal modeling approach for embedded software

PAN Jie1, WATANABE Masahiko2, ZHOU Kuanjiu1, LIANG Haoran1, CUI Kai1   

  1. 1.School of Software, Dalian University of Technology, Dalian, Liaoning 116620, China
    2.CATS Co., Ltd., Yokohama 222-0033, Japan
  • Online:2018-04-15 Published:2018-05-02

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

潘  杰1,渡边政彦2,周宽久1,梁浩然1,崔  凯1   

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

Abstract: With the popularization of embedded systems in all walks of life, embedded systems are becoming more and more complicated. In order to ensure the correctness of embedded systems, it is very important to study from the requirements analysis, system design to system verification and code generation. To solve these problems, the STM modeling approach, confirming in every cells in STM to ensure software correctness, for embedded software is proposed. In this way, requirement analysis phase is more likely to find omission of demand. Aiming at the plenty of the logical judgment problem when dealing with cells, the decision table model is adopted to tackle the complex multi-condition judgment problem. After building and verifying the model, the code can be automatically generated. The correctness of the method is proven by the experiment of emergency braking control.

Key words: state transform matrix, decision table model, decision tree, embedded system, code automatic generation

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

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