基于場景的SOFL規(guī)約示范系統(tǒng)的設(shè)計與實現(xiàn).pdf

1、多年以來，形式化規(guī)約(formal specification)一直是軟件工程領(lǐng)域中的一個研究熱點，它的應(yīng)用范圍也正在逐步增長。一般來說，形式化規(guī)約是用形式化語言編寫的系統(tǒng)規(guī)格說明，是系統(tǒng)的屬性在某種級別上的抽象表示，能夠提供系統(tǒng)行為的精確描述。不過，大型復(fù)雜系統(tǒng)的形式化規(guī)約在可讀性上總是不能令人滿意，有時候甚至是規(guī)約的編寫人員自己都無法知道規(guī)約是否定義了“應(yīng)有的行為”。為解決這個問題，人們提出了規(guī)約示范（Specification a

2、nimation）技術(shù)。它通過直接或間接地對規(guī)約進行解釋和執(zhí)行來提供一種模擬機制，將規(guī)約的行為展示給用戶或規(guī)約開發(fā)人員，幫助他們理解規(guī)約。此外，規(guī)約示范技術(shù)可以和規(guī)約驗證和校驗（specification verification and validation）方法結(jié)合起來使用，以達(dá)到更好的規(guī)約驗證效果。 本文提出了一種針對SOFL (Structured Object-oriented Formal Language)規(guī)約的規(guī)

3、約示范方法并討論了支持這一方法的工具——SOFL-Animator的設(shè)計和開發(fā)。SOFL-Animator在規(guī)約示范的過程中使用消息序列圖（MSC）來顯示每條序列的執(zhí)行過程，從而更好地表現(xiàn)規(guī)約中各個部分之間的交互。同時，它還提供對規(guī)約示范的過程支持，按照特定的覆蓋策略抽取出規(guī)約的典型執(zhí)行序列，然后依次對每一條序列進行示范。用戶可以在工具的引導(dǎo)下系統(tǒng)地對規(guī)約行為進行示范。 本文的工作在一定程度上克服了SOFL規(guī)約在可讀性上的缺陷，