AADL子集到TASM的轉(zhuǎn)換規(guī)則研究.pdf

1、隨著現(xiàn)代化的推進(jìn)，計(jì)算機(jī)軟件已廣泛應(yīng)用于航天航空、武器裝備、交通等安全攸關(guān)的系統(tǒng)中。由于在安全攸關(guān)實(shí)時(shí)系統(tǒng)中一個(gè)微小的邏輯錯(cuò)誤都有可能導(dǎo)致不可預(yù)見的災(zāi)難性后果，所以保證軟件系統(tǒng)的質(zhì)量成為了迫切的需求和挑戰(zhàn)。對(duì)安全攸關(guān)系統(tǒng)的建模、分析與驗(yàn)證成為了現(xiàn)在模型驗(yàn)證方向的研究熱點(diǎn)。
　　AADL語言即架構(gòu)分析和設(shè)計(jì)語言是一種支持模型工程設(shè)計(jì)的半形式化建模語言，能表示安全攸關(guān)實(shí)時(shí)系統(tǒng)的功能性需求與非功能性需求，并已發(fā)布了標(biāo)準(zhǔn)語言庫。但由于AA

2、DL語言的復(fù)雜性和半形式化語言的特性，所以對(duì)AADL子集的提取與AADL子集的形式化轉(zhuǎn)換是我們急需解決的問題。TASM是一種形式化語言，能很好的描述AADL模型的功能性行為和非功能性（時(shí)間執(zhí)行、資源消耗等）行為;并能通過簡單的轉(zhuǎn)換運(yùn)行到驗(yàn)證和仿真工具上（如UPPAAL，TASM ToolSet等），對(duì)AADL模型進(jìn)行正確性、一致性以及可調(diào)度性等非功能性驗(yàn)證。
　　為了實(shí)現(xiàn)對(duì)安全攸關(guān)實(shí)時(shí)系統(tǒng)的軟件部分的AADL建模驗(yàn)證與分析，本文選

3、取了一種AADL子集并對(duì)子集進(jìn)行形式化轉(zhuǎn)換。主要工作如下:
　　首先，在AADL全集的基礎(chǔ)上，基于最小化原則、可實(shí)現(xiàn)性原則以及完備性原則選取了一種相對(duì)完整的AADL子集，并對(duì)AADL子集構(gòu)件進(jìn)行描述。
　　其次，實(shí)現(xiàn)AADL子集到TASM的形式化轉(zhuǎn)換，完成子集到TASM的轉(zhuǎn)換規(guī)則，并以偽代碼形式對(duì)規(guī)則進(jìn)行描述。轉(zhuǎn)換規(guī)則中設(shè)計(jì)了線程構(gòu)件內(nèi)的基于多級(jí)調(diào)度的調(diào)度協(xié)議轉(zhuǎn)換規(guī)則，實(shí)現(xiàn)多級(jí)調(diào)度模型的構(gòu)建。
　　最后，以ARINC6