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

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

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