Behavioral Modeling And Model Conversion Technology Of Embedded Software

With the increasing scale and complexity of embedded software,considering the requirements of non-functional properties such as security,real-time and reliability,the traditional software development method and the code-based development method are facing real challenge.The model-based software development has become a major approach in the field of embedded software development.Taking into account the requirements of non-functional properties of embedded software,it is necessary to have an effective way to analyze and verify the model in order to improve the reliability of the software and to ensure the correctness of the design.Based on the modeling language SmartC,this paper proposes the definition of behavior model for RTESIDDVL,which is a more powerful modeling language,and gives the transformation of behavior model to time automata model,And analyzes the verification of the time automaton model.So the main work of this paper is as follows:(1)Define the behavior model for The RTESIDDVL modeling language.After analyzing the conceptual characteristics of the behavioral model and the relationship with the structural model,the grammar of the behavioral model is given,which includes the components of the behavioral model and the expression of the graphic and the text for each component.(2)A transformation method of behavior model to time automaton model is proposed.Compared with other methods to improve software reliability,such as test and theorem proofing,Model checking has many irreplaceable advantages.Therefore,this paper defines the model from the behavior model to the timed automaton Model conversion rules,including the conversion between the corresponding elements,as well as the conversion process.Then the validation of the time automaton model after the behavior model transformation is given.(3)Finally,this paper presents a implement of model conversion tool.Through the analysis of the RTESIDDVL behavior model,Lex and Yacc are used to design thelexical and grammar files of the behavior model,and the rule actions of lexical and grammar are designed according to the conversion rules.Finally,a tool to convert a RTESIDDVL behavior model to a UPPAAL time automaton template is implemented.