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

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

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

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