在軟件的生命周期內(nèi)，從需求分析到軟件維護的任何階段，都可能存在漏洞。因此工程師們期望在軟件運行中盡可能早地（最好是在需求分析階段）檢測到錯誤。面對這樣的挑戰(zhàn)，本文提出一種用需求建模語言SPARDL用于為周期性控制系統(tǒng)建模。

　　SPARDL是一種用于控制系統(tǒng)的需求建模語言，尤其適用于基于模式的、有著混合的（連須的／離散的）狀態(tài)、有限的周期行為和通信特征的控制系統(tǒng)。在每個周期中，系統(tǒng)都會并且只會精確地處在一個模式下，它可以停留在這個模式或者根據(jù)它現(xiàn)在的狀態(tài)轉(zhuǎn)換到另一個模式。作為一個輕量級的形式化語言，SPARDL可以在需求階段消除不確定性，而這通常對于系統(tǒng)的正確性來說是一個挑戰(zhàn)。

　　Event-B是一個重量級的形式化語言，它基于傳統(tǒng)的謂詞演算和定理證明。在Event-B中，事件（event）足一個主要的特征，因此它非常適合用來為周期行為建模。另外，Event-B還支持逐步精化地建立系統(tǒng)模型。用戶可以在建模之初構(gòu)建一個粗略的原型，然后不斷地使用精化策略，使之成為一個更為復(fù)雜但實用的系統(tǒng)。在軟件開發(fā)模型中，增量開發(fā)是運用于復(fù)雜系統(tǒng)開發(fā)的常見方式，能夠極大地減少漏洞的出現(xiàn)。

　　Event-B中的精化機制使得在形式化的建模和分析中進行增量開發(fā)變得方便。本文首先根據(jù)基本需求建立一個粗略的SPARDL的Event-B模型，然后再根據(jù)更多的需求精化這個模型。用Event-B為SPARDL系統(tǒng)建模，可以在一定程度上用它對應(yīng)的Rodin平臺驗證控制系統(tǒng)的需求。