本文選題：嵌入式軟件建模　切入點(diǎn)：模型轉(zhuǎn)換　出處：《浙江大學(xué)》2017年碩士論文

【摘要】：隨著嵌入式控制軟件的軟件規(guī)模與復(fù)雜度的不斷上升,考慮到嵌入式軟件對(duì)于安全性、實(shí)時(shí)性、可靠性等非功能屬性的要求,傳統(tǒng)的軟件開(kāi)發(fā)方法,以代碼為核心的開(kāi)發(fā)方法面臨著越來(lái)越多的困難,基于模型的軟件開(kāi)發(fā)方法成為了嵌入式軟件開(kāi)發(fā)領(lǐng)域的主要方式。這其中,考慮到嵌入式軟件的對(duì)非功能性屬性的要求,就必須要有一種有效的方式能夠?qū)δＰ瓦M(jìn)行分析與驗(yàn)證,以此提高軟件系統(tǒng)的安全性與可靠性。本文就是在這樣的背景下,在SmartC建模語(yǔ)言的基礎(chǔ)上,為實(shí)時(shí)嵌入式軟件一體化設(shè)計(jì)開(kāi)發(fā)與驗(yàn)證語(yǔ)言(RTESIDDVL)這個(gè)描述能力更強(qiáng)大的建模語(yǔ)言提出了行為模型的定義,并給出了 RTESIDDVL行為模型到時(shí)間自動(dòng)機(jī)模型的轉(zhuǎn)換方法,并對(duì)時(shí)間自動(dòng)機(jī)模型的驗(yàn)證進(jìn)行了分析。所以本文的工作主要如下:(1)為RTESIDDVL建模語(yǔ)言提出了行為模型的定義。在分析了行為模型的概念特點(diǎn),以及與結(jié)構(gòu)模型的關(guān)系之后,給出了行為模型的語(yǔ)法定義,包括了行為模型的各個(gè)組成部分,以及各個(gè)組成部分的圖形與文本兩種方式的表達(dá)。(2)提出了 RTESIDDVL行為模型到時(shí)間自動(dòng)機(jī)模型的轉(zhuǎn)換方法。模型驗(yàn)證對(duì)于基于模型的開(kāi)發(fā)方法來(lái)說(shuō)必不可少,相比于其他提高軟件可靠性的方式,如測(cè)試、定理證明等具有各種不可替代的優(yōu)勢(shì),所以本文定義了由行為模型到時(shí)間自動(dòng)機(jī)模型轉(zhuǎn)換的規(guī)則,包括了各個(gè)元素之間的轉(zhuǎn)換,以及轉(zhuǎn)換流程。然后對(duì)行為模型轉(zhuǎn)換之后的時(shí)間自動(dòng)機(jī)模型的驗(yàn)證給出了分析。(3)最后本文給出了一個(gè)模型轉(zhuǎn)換工具的實(shí)現(xiàn)。通過(guò)使用Lex與Yacc這兩個(gè)工具,經(jīng)過(guò)對(duì)RTESIDDVL行為模型的分析,設(shè)計(jì)了行為模型的詞法與語(yǔ)法文件,并根據(jù)轉(zhuǎn)換規(guī)則對(duì)詞法與語(yǔ)法的規(guī)則動(dòng)作進(jìn)行了設(shè)計(jì)。最終通過(guò)這兩個(gè)工具實(shí)現(xiàn)了一個(gè)RTESIDDVL行為模型到UPPAAL時(shí)間自動(dòng)機(jī)模板的轉(zhuǎn)換工具。
[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.
【學(xué)位授予單位】：浙江大學(xué)
【學(xué)位級(jí)別】：碩士
【學(xué)位授予年份】：2017
【分類號(hào)】：TP311.52

【參考文獻(xiàn)】

相關(guān)期刊論文 前2條

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

2 薛振偉;吳志杰;;模型驅(qū)動(dòng)的軟件開(kāi)發(fā)模式研究[J];計(jì)算機(jī)技術(shù)與發(fā)展;2008年02期

相關(guān)博士學(xué)位論文 前1條

1 楊國(guó)青;基于模型驅(qū)動(dòng)的汽車電子軟件開(kāi)發(fā)方法研究[D];浙江大學(xué);2006年

，

本文編號(hào)：1724087