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