本文選題：形式化方法 + 概率模型驗(yàn)證��； 參考：《山東大學(xué)》2012年碩士論文

【摘要】：近年來,越來越多的計(jì)算機(jī)科學(xué)方法被廣泛應(yīng)用到諸如生物學(xué)等領(lǐng)域。一方面,計(jì)算機(jī)科學(xué)的方法可以通過在計(jì)算機(jī)上進(jìn)行模擬等方式使得對(duì)問題的研究可以擺脫原本復(fù)雜的實(shí)驗(yàn)環(huán)境和條件,大大節(jié)約了研究成本和研究時(shí)間,降低了研究難度;另一方面,計(jì)算機(jī)領(lǐng)域方法的多樣性和計(jì)算機(jī)的強(qiáng)大計(jì)算能力,為復(fù)雜問題的解決提供了可能性。由于系統(tǒng)生物學(xué)和計(jì)算機(jī)科學(xué)研究中的復(fù)雜分布式系統(tǒng)有著類似的地方,形式化方法領(lǐng)域中的模型和驗(yàn)證技術(shù)可以被應(yīng)用到系統(tǒng)生物學(xué)領(lǐng)域。形式化方法在分析大型系統(tǒng)方面優(yōu)勢(shì)明顯,它有著高效的驗(yàn)證技術(shù),可以利用自動(dòng)化的計(jì)算機(jī)工具分析具有復(fù)雜行為的大型系統(tǒng)。 作為一種表現(xiàn)良好的形式化方法,概率模型驗(yàn)證方法近年來廣受人們的關(guān)注與研究。概率模型驗(yàn)證是從定量方面去檢查一個(gè)具有隨機(jī)性行為的有限狀態(tài)系統(tǒng)的正確性。它與已有的基于仿真的方法有著一個(gè)明顯的區(qū)別是它能對(duì)所要驗(yàn)證的系統(tǒng)進(jìn)行徹底地挖掘,而不是僅僅挖掘系統(tǒng)的一個(gè)子集。 本文將概率模型驗(yàn)證的方法應(yīng)用到分析PDGF生物信號(hào)路徑系統(tǒng)中。 首先,作為本文的理論基礎(chǔ),本文詳細(xì)討論了概率模型驗(yàn)證的相關(guān)概念及理論推演。概率模型驗(yàn)證需要用到兩種輸入,即對(duì)系統(tǒng)的詳細(xì)描述以及對(duì)系統(tǒng)屬性的詳細(xì)描述。本文首先給出了概率模型驗(yàn)證的含義以及對(duì)系統(tǒng)詳細(xì)描述的方法,討論了所要驗(yàn)證系統(tǒng)的瞬時(shí)概率和穩(wěn)定概率的計(jì)算方法。接下來本文討論了系統(tǒng)屬性的描述方法,詳細(xì)給出了文中用到的語言——CSL(持續(xù)概率邏輯),并對(duì)其擴(kuò)展,即回報(bào)屬性進(jìn)行了討論。另外,本文給出了關(guān)于文中所用的概率模型驗(yàn)證工具PRISM的詳細(xì)介紹。 其次,本文所要分析的PDGF生物信號(hào)路徑系統(tǒng)對(duì)于細(xì)胞的繁殖和生長(zhǎng)具有重要意義,它直接調(diào)控細(xì)胞分裂和增殖,與癌癥的產(chǎn)生密切相關(guān)。本文詳細(xì)分析了其組成,并將對(duì)其的研究細(xì)化為三個(gè)具體的目標(biāo),從而實(shí)現(xiàn)對(duì)PDGF生物信號(hào)路徑的更好理解。 再次,本文通過三組實(shí)驗(yàn)來實(shí)現(xiàn)了對(duì)三個(gè)目標(biāo)的分析。實(shí)驗(yàn)中本文采用通過添加／移除單一反應(yīng)來進(jìn)行比較分析的方法,創(chuàng)建了多個(gè)模型的變種,以此來研究某一反應(yīng)對(duì)路徑信號(hào)的影響。這三組實(shí)驗(yàn)的結(jié)果顯示,定量驗(yàn)證的方法能夠幫助我們更加深刻的理解PDGF信號(hào)路徑,更進(jìn)一步地,能夠提供一個(gè)關(guān)于路徑行為的預(yù)測(cè)。 最后,由于除了概率模型驗(yàn)證方法,許多基于仿真的方法在研究生物系統(tǒng)時(shí)也非常流行,本文選擇了其中的常微分方程方法將其與概率模型驗(yàn)證方法進(jìn)行了比較研究。對(duì)常微分方法的研究分為理論與實(shí)踐兩部分。理論方面,本文首先給出了常微分方程在生物系統(tǒng)中的概念,然后為了更好地與概率模型驗(yàn)證方法進(jìn)行比較,本文詳細(xì)討論了常微分方法中瞬時(shí)狀態(tài)行為與穩(wěn)定狀態(tài)行為的計(jì)算。在實(shí)踐方面,本文給出了用常微分方法分析PDGF信號(hào)路徑的詳細(xì)實(shí)驗(yàn)過程,并將實(shí)驗(yàn)結(jié)果與概率模型驗(yàn)證方法的結(jié)果進(jìn)行了比較分析。兩種方法所的結(jié)果較為類似,本文進(jìn)一步分析了兩種方法類似與不同的原因。
[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.
【學(xué)位授予單位】：山東大學(xué)
【學(xué)位級(jí)別】：碩士
【學(xué)位授予年份】：2012
【分類號(hào)】：Q811

【共引文獻(xiàn)】

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

1 王晶;戎玫;張廣泉;祝義;;基于概率模型檢測(cè)的Web服務(wù)組合驗(yàn)證[J];計(jì)算機(jī)科學(xué);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 周從華;劉志鋒;王昌達(dá);;概率計(jì)算樹邏輯的限界模型檢測(cè)[J];軟件學(xué)報(bào);2012年07期

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

5 張君華;黃志球;曹子寧;仲晶;;代價(jià)和概率時(shí)間自動(dòng)機(jī)上概率有界的成本優(yōu)化可達(dá)性[J];應(yīng)用科學(xué)學(xué)報(bào);2009年01期

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

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

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

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

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

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

，

本文編號(hào)：1989704