本文關(guān)鍵詞：Linux環(huán)境下基于MSVL的仿真與驗(yàn)證　出處：《西安電子科技大學(xué)》2013年碩士論文　論文類型：學(xué)位論文

  更多相關(guān)文章： 時(shí)序邏輯 MSVL 形式化方法 仿真驗(yàn)證 CTCS-3系統(tǒng)

【摘要】：隨著計(jì)算機(jī)和互聯(lián)網(wǎng)技術(shù)的快速發(fā)展，各種軟、硬件系統(tǒng)已經(jīng)廣泛滲透到人類生產(chǎn)和生活中，如何保證計(jì)算機(jī)系統(tǒng)嚴(yán)格按照人類設(shè)計(jì)的方式進(jìn)行工作已經(jīng)成為當(dāng)前計(jì)算機(jī)相關(guān)研究課題之一。采用形式化方法來(lái)描述軟硬件系統(tǒng)，能夠有效地減少系統(tǒng)設(shè)計(jì)中的錯(cuò)誤，提高設(shè)計(jì)的可靠性。時(shí)序邏輯作為一種形式化方法已被廣泛的應(yīng)用于系統(tǒng)的仿真和驗(yàn)證中。 建模仿真和驗(yàn)證語(yǔ)言(Modeling, Simulation and Verification Language，MSVL)是一種基于投影時(shí)序邏輯(Projection Temporal Logic，PTL)的時(shí)序邏輯程序設(shè)計(jì)語(yǔ)言，它可以用于對(duì)計(jì)算機(jī)軟硬件系統(tǒng)進(jìn)行建模、仿真和驗(yàn)證。本文主要討論Linux環(huán)境下基于MSVL的仿真和驗(yàn)證。文中首先介紹了PTL和MSVL的語(yǔ)法和語(yǔ)義，，并討論了MSVL解釋器的實(shí)現(xiàn)原理和功能，接著介紹了MSVL對(duì)系統(tǒng)進(jìn)行仿真和驗(yàn)證的原理，然后基于系統(tǒng)層次化設(shè)計(jì)理論詳細(xì)介紹了MSVL對(duì)系統(tǒng)的形式化描述方法，最后給出了一個(gè)用MSVL對(duì)CTCS-3列控系統(tǒng)進(jìn)行形式化描述的實(shí)例，借助解釋器MSV實(shí)現(xiàn)了對(duì)CTCS-3系統(tǒng)的仿真和驗(yàn)證，并給出了仿真和驗(yàn)證的結(jié)果。實(shí)例結(jié)果表明，此方法可以有效地檢測(cè)系統(tǒng)設(shè)計(jì)上的缺陷。
[Abstract]:With the rapid development of computer and Internet technology , various software and hardware systems have been widely used in human production and life . How to ensure the computer system to work in strict accordance with human design has become one of the current computer - related research topics . The formal method is used to describe the software and hardware system , which can effectively reduce the errors in the system design and improve the reliability of the design . The time sequence logic has been widely used in the simulation and verification of the system as a formal method . Modeling , Simulation and Verification Language ( MSVL ) is a kind of sequential logic programming language based on Projection Logic Logic , which can be used to model , simulate and validate the hardware and software system of computer .

【學(xué)位授予單位】：西安電子科技大學(xué)
【學(xué)位級(jí)別】：碩士
【學(xué)位授予年份】：2013
【分類號(hào)】：TP302

【參考文獻(xiàn)】

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

1 林惠民,張文輝;模型檢測(cè):理論、方法與應(yīng)用[J];電子學(xué)報(bào);2002年S1期

2 王淑禮,袁俊紅,江祥奎;描述與求解哲學(xué)家就餐問(wèn)題的Petri網(wǎng)模型研究[J];信陽(yáng)師范學(xué)院學(xué)報(bào)(自然科學(xué)版);2004年04期

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

1 王小兵;面向?qū)ο驧SVL語(yǔ)言及其在組合Web服務(wù)驗(yàn)證中的應(yīng)用[D];西安電子科技大學(xué);2009年

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

1 馬永濤;框架時(shí)序邏輯程序設(shè)計(jì)解釋器及模型檢測(cè)工具[D];西安電子科技大學(xué);2008年

本文編號(hào)：1392826