嵌入式软件的行为建模与模型转换技术

发布时间：2018-04-09 00:34

本文选题：嵌入式软件建模　切入点：模型转换　出处：《浙江大学》2017年硕士论文

【摘要】：随着嵌入式控制软件的软件规模与复杂度的不断上升,考虑到嵌入式软件对于安全性、实时性、可靠性等非功能属性的要求,传统的软件开发方法,以代码为核心的开发方法面临着越来越多的困难,基于模型的软件开发方法成为了嵌入式软件开发领域的主要方式。这其中,考虑到嵌入式软件的对非功能性属性的要求,就必须要有一种有效的方式能够对模型进行分析与验证,以此提高软件系统的安全性与可靠性。本文就是在这样的背景下,在SmartC建模语言的基础上,为实时嵌入式软件一体化设计开发与验证语言(RTESIDDVL)这个描述能力更强大的建模语言提出了行为模型的定义,并给出了 RTESIDDVL行为模型到时间自动机模型的转换方法,并对时间自动机模型的验证进行了分析。所以本文的工作主要如下:(1)为RTESIDDVL建模语言提出了行为模型的定义。在分析了行为模型的概念特点,以及与结构模型的关系之后,给出了行为模型的语法定义,包括了行为模型的各个组成部分,以及各个组成部分的图形与文本两种方式的表达。(2)提出了 RTESIDDVL行为模型到时间自动机模型的转换方法。模型验证对于基于模型的开发方法来说必不可少,相比于其他提高软件可靠性的方式,如测试、定理证明等具有各种不可替代的优势,所以本文定义了由行为模型到时间自动机模型转换的规则,包括了各个元素之间的转换,以及转换流程。然后对行为模型转换之后的时间自动机模型的验证给出了分析。(3)最后本文给出了一个模型转换工具的实现。通过使用Lex与Yacc这两个工具,经过对RTESIDDVL行为模型的分析,设计了行为模型的词法与语法文件,并根据转换规则对词法与语法的规则动作进行了设计。最终通过这两个工具实现了一个RTESIDDVL行为模型到UPPAAL时间自动机模板的转换工具。
[Abstract]:With the increasing scale and complexity of embedded control software, considering the requirements of embedded software for security, real-time, reliability and other non-functional attributes, traditional software development methods,The development method based on code is facing more and more difficulties, and model-based software development method has become the main way in the field of embedded software development.In order to improve the security and reliability of software system, there must be an effective way to analyze and verify the model considering the requirement of non-functional properties of embedded software.In this paper, on the basis of SmartC modeling language, this paper proposes the definition of behavior model for RTE IDDVL, which is a more powerful modeling language for the integrated design and verification of real-time embedded software.The transformation method from RTESIDDVL behavior model to time automaton model is given, and the verification of time automata model is analyzed.So the main work of this paper is as follows: (1) the definition of behavior model for RTESIDDVL modeling language is proposed.After analyzing the conceptual characteristics of the behavior model and its relationship with the structural model, the grammatical definition of the behavior model is given, which includes the components of the behavior model.The transformation method of RTESIDDVL behavior model to time automata model is proposed.Model verification is essential for model-based development, and has irreplaceable advantages over other ways to improve software reliability, such as testing, theorem proving, etc.So this paper defines the transformation rules from the behavior model to the time automata model, including the transformation between the elements and the transformation process.Then, the verification of the time-automata model after the behavior model transformation is analyzed. Finally, the implementation of a model transformation tool is given in this paper.By using Lex and Yacc, the lexical and grammatical files of the behavior model are designed through the analysis of the RTESIDDVL behavior model, and the regular actions of lexical and grammatical are designed according to the transformation rules.Finally, a transformation tool from RTESIDDVL behavior model to UPPAAL time automata template is implemented by these two tools.
【学位授予单位】：浙江大学
【学位级别】：硕士
【学位授予年份】：2017
【分类号】：TP311.52

【参考文献】