本文選題：形式化方法 + 概率模型驗證　； 參考：《山東大學》2012年碩士論文

【摘要】：近年來,越來越多的計算機科學方法被廣泛應用到諸如生物學等領(lǐng)域。一方面,計算機科學的方法可以通過在計算機上進行模擬等方式使得對問題的研究可以擺脫原本復雜的實驗環(huán)境和條件,大大節(jié)約了研究成本和研究時間,降低了研究難度;另一方面,計算機領(lǐng)域方法的多樣性和計算機的強大計算能力,為復雜問題的解決提供了可能性。由于系統(tǒng)生物學和計算機科學研究中的復雜分布式系統(tǒng)有著類似的地方,形式化方法領(lǐng)域中的模型和驗證技術(shù)可以被應用到系統(tǒng)生物學領(lǐng)域。形式化方法在分析大型系統(tǒng)方面優(yōu)勢明顯,它有著高效的驗證技術(shù),可以利用自動化的計算機工具分析具有復雜行為的大型系統(tǒng)。 作為一種表現(xiàn)良好的形式化方法,概率模型驗證方法近年來廣受人們的關(guān)注與研究。概率模型驗證是從定量方面去檢查一個具有隨機性行為的有限狀態(tài)系統(tǒng)的正確性。它與已有的基于仿真的方法有著一個明顯的區(qū)別是它能對所要驗證的系統(tǒng)進行徹底地挖掘,而不是僅僅挖掘系統(tǒng)的一個子集。 本文將概率模型驗證的方法應用到分析PDGF生物信號路徑系統(tǒng)中。 首先,作為本文的理論基礎(chǔ),本文詳細討論了概率模型驗證的相關(guān)概念及理論推演。概率模型驗證需要用到兩種輸入,即對系統(tǒng)的詳細描述以及對系統(tǒng)屬性的詳細描述。本文首先給出了概率模型驗證的含義以及對系統(tǒng)詳細描述的方法,討論了所要驗證系統(tǒng)的瞬時概率和穩(wěn)定概率的計算方法。接下來本文討論了系統(tǒng)屬性的描述方法,詳細給出了文中用到的語言——CSL(持續(xù)概率邏輯),并對其擴展,即回報屬性進行了討論。另外,本文給出了關(guān)于文中所用的概率模型驗證工具PRISM的詳細介紹。 其次,本文所要分析的PDGF生物信號路徑系統(tǒng)對于細胞的繁殖和生長具有重要意義,它直接調(diào)控細胞分裂和增殖,與癌癥的產(chǎn)生密切相關(guān)。本文詳細分析了其組成,并將對其的研究細化為三個具體的目標,從而實現(xiàn)對PDGF生物信號路徑的更好理解。 再次,本文通過三組實驗來實現(xiàn)了對三個目標的分析。實驗中本文采用通過添加／移除單一反應來進行比較分析的方法,創(chuàng)建了多個模型的變種,以此來研究某一反應對路徑信號的影響。這三組實驗的結(jié)果顯示,定量驗證的方法能夠幫助我們更加深刻的理解PDGF信號路徑,更進一步地,能夠提供一個關(guān)于路徑行為的預測。 最后,由于除了概率模型驗證方法,許多基于仿真的方法在研究生物系統(tǒng)時也非常流行,本文選擇了其中的常微分方程方法將其與概率模型驗證方法進行了比較研究。對常微分方法的研究分為理論與實踐兩部分。理論方面,本文首先給出了常微分方程在生物系統(tǒng)中的概念,然后為了更好地與概率模型驗證方法進行比較,本文詳細討論了常微分方法中瞬時狀態(tài)行為與穩(wěn)定狀態(tài)行為的計算。在實踐方面,本文給出了用常微分方法分析PDGF信號路徑的詳細實驗過程,并將實驗結(jié)果與概率模型驗證方法的結(jié)果進行了比較分析。兩種方法所的結(jié)果較為類似,本文進一步分析了兩種方法類似與不同的原因。
[Abstract]:In recent years, more and more computer science methods have been widely used in such fields as biology. On the one hand, the method of computer science can make the research of the problem free from the original complex experimental environment and conditions, and greatly save the research cost and the research time and reduce the research. On the other hand, the diversity of the computer domain method and the powerful computing power of the computer provide the possibility for the solution of complex problems. Because the complex distributed system in the system biology and computer science research has the similar place, the model and verification technology in the formal method domain can be applied to the system. In the field of biology, the formalization method has an obvious advantage in the analysis of large systems. It has an efficient verification technique and can use automated computer tools to analyze large systems with complex behavior.
As a formalized method with good performance, probability model verification method has been widely concerned and studied in recent years. The probability model verification is the validity of checking a finite state system with random behavior from the quantitative aspect. It has a distinct difference from the existing simulation based method that it can be tested. The system of certificates is thoroughly excavated, rather than just mining a subset of the system.
In this paper, the method of probabilistic model validation is applied to the analysis of PDGF biological signal path system.
First, as the theoretical basis of this paper, this paper discusses the related concepts and theoretical deduction of probability model verification in detail. The probability model verification needs two kinds of input, that is, detailed description of the system and detailed description of the system properties. In this paper, the method of describing the instantaneous probability and the stability probability of the system is discussed. In this paper, the description method of the system property is discussed, and the language used in the paper is given in detail, CSL (continuous probability logic), and its extension, that is, the return attribute is discussed. In addition, this paper gives the verification of the probability model used in the paper. A detailed introduction to the tool PRISM.
Secondly, the PDGF biosignal pathway system in this paper is of great significance to cell reproduction and growth. It directly regulates cell division and proliferation and is closely related to the production of cancer. This paper analyzes its composition in detail, and will refine its research into three specific targets, thus realizing the PDGF biological signal path. Good understanding.
Thirdly, in this paper, the analysis of three targets is realized through three groups of experiments. In the experiment, we use the method of adding / removing the single reaction to make a comparison and analysis, and create a variety of models, in order to study the effect of a reaction on the path signal. The results of the three groups of tests show that the method of quantitative verification can help. To help us understand the PDGF signal path more deeply, we can further provide a prediction of path behavior.
Finally, in addition to the probability model verification method, many simulation based methods are also very popular in the study of biological systems. This paper chooses the ordinary differential equation method to compare it with the probability model verification method. The study of the ordinary differential method is divided into two parts: Theory and practice. The concept of the ordinary differential equation in the biological system is given, and in order to compare with the probability model verification method better, the calculation of the instantaneous state behavior and the stable state behavior in the ordinary differential method is discussed in detail. In practice, the detailed experimental process of the analysis of the PDGF signal path by the ordinary differential method is given in this paper. The experimental results are compared with the results of the probabilistic model verification method. The results of the two methods are similar. This paper further analyzes the reasons for the similarity and difference between the two methods.
【學位授予單位】：山東大學
【學位級別】：碩士
【學位授予年份】：2012
【分類號】：Q811

【共引文獻】

相關(guān)期刊論文 前5條

1 王晶;戎玫;張廣泉;祝義;;基于概率模型檢測的Web服務組合驗證[J];計算機科學;2012年01期

2 劉陽;繆淮扣;曾紅衛(wèi);馬艷;劉攀;;Nondeterministic Probabilistic Petri Net—A New Method to Study Qualitative and Quantitative Behaviors of System[J];Journal of Computer Science & Technology;2013年01期

3 周從華;劉志鋒;王昌達;;概率計算樹邏輯的限界模型檢測[J];軟件學報;2012年07期

4 陸天波;方濱興;孫毓忠;郭麗;;匿名協(xié)議WonGoo的概率模型驗證分析[J];小型微型計算機系統(tǒng);2006年04期

5 張君華;黃志球;曹子寧;仲晶;;代價和概率時間自動機上概率有界的成本優(yōu)化可達性[J];應用科學學報;2009年01期

相關(guān)博士學位論文 前3條

1 張君華;實時隨機系統(tǒng)的分析診斷與控制研究[D];南京航空航天大學;2011年

2 陸天波;P2P匿名通信協(xié)議WonGoo研究[D];中國科學院研究生院（計算技術(shù)研究所）;2006年

3 余長宏;基于統(tǒng)計學模型的納米級容錯電路關(guān)鍵技術(shù)研究[D];浙江大學;2007年

相關(guān)碩士學位論文 前1條

1 韓寶梅;基于動態(tài)QoS優(yōu)化的腦卒中預防與急救服務系統(tǒng)[D];哈爾濱工業(yè)大學;2011年

，

本文編號：1989704