Z語言的實(shí)時(shí)擴(kuò)展及應(yīng)用.pdf

1、實(shí)時(shí)軟件系統(tǒng)在現(xiàn)代工業(yè)和社會生活中扮演著越來越重要的角色,隨著需求的逐步增加,實(shí)時(shí)系統(tǒng)的軟件開發(fā)方法學(xué)漸漸成為研究的熱點(diǎn)問題.形式化方法在實(shí)時(shí)系統(tǒng)的開發(fā)過程中的使用也越來越多,Z語言是一種廣泛應(yīng)用的形式化規(guī)格說明語言,然而,它并不是為處理系統(tǒng)的動態(tài)行為而設(shè)計(jì)的,因此對Z進(jìn)行擴(kuò)充以適應(yīng)實(shí)時(shí)應(yīng)用的需要是非常重要的.在該文,我們歸納了Z實(shí)時(shí)擴(kuò)展,提出了分類標(biāo)準(zhǔn),一類是被稱為集成的擴(kuò)展方法,它基于形式化說明語言Z和其它形式化方法的集成,在這里由

2、其它形式化方法提供表示動態(tài)行為的結(jié)構(gòu);另一類稱之為非集成的擴(kuò)展方法則只使用Z的語義,而由其它形式化方法對時(shí)間約束性和并發(fā)進(jìn)行的描述則被轉(zhuǎn)換成Z規(guī)格說明,完成了上述分析之后實(shí)際就給出了一個(gè)對Z進(jìn)行實(shí)時(shí)擴(kuò)展的通用方法.一種被稱為RT-Z的基于規(guī)格描述語言Z和timed CSP的實(shí)時(shí)擴(kuò)展是集成擴(kuò)展方法的典型代表,RT-Z將Z和timed CSP的功能用一個(gè)緊密的框架結(jié)合起來,實(shí)際上無論是Z還是timed CSP都缺乏對結(jié)構(gòu)化的支持機(jī)制,為了能

3、適應(yīng)系統(tǒng)復(fù)雜性的需要,RT-Z另外引入了對結(jié)構(gòu)化的支持機(jī)制.RT-Z的語義基于Z和timed CSP,這是它具有正確性和數(shù)學(xué)嚴(yán)格性的基礎(chǔ).RT-Z可以用于需求描述,也可以用于設(shè)計(jì)階段,非常適合于實(shí)時(shí)系統(tǒng)的開發(fā).另一方面,使用過程描述語言可以方便的描述時(shí)序關(guān)系,在該文中,我們也討論了這種非集成的擴(kuò)展方式,它能夠利用時(shí)序狀態(tài)轉(zhuǎn)換系統(tǒng)將過程描述語言轉(zhuǎn)換為Z規(guī)格.通常,實(shí)時(shí)系統(tǒng)開發(fā)依賴于時(shí)間約束性和復(fù)雜的外部因素,因此無論是采用Z和timed

4、CSP集成還是使用規(guī)格描述語言轉(zhuǎn)換的非集成方法都不能很好地解決系統(tǒng)設(shè)計(jì)的所有問題,因此在實(shí)時(shí)系統(tǒng)設(shè)計(jì)中選擇合適的方法是非常重要的.經(jīng)過進(jìn)一步研究,我們在微機(jī)仿真系統(tǒng)的設(shè)計(jì)過程中提取了通用的設(shè)計(jì)模式,這個(gè)模式基于多視點(diǎn)的軟件工程方法,采用集成方法從功能視點(diǎn)得到的規(guī)格說明和采用非集成方法從控制視點(diǎn)得到的規(guī)格說明在一個(gè)統(tǒng)一的語義下結(jié)合起來,這樣就可以利用兩種規(guī)格說明方法直接得到在語法和機(jī)制上一致的規(guī)格說明,因此可以避免單獨(dú)使用兩種方案所產(chǎn)生的