基于ε-互模擬的軟件近似正確性模型

1.淮北師范大學 計算機科學與技術學院，安徽 淮北 235000

2.上海市高可信計算重點實驗室，上海 200062

3.淮北師范大學 數學科學學院，安徽 淮北 235000

1.淮北師范大學 計算機科學與技術學院，安徽 淮北 235000

2.上海市高可信計算重點實驗室，上海 200062

3.淮北師范大學 數學科學學院，安徽 淮北 235000

1 引言

軟件正確性是軟件工程的重要內容，是軟件可信性的重要屬性。對軟件正確性進行研究可以為提高軟件質量提供保證。軟件正確性主要表現為軟件的執行能否符合人們的預期。一般地，軟件的執行抽象為軟件的實現，人們的預期抽象為軟件的規范。進而軟件正確性表示為軟件的實現與規范之間的關系。這種關系借助于進程代數中的各種理論來描述：如ACP[1]，Communicating Sequential Process（CSP）[2]，Calculus of Communicating Systems（CCS）[3]等。在R.Milner提出的CCS語言（也稱為通信系統演算）中，各種進程之間的等價關系是其主要內容，如強互模擬和弱互模擬、跡等價及觀測等價等。把規范（specification）和實現（implementation）抽象為兩個進程，如果軟件規范和實現之間存在某種等價關系，則軟件是正確的。在文獻[4]中，應明生給出了這些等價關系的無限演化過程，定義了強互模擬極限、弱互模擬極限和跡極限等，從而建立了CCS語言的極限理論。為了描述在一定環境下軟件實現的無限演化，在文獻[5-6]中，作者基于ε-參數化互模擬，提出了ε-參數化極限互模擬和參數化互模擬極限，建立了ε-參數化互模擬的極限理論和拓撲理論。為了度量在拒絕環境下軟件實現與規范之間的近似程度，在文獻[7]中作者建立了三分之二互模擬的度量理論。……