Behavioural Verification In Embedded Software, From Model To Source Code
Proceedings of the 16th International Conference on Model-Driven Engineering Languages and Systems - Volume 8107(2013)
摘要
To reduce the verification costs and to be more confident on software, static program analysis offers ways to prove properties on source code. Unfortunately, these techniques are difficult to apprehend and to use for non-specialists. Modelling allows users to specify some aspects of software in an easy way. More precisely, in embedded software, state machine models are frequently used for behavioural design. The aim of this paper is to bridge the gap between model and code by offering automatic generation of annotations from model to source code. These annotations are then verified by static analysis in order to ensure that the code behaviour conforms to the model-based design. The models we consider are UML state machines with a formal non-ambiguous semantics, the annotation generation and verification is implemented in a tool and applied to a case study.
更多查看译文
关键词
Verification,UML,Formal Methods,Model Driven Engineering
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络