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

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

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