結(jié)合程序切片技術(shù)的并行面向?qū)ο蟪绦蚰Ｐ蜋z查.pdf

1、隨著信息技術(shù)的發(fā)展，軟件在各個(gè)領(lǐng)域中的應(yīng)用越來(lái)越廣泛，軟件可靠性成為一個(gè)非常重要的問(wèn)題。面向軟件源程序的形式驗(yàn)證是保障軟件高可靠性的一種有效方法，已經(jīng)逐步由理論走向應(yīng)用。但是由于軟件日趨復(fù)雜、規(guī)模日漸龐大，如何提高軟件源程序驗(yàn)證的效率仍是當(dāng)前研究所面臨的主要問(wèn)題。 軟件模型檢查是對(duì)有窮狀態(tài)系統(tǒng)的一種形式化驗(yàn)證方法，它基于狀態(tài)搜索的基本思想。軟件通常是非常復(fù)雜的，在源代碼上直接進(jìn)行模型檢測(cè)是不實(shí)際的。因此必須從軟件程序或形式化軟件

2、規(guī)范中抽取驗(yàn)證模型。為減低面向?qū)ο蟛l(fā)程序驗(yàn)證模型的復(fù)雜性，本文提出一種面向?qū)ο蟛l(fā)程序的切片技術(shù)，并把該技術(shù)引入針對(duì)此種程序的模型檢查中。本文的主要工作有： 1．研究了面向?qū)ο蟛l(fā)程序設(shè)計(jì)語(yǔ)言Compositional C++，考察了該語(yǔ)言具有的非確定性、同步、通信等性質(zhì)，結(jié)合時(shí)態(tài)邏輯有關(guān)理論，提出基于LTL的并發(fā)程序形式描述。 2．研究了Compositional C++和Promela的語(yǔ)法和語(yǔ)義，在兩種語(yǔ)言的子集