發(fā)布時間：2018-04-09 00:34

  本文選題：嵌入式軟件建模　切入點：模型轉換　出處：《浙江大學》2017年碩士論文

【摘要】：隨著嵌入式控制軟件的軟件規(guī)模與復雜度的不斷上升,考慮到嵌入式軟件對于安全性、實時性、可靠性等非功能屬性的要求,傳統(tǒng)的軟件開發(fā)方法,以代碼為核心的開發(fā)方法面臨著越來越多的困難,基于模型的軟件開發(fā)方法成為了嵌入式軟件開發(fā)領域的主要方式。這其中,考慮到嵌入式軟件的對非功能性屬性的要求,就必須要有一種有效的方式能夠對模型進行分析與驗證,以此提高軟件系統(tǒng)的安全性與可靠性。本文就是在這樣的背景下,在SmartC建模語言的基礎上,為實時嵌入式軟件一體化設計開發(fā)與驗證語言(RTESIDDVL)這個描述能力更強大的建模語言提出了行為模型的定義,并給出了 RTESIDDVL行為模型到時間自動機模型的轉換方法,并對時間自動機模型的驗證進行了分析。所以本文的工作主要如下:(1)為RTESIDDVL建模語言提出了行為模型的定義。在分析了行為模型的概念特點,以及與結構模型的關系之后,給出了行為模型的語法定義,包括了行為模型的各個組成部分,以及各個組成部分的圖形與文本兩種方式的表達。(2)提出了 RTESIDDVL行為模型到時間自動機模型的轉換方法。模型驗證對于基于模型的開發(fā)方法來說必不可少,相比于其他提高軟件可靠性的方式,如測試、定理證明等具有各種不可替代的優(yōu)勢,所以本文定義了由行為模型到時間自動機模型轉換的規(guī)則,包括了各個元素之間的轉換,以及轉換流程。然后對行為模型轉換之后的時間自動機模型的驗證給出了分析。(3)最后本文給出了一個模型轉換工具的實現。通過使用Lex與Yacc這兩個工具,經過對RTESIDDVL行為模型的分析,設計了行為模型的詞法與語法文件,并根據轉換規(guī)則對詞法與語法的規(guī)則動作進行了設計。最終通過這兩個工具實現了一個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

【參考文獻】

相關期刊論文 前2條

1 顧斌;董云衛(wèi);王政;;面向航天嵌入式軟件的形式化建模方法[J];軟件學報;2015年02期

2 薛振偉;吳志杰;;模型驅動的軟件開發(fā)模式研究[J];計算機技術與發(fā)展;2008年02期

相關博士學位論文 前1條

1 楊國青;基于模型驅動的汽車電子軟件開發(fā)方法研究[D];浙江大學;2006年

，

本文編號：1724087