本發(fā)明涉及一種基于AADL模型擴(kuò)展的軟件系統(tǒng)安全性驗(yàn)證與評估方法，是為了解決現(xiàn)有的基于AADL模型的驗(yàn)證評估很難對系統(tǒng)模型進(jìn)行直接處理，需要付出巨大計算代價，且計算中蘊(yùn)含大量冗余的缺點(diǎn)而提出的，包括：使危險因素與AADL架構(gòu)模型建立聯(lián)系，形成機(jī)理生成模型；提取模型元素并根據(jù)模型元素生成時間狀態(tài)故障樹、硬件軟件影響分析樹以及共因時效分析樹，并根據(jù)樹形結(jié)構(gòu)自底向上逆推危險產(chǎn)生路徑；設(shè)置每個物理器件的物理資源的性能與容量；并根據(jù)標(biāo)注好的物理器件的危險因素概率來計算所述物理器件的失效概率；將AADL安全性模型轉(zhuǎn)換為時間自動機(jī)模型；調(diào)用形式化驗(yàn)證工具UPPAAL對所述時間自動機(jī)模型進(jìn)行分析和驗(yàn)證；本發(fā)明適用于軟硬件系統(tǒng)的安全性評估。