SLDDS問(wèn)題的離散化與形式化.pdf

1、程序正確性驗(yàn)證不僅是計(jì)算機(jī)科學(xué)界一直關(guān)注的一個(gè)重要問(wèn)題，也是推動(dòng)計(jì)算機(jī)科學(xué)發(fā)展的主要?jiǎng)恿χ?。分離邏輯是此問(wèn)題研究下出現(xiàn)的新研究領(lǐng)域，它是一個(gè)用來(lái)對(duì)關(guān)于共享可變數(shù)據(jù)結(jié)構(gòu)的程序進(jìn)行推理的邏輯系統(tǒng)，其主要的特征是支持局部推理。 時(shí)段演算是一個(gè)用于嵌入式實(shí)時(shí)軟件系統(tǒng)設(shè)計(jì)的演算系統(tǒng)，即在設(shè)計(jì)嵌入式實(shí)時(shí)軟件系統(tǒng)時(shí)，用該形式語(yǔ)言來(lái)描述軟件需求和特征，并且通過(guò)推理驗(yàn)證來(lái)保證最終的軟件產(chǎn)品是否滿足這些需求和具備這些特征。 當(dāng)前對(duì)實(shí)時(shí)任務(wù)調(diào)

2、度理論的研究很少考慮到空間的約束，往往只考慮實(shí)時(shí)限制，但在許多實(shí)際問(wèn)題中，（比如鐵路交叉口控制、網(wǎng)絡(luò)服務(wù)的擁塞問(wèn)題、城市交通的指揮問(wèn)題、軟件系統(tǒng)資源共享問(wèn)題等等）中，空間是一個(gè)不可忽視的因素。時(shí)段演算是規(guī)約實(shí)時(shí)系統(tǒng)的一個(gè)強(qiáng)有力工具，然而它幾乎沒(méi)有考慮空間因素；分離邏輯較好地解決了空間共享問(wèn)題，但它不能夠較好地解決并發(fā)程序的同步問(wèn)題。由此，在時(shí)段演算中引入空間概念顯得極為必要，我們采用的方法是在時(shí)段演算中引入空間變量，這為我們規(guī)約實(shí)時(shí)問(wèn)題

3、中的空間共享與空間分離提供了方便。 本文從一些現(xiàn)實(shí)問(wèn)題的背景中抽象出SLDDS模型，并研究此模型里的調(diào)度問(wèn)題，最后考慮這個(gè)模型的形式化問(wèn)題。 本文的主要內(nèi)容安排如下： 序言，介紹分離邏輯，時(shí)段演算的研究現(xiàn)狀和本文的出發(fā)點(diǎn)。 第1章介紹基礎(chǔ)分離邏輯。 第2章介紹時(shí)段演算。 第3章先將DDS模型擴(kuò)充為更一般的SLDDS問(wèn)題，重新審視Liu-Layland定理，給出此類(lèi)實(shí)時(shí)問(wèn)題離散化的理論基礎(chǔ)，

4、然后研究SLDDS模型里的調(diào)度問(wèn)題。 第4章先介紹我們所要用到的語(yǔ)言，然后初步給出該模型的形式化。 本文主要理論結(jié)論如下： 定理1 給定一個(gè)SLDDS問(wèn)題Q，Q是可調(diào)度的當(dāng)僅當(dāng)存在對(duì)Q的一個(gè)劃分： P1=⊕K1j=1 Pj1,P2=⊕k2j=1Pj2,…,Pm=⊕kmj=1pjm使得所有的長(zhǎng)條{di×ai│1≤i≤n}可以滿足如下要求放入長(zhǎng)方塊 D×1中： (ⅰ)所有長(zhǎng)條都是垂直而不重疊地；

5、(ⅱ)來(lái)自的任何兩個(gè)小長(zhǎng)條一個(gè)不能在另一個(gè)的上方，即對(duì)來(lái)自某個(gè)di×Wi的所有小長(zhǎng)條，通過(guò)長(zhǎng)方塊底邊上任何點(diǎn)的垂線至多穿過(guò)其中一個(gè)的中間。 定理2 SLDDS問(wèn)題Q有解的充要條件是存在[0,1] 上的一個(gè)階梯函數(shù)f(t)使: (ⅰ)(∨)t，t∈[0,1]，滿足f(t)≤│D│ (ⅱ)(∨)t，t∈[0,1],f(t)=∑ki=1δi,δi∈{d1,d2…dm} k∈N,這里f(t)=∑ki=1δi僅僅是一個(gè)符號(hào)表達(dá)