摘要：運(yùn)用形式化方法建模在軟件開發(fā)過程中可提高目標(biāo)系統(tǒng)的正確性和可靠性，在此提出了一種利用Z語言進(jìn)行語義分析的方法。該方法在序列圖Z規(guī)范的基礎(chǔ)上，用屬性集表示對(duì)象狀態(tài)，并將序列圖的上下文表示為Z形式約束，通過檢查上下文約束與對(duì)象狀態(tài)間的一致性對(duì)序列圖進(jìn)行語義分析。在此以一個(gè)基于學(xué)分制的排課系統(tǒng)為例，使用面向?qū)ο蟮男问揭?guī)格說明語言Z，描述了一個(gè)精確、完整的高校排課系統(tǒng)的形式化數(shù)學(xué)模型。過程顯示，該方法具有精確的描述性和很強(qiáng)的抽象性，能為軟件系統(tǒng)的開發(fā)和驗(yàn)證提供科學(xué)的框架。

關(guān)鍵詞：形式化方法；規(guī)格說明；Z語言；排課系統(tǒng)

中圖分類號(hào)：TP311-34文獻(xiàn)標(biāo)識(shí)碼：A文章編號(hào)：1004-373X(2012)12-0050-04