（計(jì)算機(jī)軟件與理論專業(yè)論文）一類對象petri網(wǎng)建模與驗(yàn)證方法研究.pdf

內(nèi)容摘要 一類對象p e 砸網(wǎng)建模與驗(yàn)證方法研究 內(nèi)容摘要 p e 砸網(wǎng)是一種既有直觀的圖形表示方式，又有嚴(yán)格數(shù)學(xué)理論基礎(chǔ)和多種分 析方法的建模工具。使用p e 砸網(wǎng)的分析方法可以刻畫系統(tǒng)的結(jié)構(gòu)，展現(xiàn)系統(tǒng)的 運(yùn)行機(jī)制，表示和分析系統(tǒng)的動(dòng)態(tài)行為。帶有對象的p e 研網(wǎng)( p n o ) 是將面向?qū)ο?方法和謂詞變遷網(wǎng)有機(jī)結(jié)合而定義的一種高級p e 砸網(wǎng)。因?yàn)閜 n o 在初始化和 驗(yàn)證具體系統(tǒng)時(shí)才構(gòu)建庫所的標(biāo)識(shí)關(guān)系，變遷的使能與對象狀態(tài)相關(guān)，并且變遷 的實(shí)施需要修改托肯和相關(guān)對象的屬性，因此不便于直接使用常規(guī)的分析技術(shù)驗(yàn) 證p n o 模型。 針對p n o 模型存在的分析驗(yàn)證問題，本文將時(shí)態(tài)邏輯引入p n o 模型，提出 了相應(yīng)的建模及驗(yàn)證方法。建模方法使用精確標(biāo)識(shí)p n o 描述系統(tǒng)體系結(jié)構(gòu)模型， 并通過時(shí)態(tài)邏輯定義模型上的需求和限制。驗(yàn)證方法使用s m v 工具驗(yàn)證p n o 模型和時(shí)態(tài)邏輯之間的一致性，該方法包括三個(gè)步驟。首先，根據(jù)s m v 的要求 在模型中增加與變遷有關(guān)的對象屬性，并根據(jù)增加的對象屬性細(xì)化變遷附加條件 函數(shù)和變遷實(shí)施處理函數(shù)。其次，使用時(shí)態(tài)邏輯公式描述系統(tǒng)的屬性。最后，通 過算法p n 0 2 s m v 將p n o 模型轉(zhuǎn)換成s m v 程序表示的有限變遷系統(tǒng)，以驗(yàn)證 有限變遷系統(tǒng)是否滿足系統(tǒng)屬性對應(yīng)的邏輯公式，從而確保了系統(tǒng)設(shè)計(jì)的正確 性。 本文將上述建模及驗(yàn)證方法應(yīng)用在列車運(yùn)行模型( t o i p n o ) 上，通過在某一列 車運(yùn)行區(qū)域和列車運(yùn)行圖實(shí)例上的應(yīng)用表明：使用本文提出的建模及驗(yàn)證方法可 以在系統(tǒng)開發(fā)過程的更早階段揭示潛在的問題，確保系統(tǒng)設(shè)計(jì)的正確性，從而實(shí) 現(xiàn)系統(tǒng)設(shè)計(jì)和分析驗(yàn)證之問的高度完整性。 關(guān)鍵字：帶有對象的p e 城網(wǎng)，列車運(yùn)行p n o 模型，s m v ，建模，驗(yàn)證 t 內(nèi)容摘要一類對象p 靠i 網(wǎng)建模與驗(yàn)證方法研究 a b s t r a c t p e 砸n e t sa sam o d e l i i 培t o o lh a v et h ep r o p e n i e so f v i s u a l 口a p l l i c a lr 印r e s c n t a t i o 瑪 s m c tm 址e 缸l a t i c a lm e o r y 齟dm 山t i p l ew o r k d b l e 缸a 1 ) r t i c a lt e c 眥q u e s u s i n gt h e s e a n a l y t i c a lt e 涮q u e s ，w ec a nd e s c r i b e 血es y s t 咖ss m l c t u r e ，r e v e a lt h es y s t e m s 叩e 豫t i 】唱m e c h a l l i 鋤，i n d i c a t ea n d 卸a l y z em es y s t e m i sd y n a m i cb e h a v i o r s t h ep 酬 n e tw i t ho b j e c t s ( p n o ) i sak i n do fh i 曲一1 c v dp e 砸n e tw h i c hi n t e 斟a t e sm c o b j c c t 枷e n t e da p p r o a c ha n d1 l l ep r e d i c 鼬s i t i o nn e t s t h er d a t i o n s h i p sb c t w e e n p n o t sp l a c c sa r ec o n s 協(xié)l 曲e dw h e ni i l i d a l i z i i l ga n dv 甜劬n gap a n i c u l a rs y s t e m ， w t l i l om ee 1 1 a b l ec o n d i t i o i l so fa 蛔n s i d o na r ec o n c 帥e dw 濁s t a t e sa n dt u p l e so f o b j e c t s 鋤dt h e 鼬i n go fa 婦l s i t i o n 晰l lm o d i 母t h ep r o p 訓(xùn)e so f t o k e na 1 1 dr e l a t c d o b j e c t s f o ra 1 1f e a 如r c sa b o v ei ti si m p o s s i b l et ov e r i 母t o p n ou s i n go r d i n a r y a i l a l y t i c a lt e c h l l i q u c sd i r e c t l y a i l l l i n ga t 曲ep r o b l 鋤so f v e r i 螄n gp n 0 ，t l l i sp 印e ri n 吶d u c e st e i n p o r a ll o 番ct o p n 0m o d e la n dp r e s e i l t sam o d d i n ga i l dv 嘶聊n gm e t t l o db a s e do np n o 、i m p r e c i s em a r k i n g t h em o d e l i n gm e t h o dd e f i n e sm ed e c i s i o n sa b o u “h ea r c h i t e c t u t eo f as o f t w a r es y s t e mw i t hp e 砸n c t s ，a 1 1 ds p e c 墑e st h er e q u i r e m 髓t sa n dc o n s t r a i n t s i m p o s e do n l es o r w a r ea f c l l i t e c t l l r 。w i t l lt 鋤p o m ll o 百c t h ev e r i f m n gm e m o d v 酬6 e sm ec o n s i s t c n c yb 計(jì)吣e nt l l ep n o 鋤dt l l et 鋤p o r a l l o 百cf o 腫u l ab a s e do n s y m b 0 1m o d dc h e c k ( s m v ) 1 kv 謝助n gm e m o dc o n s i s t so f 恤e es t 印s t ob 哂n ， t h em c t h o de x t c n d st 1 1 ec l 船sp r o p e r t i e sr e l a c e dt ot l l em m s i t i o n ，a i l dr e f i n e st h ee x t m c o n d 謝o nf l m c t i o n sa 1 1 dm et r e a 咖e n t 如n c t i o n sa c c o r d i n gt ot 1 1 ee x t e n d e dp m p e m e s f u r t h 黜o r e 也em e m o dd e s c r i b e st l l ep r o p e r t i e so f p n om o d e lu s i n gt e i i l p o r a ll o 百c f i n a l l y ，也em 咖o dt r a i l l s f h sm ep n oi n t oa 矗n i t es t a t ct r i m s i t i o ns y s t 啪o fs m v p r o g r a mt h m u 曲a na l g o r i t l 蚰p n 0 2 s m vf o rv 喇聊n gw h e t l l c rt h ef i n i t es t a t e 打a n s i d o ns y s t e ms a t i s f i e st l l et 鋤p o r a ll o 舀cf o m m l aw h i c hd c l l o t c st h es y s t e m s p r 叩e m e s ，t h u sc l l s u r e st h ec 0 h 弓c n l e s sa tt l l es p e c i f i c a t i o nl e v e l u s i n gt h ep r o p o s e dm d h o d ，t h i sp 印e rv 舐f i c s 也ec o n s i s t e n c yb e t w e e n 也et r a i n 0 p e r a d o np e 讎n e tw i mo b j e c t s ( t o p n o ) a l l di t sp r o p e n i e s n e 鋤p m c a l r e s u l t s o nt l ec a s eo far a i l w a yn e t w o r ka 1 1 dat r a i no p e r a t i o nc h a r ts h o wt 1 1 a tt h ep r o p o s e d m e m o di sc 印a b l eo fr e v e a l i 芏1 9p o t e n t i a lp r o b l c m sa tar n u c he a r l i c rs t a g ei nt h e s y s t e md e v d o p m e n tp r o c e s sa 1 1 de n s u r i n gm ec o i t e c t n e s sa tm es p e c m c a t i o n1 e v d n u sah i 曲d e 留r e eo f 礎(chǔ)e 鰣t yi nd e s i 朗a n dv e r i f i c a t i o ni sa c h j e v e d k e y w o r d s ：p e mn e t s 謝t h0 b j e c t s ，t r a i no p e r a t i 徹p e 砸n e t 麗t l lo b j c c t s ，s m v m o d e l i n g ，v 耐f y 鄭重聲明 奉學(xué)位論文是在導(dǎo)師指導(dǎo)下獨(dú)立撰寫并完成的。除文中 已經(jīng)注明引用的內(nèi)容外，本論文不含任何其他個(gè)人或集體已 經(jīng)發(fā)表或撰寫過的作品或成果。學(xué)位論文沒有剽竊、抄襲等 違反學(xué)術(shù)道德、學(xué)術(shù)規(guī)范的侵權(quán)行為，否則，本人愿意承擔(dān) 由此產(chǎn)生的一切責(zé)任和法律后果。特此鄭重聲明。 第一章緒論一類對象p e 岍網(wǎng)建模與驗(yàn)證方法研究 第一章緒論 軟件的建模與驗(yàn)證是近幾年軟件工程領(lǐng)域最活躍的研究課題之一。本文將時(shí) 態(tài)邏輯引入p n o 模型，提出了相應(yīng)的建模及驗(yàn)證方法。其中，建模方法使用精 確標(biāo)識(shí)p n o 描述系統(tǒng)體系結(jié)構(gòu)模型，并通過時(shí)態(tài)邏輯定義模型上的需求和限制。 驗(yàn)證方法利用符號(hào)驗(yàn)證工具檢查p n o 模型和時(shí)態(tài)邏輯之間的一致性，以確保系 統(tǒng)設(shè)計(jì)的正確性。 1 1 形式化建模及驗(yàn)證方法的研究現(xiàn)狀 目前軟件系統(tǒng)建模大都采用圖形化語言從宏觀上刻畫系統(tǒng)的模型結(jié)構(gòu)，而在 某些局部使用自然語言或半形式化語言。這種建模方法比較宜觀、易于理解、便 于表達(dá)和使用。但是，采用圖形化語言構(gòu)筑的模型往往存在難以發(fā)現(xiàn)的模糊性或 歧義性等問題，而這些問題將直接影響系統(tǒng)的安全性與可靠性。形式化方法能在 早期發(fā)現(xiàn)系統(tǒng)描述中不一致、不明確或不完整之處，有助于增加軟件開發(fā)人員對 系統(tǒng)的理解，己被證明是一種行之有效的減少設(shè)計(jì)錯(cuò)誤、提高軟件系統(tǒng)可靠性的 重要途徑。 所謂形式化方法，是指建立在邏輯、代數(shù)、自動(dòng)機(jī)、圖論等數(shù)學(xué)基礎(chǔ)上的軟 件開發(fā)方法，它通過揭示系統(tǒng)的不一致性、二義性及不完全性，使軟件系統(tǒng)具有 較高的可信度和正確性，并能使系統(tǒng)具有良好的結(jié)構(gòu)，能較好地滿足用戶要求 【lj ”。形式化方法的重要研究內(nèi)容是形式規(guī)約和形式驗(yàn)證。形式規(guī)約是對程序“做 什么”的數(shù)學(xué)描述，它通過具有精確語義的形式語言描述程序的功能，是設(shè)計(jì)和 編寫程序的出發(fā)點(diǎn)，也是驗(yàn)證程序正確與否的依據(jù)。形式驗(yàn)證用來分析己有系統(tǒng) 是否滿足形式規(guī)約的要求，是形式化方法所要解決的核心問題。基于邏輯和基于 圖論的方法是當(dāng)前常用的兩類形式化方法。 基于邏輯的形式化方法使用邏輯描述程序行為的低級規(guī)范、使用與時(shí)間相關(guān) 的行為規(guī)范描述系統(tǒng)特性。常用的邏輯方法有基于線性時(shí)態(tài)邏輯( l i 媳a r1 1 e m p o r a l l o g i c ) 的方法 3 _ 5 1 和基于分支時(shí)態(tài)邏輯( b m i l c h i n gt e m p o m ll o 百c ) 的方法m 1 兩類。 基于邏輯的分析方法能夠模擬系統(tǒng)的動(dòng)念現(xiàn)象，應(yīng)用公理的形式明確表達(dá)系統(tǒng)的 行為性質(zhì)。但是，基于邏輯的形式化方法主要針對系統(tǒng)運(yùn)行機(jī)制，不能很好地體 第一章緒論一類對象p e 岍網(wǎng)建模與驗(yàn)證方法研究 現(xiàn)系統(tǒng)的物理結(jié)構(gòu)；并且基于邏輯的形式化方法的描述與驗(yàn)證過程過于抽象，既 不便于系統(tǒng)結(jié)構(gòu)的設(shè)計(jì)和調(diào)整，也不易被系統(tǒng)的開發(fā)和應(yīng)用者掌握。 基于網(wǎng)絡(luò)的形式化方法根據(jù)網(wǎng)絡(luò)中的數(shù)據(jù)流給出系統(tǒng)模型及網(wǎng)絡(luò)各結(jié)點(diǎn)間 的轉(zhuǎn)換條件，包括謂詞變換網(wǎng)、p e 缸網(wǎng)等。目前，使用廣泛的網(wǎng)絡(luò)形式化方法 是p e 踴網(wǎng)睜“】。p e 缸網(wǎng)具有圖形的表示方式，能直觀地描繪系統(tǒng)的結(jié)構(gòu)特性， 比較容易學(xué)習(xí)和理解。p e 缸網(wǎng)還有一套成熟的數(shù)學(xué)理論工具，建立了許多分析 技術(shù)，包括可達(dá)性分析、不變量分析、保持特性的變換f 包括化簡) 、構(gòu)造理論、 形式語言理論、同步距離及網(wǎng)的分勰和等價(jià)。可以借助p e 缸網(wǎng)的描述形式表示 和分析系統(tǒng)的動(dòng)態(tài)行為性質(zhì)：借助p e t r i 網(wǎng)的代數(shù)分析技術(shù)刻畫系統(tǒng)的結(jié)構(gòu)，建 立狀態(tài)可達(dá)的線性系統(tǒng)關(guān)系；借助p c 仃j 網(wǎng)的圖分析技術(shù)展現(xiàn)系統(tǒng)的運(yùn)行機(jī)制、 分析系統(tǒng)的動(dòng)態(tài)行為；借助p e m 網(wǎng)的歸納分析技術(shù)縮小系統(tǒng)的可達(dá)狀態(tài)空間、 降低系統(tǒng)分析的復(fù)雜度。隨著p e 缸網(wǎng)技術(shù)的發(fā)展和完善，涌現(xiàn)出了多種擴(kuò)展的 p e 缸網(wǎng)形式，如著色剛、時(shí)間p e 砸網(wǎng)f 1 3 l 、對象網(wǎng)1 1 4 l 【1 5 】、隨機(jī)p e 仃i 網(wǎng)等， 使得p e m 網(wǎng)的模擬能力和分析能力不斷增強(qiáng)。 基于邏輯的形式化方法可以驗(yàn)證系統(tǒng)的屬性，但需要對系統(tǒng)進(jìn)行高級抽象， 不便于系統(tǒng)結(jié)構(gòu)的設(shè)計(jì)和調(diào)整，應(yīng)用范圍受到一定的限制。p c t r i 網(wǎng)方法既具有 嚴(yán)格的數(shù)學(xué)定義又具有可視的圖形描述，但不能很好地表達(dá)系統(tǒng)屬性。為了充分 利用這兩種形式化方法的優(yōu)點(diǎn)，同時(shí)避免其不足，在文獻(xiàn) 1 7 】中，用時(shí)序p e 讎 網(wǎng)描述和分析并發(fā)系統(tǒng)的時(shí)序性質(zhì)，并將時(shí)序邏輯引入p e 啊網(wǎng)，增加了p e t 訂網(wǎng) 的推理能力，使得p e 晡網(wǎng)能夠表達(dá)和驗(yàn)證系統(tǒng)的時(shí)序需求。在文獻(xiàn)【1 8 【1 9 1 【2 0 1 中提出的軟件體系結(jié)構(gòu)s a m 使用時(shí)問p e 砸網(wǎng)或謂詞變遷網(wǎng)來描述軟件體系結(jié) 構(gòu)，使用時(shí)態(tài)邏輯來描述系統(tǒng)屬性，通過檢查兩者的一致性確保軟件的正確性。 在文獻(xiàn) 2 l 】中討論了將時(shí)間p e 缸網(wǎng)轉(zhuǎn)換成時(shí)間自動(dòng)機(jī)( t i m c da u t o m a t a ) 的方法，從 而可以利用針對t a 的驗(yàn)證技術(shù)驗(yàn)證時(shí)間p e m 網(wǎng)。 本文提出的軟件建模和驗(yàn)證方法采用對象p c t i i 網(wǎng)描述系統(tǒng)體系結(jié)構(gòu)模型， 使用時(shí)態(tài)邏輯定義模型的需求和限制，并通過符號(hào)模型驗(yàn)證工具驗(yàn)證對象p e t r i 網(wǎng)和時(shí)態(tài)邏輯之間的一致性。體系結(jié)構(gòu)規(guī)定了系統(tǒng)的實(shí)現(xiàn)模式，系統(tǒng)需求和限制 說明了系統(tǒng)的正確性標(biāo)準(zhǔn)，因此檢查兩者的一致性能確保系統(tǒng)設(shè)計(jì)的正確性，并 能在系統(tǒng)開發(fā)過程的更早階段揭示潛在的錯(cuò)誤，從而實(shí)現(xiàn)系統(tǒng)設(shè)計(jì)和分析驗(yàn)證之 間的高度完整性。 第一章緒論一類對象p c 一網(wǎng)建模與驗(yàn)證方法研究 1 2 研究背景及意義 鐵路運(yùn)輸作為一種重要的運(yùn)輸方式，在我國國民經(jīng)濟(jì)中發(fā)揮著重要的作用。 鐵路系統(tǒng)的行車指揮人員設(shè)計(jì)列車的運(yùn)營方案、編制運(yùn)行計(jì)劃圖并檢驗(yàn)其合理 性。運(yùn)營方案和運(yùn)行計(jì)劃圖是否滿足各類安全限制和約束條件，能否在列車偏離 運(yùn)行圖時(shí)及時(shí)有效地調(diào)整，這些都需要計(jì)算機(jī)仿真技術(shù)給出答案【2 2 】。鐵路智能運(yùn) 輸系統(tǒng)( r i t s ) 已成為當(dāng)今世界上鐵路交通運(yùn)輸發(fā)展的前沿，它是通過高效利用與 鐵路運(yùn)輸相關(guān)的各類資源，以較低的成本達(dá)到保障安全、提高運(yùn)輸效率、改善經(jīng) 營管理和提高服務(wù)質(zhì)量目的的新一代鐵路運(yùn)輸系統(tǒng)【2 3 】【2 4 】。 在對鐵路智能運(yùn)輸系統(tǒng)進(jìn)行研究的過程中，應(yīng)用計(jì)算機(jī)建模仿真技術(shù)構(gòu)建相 應(yīng)的系統(tǒng)仿真實(shí)驗(yàn)平臺(tái)，不僅能節(jié)省大量人力、物力資源，保證鐵路運(yùn)營實(shí)旌的 安全性，也能為行車組織、運(yùn)營調(diào)整提供科學(xué)的決策支持：另一方面，面向?qū)嶋H 應(yīng)用問題的列車群運(yùn)行仿真系統(tǒng)為智能混雜系統(tǒng)建模和分析理論的研究提供了 有效的實(shí)驗(yàn)平臺(tái)。在鐵路運(yùn)輸領(lǐng)域，國外于7 0 年代就開始在和運(yùn)營相關(guān)的科研 工作中采用計(jì)算機(jī)仿真技術(shù)，最初的研究內(nèi)容主要集中在閉塞區(qū)段內(nèi)列車運(yùn)行和 調(diào)整情況的分析、線路通過能力的評估、通過能力瓶頸區(qū)段的識(shí)別、交會(huì)或越行 時(shí)列車優(yōu)先級的確定、投資分析等方面。 在我國鐵路科研領(lǐng)域，計(jì)算機(jī)系統(tǒng)建模仿真正逐漸得到重視，越來越多的科 研人員和工程設(shè)計(jì)人員開始認(rèn)識(shí)到在科研工作中采用這種現(xiàn)代化技術(shù)手段的重 要性。我國鐵路的列車種類繁多、線路形式多樣，且高、低速列車混跑運(yùn)行。因 此，建立不以任何具體路網(wǎng)為背景，具有良好普適性，可以用于我國任一鐵路區(qū) 段及有軌交通仿真評估的列車運(yùn)行仿真系統(tǒng)是非常必要的。已經(jīng)設(shè)計(jì)并實(shí)施的基 于對象p e 晡網(wǎng)、對象p e t d 子網(wǎng)和基于a g e n t 的g n e t 模型、基于模糊時(shí)間p e m 網(wǎng)等一系列列車群行為建模和仿真系統(tǒng)的研究【2 5 - 2 9 1 ，為鐵路智能運(yùn)輸系統(tǒng)中相關(guān) 問題的可靠性分析、資源的可利用性分析、系統(tǒng)運(yùn)營能力分析和響應(yīng)時(shí)問性能分 析奠定了良好的基礎(chǔ)。其中基于a g 翎t(yī) 的g - n e t 模型、基于模糊時(shí)間p e 砸網(wǎng)的 列車群行為模型已經(jīng)有了推理和驗(yàn)證算法，能夠?qū)α熊囘\(yùn)行過程的時(shí)間不確定性 問題進(jìn)行定量分析，驗(yàn)證列車運(yùn)行調(diào)整方案的可行性【3 0 l 。但帶有對象p e 缸網(wǎng)的 列車運(yùn)行模型t o p n o 還沒有有效的模型驗(yàn)證方法。本文將上述建模與驗(yàn)證方法 應(yīng)用在1 1 0 p n o 上，有效地實(shí)現(xiàn)了對t o p n o 模型中列車運(yùn)行的可達(dá)性、列車到 第一章緒論 一類對象p e 晡網(wǎng)建模與驗(yàn)證方法研究 站時(shí)聞、列車在站時(shí)間、列車交會(huì)等屬性的檢測驗(yàn)證，并可以根據(jù)需要方便地調(diào) 整列車運(yùn)行計(jì)劃并再次進(jìn)行驗(yàn)證，直至滿足所要求的系統(tǒng)屬性。通過在某一列車 運(yùn)行區(qū)域和運(yùn)行計(jì)劃上的應(yīng)用，該算法表現(xiàn)出分析比較全面、轉(zhuǎn)換簡便的特點(diǎn)。 1 3 本文的內(nèi)容與結(jié)構(gòu) 帶有對象的p e 砸網(wǎng)( p n o ) 將構(gòu)成p n 0 的最基本元素和系統(tǒng)的現(xiàn)實(shí)元素分離， 系統(tǒng)的對象實(shí)例僅作為網(wǎng)的托肯元素，在初始化和驗(yàn)證具體系統(tǒng)時(shí)才構(gòu)建模型中 庫所的標(biāo)識(shí)關(guān)系，變遷的使能條件和實(shí)施過程也較為復(fù)雜，到目前還沒有很好的 分析方法。為了解決p n o 模型特殊的屬性驗(yàn)證問題，本文基于時(shí)態(tài)邏輯驗(yàn)證擴(kuò) 展了p n o 模型中對象的屬性，細(xì)化了p n o 模型中與變遷實(shí)施相關(guān)的函數(shù)，進(jìn)而 提出了將p n o 模型轉(zhuǎn)換成對應(yīng)的s m v ( 符號(hào)模型驗(yàn)證工具) 程序從而對p n o 模型 進(jìn)行驗(yàn)證的算法p n 0 2 s m v 。通過在列車運(yùn)行p n o ( t o p n o ) 模型上的試驗(yàn)表明 該方法是有效的。 本文按照如下結(jié)構(gòu)組織。 第一章：緒淪。 第二章：相關(guān)知識(shí)。這一章主要介紹本文涉及到的相關(guān)理論。包括p e m 網(wǎng) 基本理論、常用p e 砸網(wǎng)分析驗(yàn)證工具、時(shí)態(tài)邏輯與符號(hào)模型驗(yàn)證工具s m v 等。 其中2 1 節(jié)介紹了基本p e 塒網(wǎng)理論，可達(dá)樹和矩陣方程分析方法的功能和限制； 2 2 節(jié)介紹了時(shí)態(tài)邏輯的概念及時(shí)態(tài)操作符；2 3 節(jié)介紹了常見的p e t r i 網(wǎng)專用分 析驗(yàn)證工具及模型驗(yàn)證工具s m v 的功能特點(diǎn)及其工作原理。 第三章：精確標(biāo)識(shí)p n o 的建模及驗(yàn)證方法。本章首先給出了精確標(biāo)識(shí)p n o 的定義；然后提出了基于驗(yàn)證擴(kuò)展p n o 模型屬性、細(xì)化附加條件函數(shù)c o n j 和 處理函數(shù)爿c f f d 的方法：在此基礎(chǔ)上提出將精確標(biāo)識(shí)p n o 轉(zhuǎn)換成對應(yīng)s m v 程 序以進(jìn)行分析驗(yàn)證擴(kuò)展精確標(biāo)識(shí)p n o 模型的算法p n 0 2 s m v ；最后是算法 p n 0 2 s m v 的說明。 第四章：將第三章提出的建模及驗(yàn)證方法應(yīng)用在列車運(yùn)行p n o ( t o p n o 、模 型上。首先基于驗(yàn)證擴(kuò)展了t o p n o 模型中對象的屬性，細(xì)化了t o p n o 模型中 與變遷實(shí)施相關(guān)的函數(shù)，并定義了控制模型中對象實(shí)例之間隸屬和約束關(guān)系的列 車運(yùn)行圖，進(jìn)而通過算法p n 0 2 s m v 將擴(kuò)展的t o p n o 模型轉(zhuǎn)換成對應(yīng)的 s m v ( 符號(hào)模型驗(yàn)證工具) 程序從而對t o p n o 模型進(jìn)行驗(yàn)證。使用該方法能驗(yàn)證 4 第一章緒論 一類對象p e 礬網(wǎng)建模與驗(yàn)證方法研究 t o p n 0 模型的以下屬性：列車運(yùn)行的可達(dá)性、安全性、列車到達(dá)時(shí)間、列車群 運(yùn)行過程中的列車交會(huì)。通過在某一列車運(yùn)行區(qū)域和運(yùn)行計(jì)劃上的應(yīng)用，該方法 表現(xiàn)出分析比較全面、轉(zhuǎn)換簡便的特點(diǎn)。 最后是總結(jié)與未來的工作。 第= 章相關(guān)知識(shí)一類對象p t i 網(wǎng)建模與驗(yàn)證方法研究 第二章相關(guān)知識(shí) p e 扛i 網(wǎng)既有直觀的圖形表示方式，又有成熟的數(shù)學(xué)理論工具和多種分析技 術(shù)。時(shí)態(tài)邏輯將時(shí)間因素引入普通邏輯，從而能處理含有時(shí)間信息的命題和謂詞。 在模型驗(yàn)證方法中，系統(tǒng)規(guī)范被描述成命題時(shí)態(tài)邏輯公式，系統(tǒng)被模型化為狀態(tài) 轉(zhuǎn)換系統(tǒng)，通過使用高效的搜索算法來判定規(guī)范是否在系統(tǒng)中成立。s m v 是一 個(gè)功能強(qiáng)大的符號(hào)模型驗(yàn)證工具，最初主要應(yīng)用于通訊協(xié)議和硬件系統(tǒng)的驗(yàn)證， 目前在p e m 網(wǎng)驗(yàn)證方面已展現(xiàn)出強(qiáng)大生命力。 2 1p e t r i 網(wǎng)理論 p e 缸網(wǎng)是一種以圖形形式研究系統(tǒng)組織結(jié)構(gòu)和動(dòng)態(tài)特性的理論”，出 c a p e 蛹先生于1 9 6 2 年在他的博士論文中提出。p e m 網(wǎng)理論既有直觀的圖形表 示方式又有嚴(yán)格的數(shù)學(xué)理論基礎(chǔ)和分析方法，支持系統(tǒng)模型各種性質(zhì)的分析和性 能的評價(jià)，能夠?qū)哂胁⑿? p a r a l l d i s m ) 、并發(fā)( c o n c u r r 鋤c y ) 、同步 ( s ”d 啪i l i z a t i o n ) 、資源共享( r e s o u r c cs h 耐n g ) 等特性的系統(tǒng)建立模型。p e t r i 網(wǎng)廣 泛應(yīng)用于軟件體系結(jié)構(gòu)、軟件工程、知識(shí)表達(dá)與推理、并行計(jì)算、網(wǎng)絡(luò)通信協(xié)議、 柔性制造系統(tǒng)的建模、分析、控制領(lǐng)域。 2 1 1 p e t r i 網(wǎng)的定義 下面給出p e t r i 網(wǎng)及相關(guān)定義【9 _ l “。 定義2 1p e 缸網(wǎng) p e t r i 網(wǎng)是一個(gè)三元組，尸 ( p ，乃一，相應(yīng)符號(hào)的含義如下： ( 1 ) 仁扣l 拙，拂) 為有限的庫所集： ( 2 ) 仁 f l ，龜，矗) 為有限的變遷集： ( 3 ) p n 嚴(yán)( 集合p 和集合丁不相交) ，p u 降( 集合p 和集合r 不同時(shí)為 空) ； ( 4 ) 埏( a 乃u ( a p ) ( 流關(guān)系僅存在元素p 和r 之間，f 中的元素稱為弧) ； ( 5 ) d o m ( d uc o d ( 叼叩u 玎不存在孤立元素，d o m ( d = 扛i 砂：0 ) 毋；c o d ( 叼= 洲砂：o ，功毋；攙 p ur 是網(wǎng)元素的集合) 6 第二章相關(guān)知識(shí)一類對象p e 耐網(wǎng)建模與驗(yàn)證方法研究 定義2 2 前置集和后置集 令p h 尸耳一是一個(gè)網(wǎng)，且z z 那么，工的前置集心和后置集d 分別 = 秒f d 力f ) ； 0 0 ) = 9 f 0 毋。 定義2 3p e 血網(wǎng)系統(tǒng)( 西 六元組乏( p ，強(qiáng)鞏誓) 是一個(gè)p e 砸網(wǎng)系統(tǒng)i 越當(dāng)且僅當(dāng)) ： ( 1 ) ( p ，z 抑是一個(gè)網(wǎng)； ( 2 ) 量：p 一 1 ，2 ，3 ，) 是庫所容量函數(shù)； ( 3 ) 肌f 一( 1 ，2 ，3 ，) 是弧權(quán)函數(shù)； ( 4 ) ：p 一 o ，1 ，2 ，3 ，) 是初始標(biāo)識(shí)，滿足：v p ：( 力型【) 。 ( 5 ) 函數(shù)肘：p 一 0 ，1 ，2 ，3 ，) 是毋拘標(biāo)識(shí)i m 坳p ：肘c 力型r p ) 。 在p e 硒網(wǎng)的圖形表示中，對于弧，f p 1 時(shí)，將 坳標(biāo)注在弧上。根 據(jù)足函數(shù)的取值可將p e t r i 網(wǎng)分為無界網(wǎng)和有界網(wǎng)，如果置可取m ，則p e 廿i 網(wǎng)是 定義2 4 變遷的使能和觸發(fā)( e n a b l i n ga n df 訊n 曲 乎c p ，正f ，彬墨) 是一個(gè)p e t r i 網(wǎng)系統(tǒng)。 ( 1 ) 一個(gè)變遷拒r 在標(biāo)識(shí)m 下是使能的， i 仃 v 口p ： ( 2 ) 變遷f 丁在標(biāo)識(shí)m 下是使能的，在f 觸發(fā)后產(chǎn)生一個(gè)新的后繼標(biāo)識(shí)塒， 凹可由下列方程給出：b p ：協(xié)) = 肘p ) 一阡協(xié)，0 + 職f ) ；實(shí)際上f 的觸 發(fā)僅對其前置集和后置集以0 、0 ( 0 中的“托肯”數(shù)量有影響。也可用下 i 坳) - 阡p ，o ，p 廈f ) 爐萑o ( f ) i j 坳) + 壩印) ， p o ( 力，p 芒“力 【 腳卜1 川卅職慨 p 喇n d ( f ) 廣 m ，其它l ( 3 ) 系統(tǒng)標(biāo)識(shí)m 經(jīng)過f 的觸發(fā)得到新的標(biāo)識(shí)m ，可以表示成 研f m 。 第二章相關(guān)知識(shí)一類對象p e 啊網(wǎng)建模與驗(yàn)證方法研究 2 1 2p e t r i 網(wǎng)基本性質(zhì)及分析方法 p e 晡網(wǎng)有一套成熟的數(shù)學(xué)理論工具，支持系統(tǒng)模型各種性質(zhì)的分析和性能 的評價(jià)。使用這些分析方法可以刻畫系統(tǒng)的結(jié)構(gòu)，展現(xiàn)系統(tǒng)的運(yùn)行機(jī)制，表示和 分析系統(tǒng)的動(dòng)態(tài)行為，降低系統(tǒng)分析的復(fù)雜度。 1 p e t r i 網(wǎng)的基本性質(zhì) p e 晡網(wǎng)的基本性質(zhì)主要體現(xiàn)在可達(dá)性、有界性、安全性和活性等方面，這 些性質(zhì)充分體現(xiàn)了系統(tǒng)性能、結(jié)構(gòu)和行為之間的對應(yīng)關(guān)系【9 】 1 0 1 。 定義2 5 可達(dá)性 對一個(gè)給定初始標(biāo)識(shí)即初始托肯( t o k e l l ) 標(biāo)識(shí)硒的p e 砸網(wǎng)( v 舶) ，可達(dá)集 r ( m ) 表示該p e 喇網(wǎng)在初始狀態(tài)標(biāo)識(shí)下，觸發(fā)所有變遷可到達(dá)的狀態(tài)標(biāo)識(shí) 集合。r ( 刪i ) 既取決于網(wǎng)的結(jié)構(gòu)，也取決于網(wǎng)的初始狀態(tài)標(biāo)識(shí)。直觀上看，一 個(gè)狀態(tài)標(biāo)識(shí)即托肯分布 矗為可達(dá)意味著，在給定的初始標(biāo)識(shí)下經(jīng)過有限次 變遷觸發(fā)到達(dá)托肯分布j 】l 矗。 定義2 6 有界性 p c 仃j 網(wǎng)( a 動(dòng)是盡有界的，i 行v m r u v 舶) ，b p ：朋p ) 蘭彤，其中 廳 1 ，2 ，3 ，) 。有界性意味著在所有可能的狀態(tài)標(biāo)識(shí)下，p e 晡網(wǎng)中庫所節(jié)點(diǎn)的托 肯數(shù)必為有界。 定義2 7 安全性 1 有界p e 砸網(wǎng)是安全的，它是一種晟為苛刻的有界性。如果在初始標(biāo)識(shí)的 任何可達(dá)集里，一個(gè)庫所的托肯數(shù)都不超過1 ，則稱該庫所都是安全的。如果一 個(gè)p e 砸網(wǎng)的每一個(gè)庫所都是安全的，則稱該p “網(wǎng)是安全的。 定義2 8 活性 如果從經(jīng)若干次變遷觸發(fā)到達(dá)的任一標(biāo)識(shí)尬，網(wǎng)中存在觸發(fā)序列使所有 變遷都能觸發(fā)，那么稱該p e 砸網(wǎng)( _ 嬲) 是活性的( 或者說，肘j 對來說是個(gè)活 性的標(biāo)識(shí)) 。 2 p e t r i 網(wǎng)的常用分析方法 p e m 網(wǎng)有一套成熟的數(shù)學(xué)理論工具，建立了許多分析技術(shù)，包括可達(dá)性分 析、不變量分析、保持特性的變換( 包括化簡) 、構(gòu)造理論、形式語言理論、同步 距離及網(wǎng)的分解和等價(jià)。使用這些分析方法可以刻畫系統(tǒng)的結(jié)構(gòu)，展現(xiàn)系統(tǒng)的運(yùn) 第二章相關(guān)知識(shí)一類對象p e 砸網(wǎng)建模與驗(yàn)證方法研究 行機(jī)制，表示和分析系統(tǒng)的動(dòng)態(tài)行為，降低系統(tǒng)分析的復(fù)雜度。 ( 1 ) 可達(dá)樹技術(shù) 從一個(gè)給定p e t i i 網(wǎng)的初始狀態(tài)j l 而出發(fā)，觸發(fā)使能變遷能得到多個(gè)新標(biāo)識(shí)， 從這些新標(biāo)識(shí)出發(fā)再次觸發(fā)使能變遷能得到更多的標(biāo)識(shí)。如此類推，可以得到由 p e 缸網(wǎng)可達(dá)標(biāo)識(shí)組成的可達(dá)樹?？蛇_(dá)樹的節(jié)點(diǎn)代表從初始標(biāo)識(shí)出發(fā)得到的所有 標(biāo)識(shí)，弧線代表觸發(fā)的變遷。 當(dāng)p e 缸網(wǎng)無界時(shí)，不可能得到p e 缸網(wǎng)的所有可達(dá)標(biāo)識(shí)。為了用有限的形式 表達(dá)有無限個(gè)狀態(tài)的系統(tǒng)的運(yùn)行情況，需要引入一個(gè)表示無界量的符號(hào)緲。具 有這樣的性質(zhì)：對于所有n ，n = 打m e c 0 n d ：s f t r n e x t j e c t t o na n dt r n e x t j e c t i o n p l n n t i m e = n m e n 故8 ) ：乃c “ 萬。加如押d 0 缸砌以) a n dn 以甜u 砌以= ( 3 ) 變遷處理函數(shù)彳c 打伽的細(xì)化 根據(jù)增加的對象屬性細(xì)化模型中變遷附加條件函數(shù)c b ”d ，如下所示： a c t i o n o ：t r c t r r e n t j 刪。薩s 銣碡n 刪帆h t j e c t i o 咖a n dt r s 搬r l j i m e = f 加8a 1 1 d 研f m 加= 什a i l d & 加加= 西。 a c l i o n t ：t r 叫r r e n u 塒蛀。艫妒a n d 西c t l r r e m j e c t i o 薩s e 觚dn s t 倪r f j i m e = 盯聊8a n d 打誼f m = 西a n d & f ，口加= z 卜。 第四章t o p n 0 的建橫與驗(yàn)證 一類對象p e 啊網(wǎng)建模與驗(yàn)證方法研究 一謝細(xì)) ：孤c 柳鑰。脅砌薩鋤d 弘刪 鉚坐伽礦a n d 鼴拋栩= 一a 1 1 d 弘s 肋脅w 薩功鉀口a 2 列車運(yùn)行圖 t o p n o 模型將構(gòu)成p n o 的最基本元素和路網(wǎng)元素分離；構(gòu)成路網(wǎng)的對象實(shí) 例由一系列醐t 。n 、脅加、c 豳n 等對象實(shí)例構(gòu)成；各實(shí)例之問存在一定的約 束關(guān)系。為了表示這些實(shí)例之間的隸屬和約束關(guān)系，本文定義了稱為列車運(yùn)行圖 的矩陣。 定義4 2 列車運(yùn)行圖 列車運(yùn)行圖是表示列車、站臺(tái)、區(qū)域?qū)ο髮?shí)例之間關(guān)系的矩陣。設(shè)t o p n o 模型中共有臺(tái)列車、m 個(gè)站臺(tái)、s 個(gè)運(yùn)行區(qū)域，列車運(yùn)行圖是一個(gè)+ 的矩陣，如下所示： 尸1 1 p 2 1 風(fēng)1 p 1 2 p 2 i p n 2 毖繁：般：糍1 p 2 p 2 m 1p 2 胛p 2 - m + s 島 p n mp n m 十、p n 塒+ 2 p m m + sj 列車運(yùn)行圖的每一行對應(yīng)一臺(tái)列車的運(yùn)行計(jì)劃，每一列對應(yīng)一個(gè)站臺(tái)或區(qū)域 桷蘸請謎。p 產(chǎn)岱e q h e n c e ，t 融r r “口l n m e j ，p l n n 翼掣豇m e j s s t j 妞t i o t 、，為 列車在站臺(tái)或區(qū)域的點(diǎn)計(jì)劃。其中： & ?！俺阠 g 為該點(diǎn)在列車運(yùn)行中的次序，用自然數(shù)表示。列車從& g “口n c 8 為1 的車站或區(qū)域出發(fā)，依次通過口“g n 飽為2 、3 的車站或區(qū)域直到 終點(diǎn)； 對站臺(tái)計(jì)劃而言，尸腸n 彳州陽，刀m e 為列車的計(jì)劃到站時(shí)間；對區(qū)域計(jì) 劃而言，砌n 彳r 一似，肋船為列車的計(jì)劃發(fā)車時(shí)間。因?yàn)闀r(shí)間的不確定 性，用時(shí)間區(qū)間( 如【1 ，2 】) 表示p f d n f v n l 硒竹8 ； p 腸n j 啦l 砌卯為列車的計(jì)劃停留時(shí)間( 對車站而言) 或計(jì)劃運(yùn)行時(shí)間( 對 區(qū)域而言) ，用自然數(shù)表示。 腰三f 口踟w 為列車在該點(diǎn)的作業(yè)類型，o 表示非終點(diǎn)，1 表示終點(diǎn)。 算法4 1 計(jì)算列車的下一?？空九_(tái)，對每一列車執(zhí)行以下運(yùn)算：如果列車的 c “，m ” 妣i 砌h 屬性為空( 列車不在某一站臺(tái)停靠) 或當(dāng)前時(shí)刻小于列車的發(fā)車時(shí) 間與列車計(jì)劃運(yùn)行時(shí)間之和( 列車還沒有運(yùn)行到車站) ，則置列車的下一?？空九_(tái) ，i 舞戮孵一筵i 蓊囂囂意瀚& 。 ，。1。l 第四章t o p n 0 的建模與驗(yàn)證 一類對象p c 岍網(wǎng)建模與驗(yàn)證方法研究 為空( s t e p1 3 ) ；否則根據(jù)列車運(yùn)行計(jì)劃確定列車的下一車站：如果當(dāng)前時(shí)刻大于 列車在該車站的砌n4 州f 矗m p 值( 已到計(jì)劃到站時(shí)間) 且站臺(tái)的f r a 抽屬性為 空( 站臺(tái)上沒有停放列車) ，則置列車的下一?？空九_(tái)為該站臺(tái)( s t e p1 4 1 - s t 印 1 4 ，2 、。 算法4 1 ：計(jì)算列車的下一?？空九_(tái) 輸入：列車對象實(shí)例集合m 跏、站臺(tái)對象實(shí)例集合鼬口砌一、列車運(yùn)行圖 p l 口n 輸出：列車對象實(shí)例集合m 脅 s t 印1 ) 對砌脅的每一列車對象丹，執(zhí)行步驟1 1 一1 4 s t e p1 1 ) l n 在j 彈的行標(biāo) s t 印1 2 ) ，一乃c “，陀n f - 8 c 如n 在j 打的列標(biāo) s t 印1 3 ) 如果( n c “w n t 缸砌n ! = 廬或f 砌f ；p k 月 訂 同p 腸叫州，哪l 刀m 0 ，則 腳h “t m n o n + s t ； s t e p2 ) 返回( z h 婦) 算法4 2 計(jì)算列車的下一運(yùn)行區(qū)域，其運(yùn)算步驟為：如果列車的 洲e n t 缸f f d n 屬性非空( 列車在某站臺(tái)?？? 且列車在該站臺(tái)的趣邪o 舭m 值 為1 ( 當(dāng)前站臺(tái)是終點(diǎn)站) ，則下一運(yùn)行區(qū)域?yàn)轲?，代表到達(dá)終點(diǎn)( s f 印1 3 ) ；否則， 如果列車的“n fs m 如n 屬性非空( 列車在某站臺(tái)?？? 且當(dāng)前時(shí)刻還沒到列車 的到站時(shí)間與列車計(jì)劃停靠時(shí)間之和( 還沒到發(fā)車時(shí)間) ，則列車的下一運(yùn)行區(qū)域 置為一1 ( s t 印1 4 ) ；否則，根據(jù)列車計(jì)劃確定列車的下一運(yùn)行區(qū)域：如果當(dāng)前時(shí)刻 大于列車在該區(qū)域的肋h(yuǎn) j 州m l z 砌e 值( 已到計(jì)劃到沾時(shí)間) ，將列車下一運(yùn)行 區(qū)域設(shè)置為該區(qū)域( s t 印1 5 1 一s t 印1 5 2 ) 。 算法4 2 ：計(jì)算列車的下一運(yùn)行區(qū)域 輸入：列車對象實(shí)例集合丁h 跏、區(qū)域?qū)ο髮?shí)例集合鼬c 砌雎、列車運(yùn)行圖 第四章t 。p n o 的建模與驗(yàn)證 類對象p 謝i 網(wǎng)建模與驗(yàn)證方法研究 p l n n 輸出：列車對象實(shí)例集合打衲l s t c p1 ) 對打砌l 的每一列車對象打，執(zhí)行步驟1 1 - 1 4 s t e p1 1 ) f 一乃在p 缸雄的行標(biāo) s 卸1 2 ) - ，一乃c 刪t 缸f 泐l 在脅一的列標(biāo) s t 印1 3 ) 如果( n c “r 陀h t 招勘n ! = 妒且j 一【f d 1 西一l 蚍如，z = 1 ) t r n e x j e c t i o n 一咖 s t 印1 4 ) 如果( 行刪r m h t 凹踟n ! = 且 f 折l p = 行j 脅蔬晰p + j 肼【f 】們p ? 口以j 啞五m 0 乃n 哦，p 咖n 一- 1 s t 印1 5 ) 否則，對& 蹦鯽的每一站臺(tái)對象& ，執(zhí)行步驟1 5 1 1 5 - 2 s t c p1 5 1 ) 七一& 在川鯽的列標(biāo) s t e p1 5 2 ) 如果( p f 口一嘲嘲j 叼 鋤c 薩脅斗【f 陰3 叼”柳c 時(shí)1 且 砌l 驢= p 腸櫛 司嗣訛叫刪m l 砌”力 砰h “i e c 如，i 一& ； s t 印2 ) 返回( 砌抽) 3 擴(kuò)展t o p n o 模型的屬性 在對t o p n o 模型進(jìn)行驗(yàn)證時(shí)，需要驗(yàn)證與列車對象相關(guān)的屬性，如列車的 可達(dá)性、列車到站時(shí)間、列車在站時(shí)間等屬性。就列車運(yùn)行而言，只有在所有列 車都能到達(dá)終點(diǎn)的情況下對系統(tǒng)屬性的驗(yàn)證刁+ 有意義。本文定義了如下t o p n o 模型的屬性： 定義4 3 列車的弱可達(dá)性 指存在一個(gè)列車運(yùn)行序列，使得列車對象辦能到達(dá)終點(diǎn)?？捎萌缦聲r(shí)態(tài)邏 輯公式表示： 了o ( 掙s 啦p ( p 0 ) 定義4 4 列車的強(qiáng)可達(dá)性 指對于任何列車運(yùn)行序列，列車對象都能到達(dá)終點(diǎn)。可用如下時(shí)態(tài)邏輯表示： v o ( 丹s 雌烈m ) 定義4 5 列車到站時(shí)間 指在所有列車都能到達(dá)終點(diǎn)的前提下，列車在某一時(shí)刻到達(dá)車站。例如列車 第刪章t d p n o 的建模與驗(yàn)證 一類對象p e 晡網(wǎng)建模與驗(yàn)證方法研究 打到達(dá)站的時(shí)間是l 那么對于任何列車運(yùn)行順序，所有列車必定能到達(dá)終 點(diǎn)站( 強(qiáng)可達(dá)) ，這一屬性可用如下時(shí)態(tài)邏輯表示： ( 韻( 丹硎腳n o 細(xì)加以 弘s 缸疋砌f d ) ( v 口( ( 乃刪腳以。脅砌2 弘砌r o 擁f 力寸v o ( 對所有辦d ( 7 h 加) ，有乃j 卿( | p 功) ) ) 同樣，如果開到達(dá)站的時(shí)間是l 那么存在一個(gè)列車運(yùn)行順序，使得所 有列車能到達(dá)終點(diǎn)站( 弱可達(dá)) ，這一屬性可用如下時(shí)態(tài)邏輯表示： ( j o ( n c 聊硎t m 如h 乃礎(chǔ)z r o 咖f 即) ( v o ( ( n c “，地n t 脅“d 開 丹礎(chǔ)i t 砌4 f 乃斗j o ( 對所有n d ( m 加) ，有紛s 唧( p 們) ) ) 定義4 6 列車在站時(shí)間 指在所有列車都能到達(dá)終點(diǎn)的前提下，列車在某一時(shí)刻?？吭谲囌尽＠缌?車丹在n 亞之間的任一時(shí)刻?？吭谡荆敲创嬖谝粋€(gè)列車運(yùn)行順序，使得 所有列車能到達(dá)終點(diǎn)站，這一系統(tǒng)屬性可用如下時(shí)態(tài)邏輯表示： 對于所有的t 【n ，死 ( j o ( 時(shí)鐘= r 丹翻刪刀。加f f d 胛跚) ( v o ( ( 時(shí)鐘= r 乃c “胱以。塒砌竹e 踟寸j o ( 對所有抒d ( m f n ) ，有乃j 卿( p f 一) ) ) 定義4 7 列車交會(huì) 指兩列或多列列車同時(shí)?？吭谀骋卉囌?。例如驗(yàn)證列車丹1 和打2 能否在車 站& 交會(huì)，可用如下邏輯公式表示： j ot n l 甜r r e m j t a n o n s t t ，2 c h r r e n t j t n n o n s 如 定義4 8 列車運(yùn)行的安全性 列車運(yùn)行的安全性指列車運(yùn)行過程中要保證任何兩列列車不能同時(shí)在同一 站臺(tái)?？炕蛲瑫r(shí)在同一區(qū)域中運(yùn)行?？捎萌缦逻壿嫻奖硎救魏蝺闪辛熊嚥荒芡?時(shí)在同一站臺(tái)停靠： 對于所有的n 1 d ( m 加) ，z 挖d ( m m ) ，乃1 z 挖，有 v 口_ 1 ( 護(hù)1 c “，陽n t 脅加以= 眈c z 胛伽t 脅咖玎 護(hù)1 c “，r 陰f 塒矗d n 彩； 可用如下邏輯公式表示任何兩列列車不能同時(shí)在同一站臺(tái)?？浚?對于所有的n 1 d ( z 婦f ) ，m d ( m 加) ，乃1 z 挖，有 d q n c u r r e n t j e c t i o h = t r 2 c h r r e m j e c t i o n 亡r 1 c t t r r e n t j e c t t o n 鈉| 第四章m p n o 的建模與驗(yàn)證 一類對象p e 岍網(wǎng)建模與驗(yàn)證方法研究 4 2 2t o p n o 到s m v 程序的轉(zhuǎn)換說明 t o p n o 作為精確標(biāo)識(shí)p n o 的一個(gè)特例，可根據(jù)算法3 1 從t o p n 0 模型的 定義出發(fā)得到相應(yīng)的s m v 程序。下面重點(diǎn)說明程序中時(shí)間的表示及處理，對象 實(shí)例d 、庫所p 、變遷a 變量礦在s m v 中的表示方法，以及變遷o l 、f 2 、如的 實(shí)施過程。 1 轉(zhuǎn)換程序的時(shí)間表示及處理 鐵路智能運(yùn)輸系統(tǒng)中構(gòu)成系統(tǒng)主體的列車群并發(fā)性的表述、面向不同分析問 題的系統(tǒng)混合屬性的處理、影響列車群運(yùn)行的各種不確定性因素的處理均涉及到 對時(shí)間參數(shù)的分析，因此在模型驗(yàn)證時(shí)要能表示并處理與時(shí)間有關(guān)的屬性。由于 存在影響列車運(yùn)行的多種不確定因素，列車并不能完全按運(yùn)行圖確定的時(shí)問運(yùn) 行，因此如何有效表示時(shí)間就成為驗(yàn)證的關(guān)鍵問題，也是難點(diǎn)問題。為此，在驗(yàn) 證程序中定義了一個(gè)時(shí)鐘變量，并采用時(shí)聞區(qū)間來控制列車運(yùn)行。在模擬模型的 狀態(tài)變遷過程中，如果在某一時(shí)刻存在多個(gè)使能變遷，則隨機(jī)觸發(fā)一個(gè)使能變遷； 如果不存在使能變遷，則在下一狀態(tài)將時(shí)鐘變量的值增加l 。 2 t o p n 0 的對象實(shí)例o 、庫所p 、變遷扎變量y 在轉(zhuǎn)換程序中的表示 根據(jù)算法3 1 的s t 印1 1 s t e p1 4 ，需要分別在s m v 程序中定義與t o p n o 模型中類m m 、s 缸f f o 璣覷砌”對應(yīng)的結(jié)構(gòu)體鉚旭一z 勉加、0 p g j 鈀肋n ， 卯口，跆甜d n 及對應(yīng)的對象實(shí)例數(shù)組跏匕了h 跏、s m 匕跏砌n 、跏匕& 砸肼；定 義與庫所p ，凇、m 、a p 、r ，、n f 對應(yīng)的一維布爾數(shù)組肋i v 砌s 、5 鋤vn 口、 s 鋤v 脅、跏va r 、m v 腳。并根據(jù)對象的初始值和初始狀念下庫所的托肯值 設(shè)置上述數(shù)組的初始值。 此外，還要在s m v 程序中定義與模型變量辦、& 、對應(yīng)的變量5 如v 打、 s 鋤y j 趴脅- 野，這些變量的取值范圍分別在0 到i d ( 加抽) l 、o 到i d 0 口c 打m ) l 、o 到1 d ( s 加幻n ) 窿間。 3 轉(zhuǎn)換程序中狀態(tài)變遷的實(shí)旅 在t o p n o 中，變遷的實(shí)旌將實(shí)例化該變遷的前相關(guān)函數(shù)和后相關(guān)函數(shù)；設(shè) 置變遷的前置庫所和后置庫所下一狀態(tài)的值；執(zhí)行變遷的4 甜o n 函數(shù)，并修改所 涉及對象的屬性。下面說明t o p n 0 中列車進(jìn)站、出站和到達(dá)終點(diǎn)的處理。 ( 1 1 列車進(jìn)站處理 第四章t o p n o 的建模與驗(yàn)證一類對象p e 砸網(wǎng)建模與驗(yàn)證方法研究 列車迸站對應(yīng)變遷f 1 ，根據(jù)t o p