MSVL中異步通信方法的研究與實(shí)現(xiàn).pdf

1、隨著計(jì)算機(jī)和互聯(lián)網(wǎng)技術(shù)的快速發(fā)展，各種計(jì)算機(jī)軟、硬件系統(tǒng)已廣泛滲透到人類生產(chǎn)和生活中，然而如何保證計(jì)算機(jī)系統(tǒng)嚴(yán)格按照人類設(shè)計(jì)的方式工作已成為當(dāng)前計(jì)算機(jī)相關(guān)研究課題之一。時(shí)序邏輯作為一種形式化方法已廣泛應(yīng)用于系統(tǒng)的建模與驗(yàn)證中。
　　MSVL(Modeling,Simulationand Verification Language)是一種基于投影時(shí)序邏輯PTL(Projection Temporal Logic)的時(shí)序邏輯語言，它可

2、用于對(duì)計(jì)算機(jī)軟、硬件系統(tǒng)進(jìn)行建模、仿真和驗(yàn)證。本文實(shí)現(xiàn)了MSVL的異步通信方法，以實(shí)現(xiàn)MSVL對(duì)異步并發(fā)系統(tǒng)的建模與驗(yàn)證。文中首先介紹了PTL和MSVL的語法和語義，并討論了MSVL解釋器的實(shí)現(xiàn)原理及功能，接著形式化定義了進(jìn)程，通道以及通信命令的語法和語義，進(jìn)程用于對(duì)并發(fā)系統(tǒng)中的組件進(jìn)行建模，通道作為不同組件之間通信的消息緩沖，進(jìn)程執(zhí)行通信命令實(shí)現(xiàn)不同組件之間的消息傳遞，此外文中還給出了MSVL解釋器中異步通信的實(shí)現(xiàn)過程，最后通過三個(gè)具