結合程序切片技術的并行面向對象程序模型檢查.pdf

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

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