基于UML與PVS的嚴格建模技術(shù)研究----嵌入式實時系統(tǒng)的嚴格建模.pdf

1、該文在已有研究基礎(chǔ)上提出了一種新方法用于嵌入式實時系統(tǒng)的嚴格建模.該文通過構(gòu)造面向?qū)ο笳Z言UML與形式化方法PVS之間的轉(zhuǎn)換橋梁,為嵌入式實時系統(tǒng)開發(fā)團隊提供了一個易用、可以實現(xiàn)模型階段驗證的軟件方法.該團隊包括UML建模人員以及形式化驗證人員,UML建模人員首先使用一種帶有擴展的UML子集對系統(tǒng)建立圖形表示的最初模型,然后使用轉(zhuǎn)換工具實現(xiàn)UML圖形到PVS規(guī)范語言的轉(zhuǎn)換,形式化驗證人員使用PVS驗證工具對規(guī)范進行驗證,達到嚴格建模的目

2、的.在UML建模方面,該文提出了使用類圖以及帶有時間擴展的狀態(tài)圖分別對系統(tǒng)的靜態(tài)、動態(tài)模型建模的策略,可以比較完整地表達模型的內(nèi)容,同時又有利于到形式化規(guī)范的轉(zhuǎn)換.該文選用PVS作為支持的形式化工具,PVS是一種通用的形式化方法,提供基于高階邏輯的規(guī)范語言,具有很強的描述能力,可實現(xiàn)對靜態(tài)、動態(tài)模型的描述;它集成了模型驗證(Model Checking)、定律證明(Theorem Proving)的工具支持,驗證能力強.該文對這種軟件方