嵌入式基于模型驅(qū)動(dòng)驗(yàn)證及軟件生產(chǎn)線的研究與實(shí)現(xiàn).pdf

1、隨著處理器的計(jì)算能力的迅速提高、嵌入式技術(shù)的迅猛發(fā)展和嵌入式系統(tǒng)應(yīng)用領(lǐng)域的不斷拓寬，使得嵌入式軟件的規(guī)模以及復(fù)雜性的不斷增長，從而導(dǎo)致了開發(fā)時(shí)間和費(fèi)用也在不斷的增長，如何快速有效的開發(fā)嵌入式軟件成為目前亟待解決的問題。為了解決上面的問題，全球最大的軟件工業(yè)標(biāo)準(zhǔn)化組織OMG(Object Management Group)提出了模型驅(qū)動(dòng)框架MDA(Model Driven Architecture)開發(fā)方法。MDA方法將軟件開發(fā)過程分成兩

2、個(gè)主要階段：模型級(jí)和代碼級(jí)。模型主要關(guān)注系統(tǒng)的設(shè)計(jì)正確性，從而達(dá)到以較小代價(jià)修改軟件錯(cuò)誤的目的。
　　 面向嵌入式軟件的開發(fā)工具目前正在從基于代碼的傳統(tǒng)開發(fā)環(huán)境向基于模型的開發(fā)環(huán)境發(fā)展。而一個(gè)基于模型的嵌入式生產(chǎn)線開發(fā)環(huán)境，應(yīng)該是集成模型開發(fā)工具和其他相關(guān)工具，包含了建模、模型仿真驗(yàn)證、代碼生成、測試等嵌入式軟件開發(fā)的全過程。這符合嵌入式軟件開發(fā)工具發(fā)展趨勢(shì)，也具備相應(yīng)的理論、技術(shù)和產(chǎn)品基礎(chǔ)。
　　 模型驅(qū)動(dòng)驗(yàn)證是基于模

3、型的嵌入式軟件生產(chǎn)線的一個(gè)重要部分，這個(gè)關(guān)鍵部分會(huì)影響到系統(tǒng)的質(zhì)量和后期的工作，如果在前期能夠及時(shí)發(fā)現(xiàn)出存在的問題，可以節(jié)省大量的人力物力。當(dāng)今主流的嵌入式實(shí)時(shí)系統(tǒng)中，實(shí)時(shí)性是一個(gè)關(guān)鍵的性能指標(biāo)，對(duì)于這類系統(tǒng)就是要求它們?cè)诤戏ǖ臅r(shí)間內(nèi)完成相應(yīng)的行為，不會(huì)發(fā)生超時(shí)現(xiàn)象，這就要求驗(yàn)證任務(wù)間的可調(diào)度性來判斷系統(tǒng)實(shí)時(shí)性是否符合要求。由Clark和Emerson提出形式化的模型驗(yàn)證的方法以開始應(yīng)用在任務(wù)的可調(diào)度分析上，該方法的基本原理是為要檢測的

4、系統(tǒng)建立形式化模型，闡明所要驗(yàn)證的性質(zhì)，然后使用算法去檢查該模型是否滿足所述性質(zhì)。
　　 本文的研究是基于模型的軟件嵌入式生產(chǎn)線開發(fā)環(huán)境，在這條主線上把重點(diǎn)放在研究和解決模型方面的形式化驗(yàn)證問題，對(duì)嵌入式模型實(shí)時(shí)性中的可調(diào)度問題進(jìn)行研究。
　　 論文先介紹了基于模型的嵌入式軟件生產(chǎn)線的背景與意義，并分析了國內(nèi)外的發(fā)展情況，接著說明課題的來源和本文研究的內(nèi)容；在此基礎(chǔ)上提出基于模型的嵌入式生成線的總體需求分析；接著重點(diǎn)介紹

5、模型驗(yàn)證調(diào)度檢測工具SCT(Scheduling CheckTool)的設(shè)計(jì)，包括SCT所分析的系統(tǒng)的相關(guān)定義和規(guī)定以及任務(wù)的兩個(gè)行為自動(dòng)機(jī)模型的設(shè)計(jì)實(shí)現(xiàn)，在這些前提下對(duì)SCT工具進(jìn)行總體設(shè)計(jì)，并對(duì)每部分進(jìn)行實(shí)現(xiàn)，其中重點(diǎn)放在調(diào)度仿真算法進(jìn)行設(shè)計(jì)與實(shí)現(xiàn)；接著在LambdaPRO的基礎(chǔ)上集成相關(guān)工具，實(shí)現(xiàn)基于模型的嵌入式軟件生成線的整個(gè)開發(fā)過程，并通過一個(gè)實(shí)例應(yīng)用來說明驗(yàn)證這個(gè)開發(fā)流程。論文最后對(duì)本文的工作進(jìn)行總結(jié)，并對(duì)后繼研究和發(fā)展進(jìn)行