翻譯以.原文和在同一文件中前

SOFL一種為工業(yè)應(yīng)用的形式化工程方形式化方法沒(méi)有取得廣泛的工業(yè)認(rèn)可的原因有多種。他們沒(méi)能很好的集成到已建立的工業(yè)軟件過(guò)程當(dāng)中，對(duì)他們的應(yīng)用需要有很強(qiáng)的抽象與數(shù)學(xué)技巧，還有現(xiàn)存的工具不能滿(mǎn)意的支持完整的形式化軟件開(kāi)發(fā)過(guò)程。我們提出了一種叫做SFL的語(yǔ)言以及對(duì)于系統(tǒng)開(kāi)發(fā)的SOF計(jì)階段用面向SOF了SLSOF如何使用。介的時(shí)候閱讀和理解形式化歸約更難了。一個(gè)軟件工程師必須花很多精力來(lái)學(xué)些必要的技負(fù)擔(dān)的起。雖然他們的系統(tǒng)質(zhì)量很重要，大部會(huì)優(yōu)先考慮先滿(mǎn)足市場(chǎng)的需求。這個(gè)觀改進(jìn)形式化方法來(lái)適應(yīng)工業(yè)應(yīng)用件過(guò)程中的改變。首先，形式化方法通常假定系統(tǒng)的形式化歸實(shí)現(xiàn)前要全部完成。這是不欠實(shí)際的。有些需求在設(shè)計(jì)之前必須獲得并記錄在歸約中，但是其他的卻可以再設(shè)計(jì)的時(shí)候獲取。因?yàn)檫@個(gè)原因，我們把用戶(hù)的需求分成兩部分，分別在不同的階段獲面的布局，可用性，有效性。次級(jí)需求可以再設(shè)計(jì)階段用原型技術(shù)來(lái)獲得。確認(rèn)對(duì)用戶(hù)需求的歸約，以及確認(rèn)設(shè)計(jì)和程序能夠滿(mǎn)足需求歸約或設(shè)計(jì)。嚴(yán)格基于形式化證明原則，但是更容易執(zhí)行。但是大部分現(xiàn)存的方法都是集中在設(shè)計(jì)和程序階段的錯(cuò)誤，比如Parnas和Weiss的活動(dòng)設(shè)計(jì)[7]，F(xiàn)agan的設(shè)計(jì)和代碼[8]，還有Knight，Meyers的階段傾向于檢測(cè)的產(chǎn)品能出來(lái)請(qǐng)求屬性。嚴(yán)格審在確認(rèn)正確性方面或許不如形式化證明那么令人信服，但是一個(gè)不錯(cuò)的且可行的技術(shù)或以自動(dòng)支持，因而可以減少時(shí)間和勞動(dòng)費(fèi)用。也應(yīng)該考慮到失敗的風(fēng)險(xiǎn)和費(fèi)用；兩者都缺乏完整的形式化證明；或者建議形式化證明應(yīng)該用于較次的關(guān)鍵歸約。無(wú)論何種情況，都應(yīng)該支持嚴(yán)格測(cè)考慮到記號(hào)，純數(shù)學(xué)記號(hào)不能很好的擴(kuò)充來(lái)支持大的復(fù)雜系統(tǒng)開(kāi)發(fā)，對(duì)工程師們來(lái)說(shuō)也因的（比如[16],VDM-S[17]）都使用數(shù)學(xué)符號(hào)這樣不能用標(biāo)準(zhǔn)鍵盤(pán)直接輸入記號(hào)。支持工具可以解決這個(gè)問(wèn)題，但是用戶(hù)會(huì)覺(jué)得有兩套記號(hào)很不方便；一個(gè)用于從標(biāo)準(zhǔn)鍵盤(pán)輸入記號(hào)，另一個(gè)則用于向顯示屏輸出。自然語(yǔ)言對(duì)于形式化歸約中的形式化記號(hào)是完整的以至可以利用他們的解釋。有效的形式化歸約需要有個(gè)在圖形記號(hào)，自然語(yǔ)言，數(shù)學(xué)記號(hào)的綜合平衡，如圖2所示。也是這篇討論的重點(diǎn)話(huà)題，這將在1.2部分進(jìn)行詳細(xì)討論。兩者方式可以采用來(lái)集成形式化方法和結(jié)構(gòu)化方法。一種是使用Yourdon或者DeMarco方需求歸約方法和結(jié)構(gòu)化形式化方法的工作，這個(gè)工作將MeMarco數(shù)據(jù)流圖和VDM組合起來(lái)程，記號(hào)和方法學(xué)中所改進(jìn)，同時(shí)現(xiàn)有的方法對(duì)于集成不同的方法不能給出一個(gè)一致這是不同于經(jīng)典的面向?qū)ο蠓椒?，?jīng)典面向?qū)ο笾袛?shù)據(jù)結(jié)構(gòu)是設(shè)計(jì)用料反映現(xiàn)實(shí)世界的對(duì)象。在使用面向?qū)ο蠓椒ň托行枨蠓治鲋灰腥齻€(gè)的。第一，當(dāng)開(kāi)發(fā)者不熟悉應(yīng)用領(lǐng)域時(shí)，定義有用的對(duì)象很。有些圖形記號(hào)工具可以使用[26]，但是這些只是幫助表定義他們并不能被確切說(shuō)明。結(jié)構(gòu)化方法通過(guò)分解和演化歸約到低層歸約可以給我們提供有用的對(duì)象和必須的方法。最后一個(gè)在于開(kāi)發(fā)者和用戶(hù)之間的溝通。用戶(hù)通常從任務(wù)SOF使用結(jié)化方來(lái)行求分和約用面對(duì)方法設(shè)。結(jié)化SOF通過(guò)描述SOFL的語(yǔ)法和非形式化語(yǔ)義從它初步描述中來(lái)定義和改進(jìn)SOFL語(yǔ)言。通過(guò)對(duì)一個(gè)居民公寓管理系統(tǒng)來(lái)證明SOFL語(yǔ)言的能力和可用性這邊的余下部分如下組織。第二部分闡述使用SOFL的軟件開(kāi)發(fā)過(guò)程。第三部分描述使用SOFL的軟件過(guò)程軟件過(guò)程是一個(gè)已經(jīng)取得很多研究者關(guān)注的領(lǐng)域[2]。倡導(dǎo)SOF的軟件過(guò)程是一個(gè)特殊化的瀑布開(kāi)發(fā)模型[29]3SOFL用嚴(yán)格來(lái)驗(yàn)證相對(duì)于需求歸約設(shè)計(jì)和相對(duì)于設(shè)計(jì)的程序是非常重要的。動(dòng)態(tài)開(kāi)發(fā)則是發(fā)現(xiàn)系統(tǒng)的動(dòng)態(tài)特征，通過(guò)用戶(hù)的需要來(lái)驗(yàn)證系統(tǒng)，以及通過(guò)原型和測(cè)試來(lái)獲取的需個(gè)層次，當(dāng)前歸約的某個(gè)部分就可以構(gòu)建原型并進(jìn)試，這可以與系統(tǒng)的剩余部分的靜態(tài)開(kāi)發(fā)同時(shí)進(jìn)行。同樣，在某些歸約構(gòu)造原型并測(cè)試后，它就能捕獲的需要和設(shè)計(jì)的構(gòu)造軟件系統(tǒng)的SOFL方法學(xué)圖4SOFL歸約的圖5SOFL實(shí)現(xiàn)的案例研究背景SF學(xué)。這個(gè)局部的住宅套房公司管理許多業(yè)務(wù)和資源。業(yè)務(wù)包括前臺(tái)桌面服務(wù)，房間服務(wù)，服務(wù)，報(bào)告服務(wù)，體育服務(wù)，金融和安全服務(wù)。資源包括50個(gè)套間（200單人間，100100305020個(gè)豪宅22個(gè)餐廳和一個(gè)游泳池。這個(gè)公司通過(guò)電腦來(lái)支持前臺(tái)活動(dòng)，但是沒(méi)有電腦系統(tǒng)來(lái)支持完整的管理。因此住宅套房公司的經(jīng)理和我們合作來(lái)開(kāi)發(fā)這個(gè)軟件系統(tǒng)的歸約。識(shí)，但是懂得管理系統(tǒng)。通過(guò)初試的需求分析，我們?cè)谝粋€(gè)次的抽象層面對(duì)這個(gè)管理系構(gòu)造條件數(shù)據(jù)流圖和歸約模條件數(shù)據(jù)流條件數(shù)據(jù)流圖是一個(gè)帶箭頭的圖，由數(shù)據(jù)流，數(shù)據(jù)和條件過(guò)程組成。數(shù)據(jù)流是標(biāo)有數(shù)據(jù)類(lèi)型的，代表在條件過(guò)程之間轉(zhuǎn)換的一包數(shù)據(jù)。數(shù)據(jù)則是某種類(lèi)型的變量來(lái)代在CDFDs和DeMarco和Yourdon數(shù)據(jù)流圖之間有四種重要的畫(huà)一個(gè)CDFD可以有助于描述一個(gè)系統(tǒng)結(jié)構(gòu)的整體樣供了定義與歸約模塊相CDFD圖6CDFDs圖8需求歸約的頂層歸約模一個(gè)重要的議題是如何定義與CDFD相關(guān)聯(lián)的歸約模塊。我們使用下面的四規(guī)則1：每個(gè)數(shù)據(jù)流，除了在靜態(tài)數(shù)據(jù)和條件過(guò)程之間的，每個(gè)在CDFD中的數(shù)據(jù)為外部變量獲得，不必要用多于的數(shù)據(jù)來(lái)轉(zhuǎn)化中的變量。然而在過(guò)程中間轉(zhuǎn)移的數(shù)據(jù)將量則指向數(shù)據(jù)，前置后置條件則定義了功能，一個(gè)分解和評(píng)論。參數(shù)列表的語(yǔ)法則是為2)不同的端口被符號(hào)|分割c-processManage-Information(res-req:Reservation|rep-req:ReportRequest|room-d-rep:DailyReport|check-out-bill:CheckOutBill|dummy:voidprePreManage-Iment...這里Reservation,ReportRequesnt,DailyReport,以及CheckOutBill圖8中條件流圖中對(duì)應(yīng)歸約模參數(shù)res-req,rep-req,room-no,d-rep,check-out-bill可以由數(shù)據(jù)流不同的名字因?yàn)榘闯霈F(xiàn)SOFL使用VDM格式的語(yǔ)義，這里變量將綁定他們類(lèi)型的一個(gè)值，或者是缺失，這表明還bound（res-req)或者bound(rep-req)或者bound(room-no),值表明或者res-req,rep- 或room-no有一個(gè)值。前置條件由操作語(yǔ)義來(lái)確保bound(res-req)或者P(rep-req,room-no),這里P（rep-req,room-no)是一個(gè)斷言依賴(lài)于或者rep-req,room-no,但是不依賴(lài)res-這個(gè)斷言需要通過(guò)rprq以及roomno來(lái)確保；條件過(guò)程僅僅定義了rprq或者roomnoifbound（rep-req)elseifroom-no>5elsebound(dummy)r-rep,rep-req和room-no綁定，這是一個(gè)明確的前置條件。這個(gè)不能直接表達(dá)，因?yàn)閂DM能斷言一個(gè)值沒(méi)有綁定。然而如果（rs-req,rep-req,room-no)是明確的前置條件，那么完整的前置條件是p(res-req,ni,nil)或者p(nl,repreq,ni),或者p(ni,ni,room-no)相似的規(guī)則可言應(yīng)用于后者條件。規(guī)則3：對(duì)一個(gè)條件過(guò)程如果有數(shù)據(jù)流從數(shù)據(jù)到條件過(guò)程但是沒(méi)有數(shù)據(jù)流從條件過(guò)程c-processA()extwrwrs:typeprePreA(s)extrds:TypeprePreB(S)這里~s和s代表?xiàng)l件過(guò)程A激活之前的值和之后的應(yīng)用上面的四個(gè)規(guī)則，我們可以為圖8中的CDFD構(gòu)造如下分CDFD.條件過(guò)程的分解定義了輸入時(shí)如何轉(zhuǎn)換到輸出的。分解必須滿(mǎn)足中給定的約束。這樣一種分解不僅是條件過(guò)程的定義，同時(shí)也可以擴(kuò)展其功能。因而這就允許SOFL支在SOFL分解和經(jīng)典的數(shù)據(jù)流圖之間有三個(gè)在低層外加的數(shù)據(jù)流被當(dāng)做是條件過(guò)程的內(nèi)部狀態(tài)變量。這些另外的數(shù)據(jù)流有一個(gè) e-rep,events-案例研究中的經(jīng)驗(yàn)表明在獲得數(shù)據(jù)和條件過(guò)程的抽象和封裝方面這個(gè)規(guī)則比起Yourdon區(qū)別2.一個(gè)條件過(guò)程可以分解成數(shù)個(gè)低層次的當(dāng)一個(gè)條件過(guò)程必須分解成幾個(gè)低層的彼此不連接的CFD把這些不互連的FD組織起來(lái)的可行方法是把每接的部分視為一個(gè)CFD,然后分別8ne-nformtion可以被分解成3個(gè)CFD.其中兩個(gè)在圖12和圖1312中的FD的歸約模塊在附錄中給出。句話(huà)說(shuō)，歸約模塊中的常量，類(lèi)型，類(lèi)和的變量的周期是這個(gè)歸約模塊本身和它的繼承如何使用分這可以由助于澄清在CDFD中國(guó)的數(shù)據(jù)流，數(shù)據(jù)，和條件過(guò)程的歧義SOFL提供下面的標(biāo)準(zhǔn)來(lái)選擇要分解的過(guò)域的時(shí)候或者有過(guò)相似應(yīng)用領(lǐng)域系統(tǒng)開(kāi)發(fā)經(jīng)驗(yàn)的時(shí)候，這個(gè)方很有效。演和結(jié)構(gòu)的改變。。條件過(guò)程可以通過(guò)構(gòu)造相應(yīng)低層的CDFD來(lái)分解從而重定義這個(gè)過(guò)程。而下面的方法在構(gòu)造歸約的時(shí)候使用演化和分解師有效的。分解和演，化史交錯(cuò)的，但是通常分解先開(kāi)始，然后如果必要可以相應(yīng)的進(jìn)行演化。當(dāng)在分解條件過(guò)程的時(shí)候如果發(fā)現(xiàn)條件過(guò)程本身的改變時(shí)必要的，則條件過(guò)程或者相應(yīng)的CDFD的演化就應(yīng)該實(shí)施。演化的結(jié)果是另一個(gè)層次結(jié)構(gòu)的CDFD，它正確的反映了在條件過(guò)程和它的分解CDFD的分解關(guān)系。通過(guò)實(shí)施分解和演化，我們可以把頂層的CDFD轉(zhuǎn)換成一個(gè)最終的歸約，它包括在圖結(jié)構(gòu)化的需求歸約轉(zhuǎn)換基于對(duì)象的設(shè)計(jì)得質(zhì)量屬性比如可靠性，可讀小學(xué)，可重用性，信息封裝，還有可性。指導(dǎo)原則1.遵循需求歸約中的CDFD的層次結(jié)構(gòu)圖把系統(tǒng)設(shè)計(jì)成CDFDs形式的層次結(jié)這不意味著是一個(gè)嚴(yán)格的一對(duì)一的關(guān)系?？梢圆扇∫恍└淖儊?lái)改進(jìn)設(shè)計(jì)的質(zhì)量。在需求歸約中的有些過(guò)程代表了現(xiàn)實(shí)世界的實(shí)體而不是軟件系統(tǒng)的一部分，比如圖8中的utom.在絕大部分案例中需求歸約中的CF圖16中的在居民套間管理系統(tǒng)中的需求歸約的CFD是源自圖8和圖12中的需求歸約。作為輸入，并產(chǎn)生相同類(lèi)的對(duì)象robjet.其他的條件過(guò)程像hknSrvie以及hk-Out-Srvie也處理其他類(lèi)的對(duì)象。呆箭頭的間斷線代表控制數(shù)據(jù)流，她們沒(méi)有攜帶實(shí)際的數(shù)據(jù)，但是卻可以激活一個(gè)條件過(guò)程。圖16設(shè)計(jì)的頂層以使用基于對(duì)象的設(shè)計(jì)技術(shù)，為每個(gè)數(shù)據(jù)創(chuàng)造類(lèi)的。在需求中的將變成在設(shè)計(jì)中的類(lèi)的。某些條件過(guò)程可以作為每個(gè)類(lèi)中的方法來(lái)實(shí)現(xiàn)。這個(gè)方法通常要改變條件過(guò)程歸約的結(jié)構(gòu)，把代表數(shù)據(jù)的外部變量放入過(guò)程的輸入和輸出參數(shù)中。選擇何種方S-moduleTop-Design:Figure16rlist:ReservationList;extwrrlist:ReservationListwrprePreReserve(res-extwrrlist:ReservationListwrprePreChange(change-req,rlist,rooms) customer-methodCheck-In( extrdrlist:ReservationList PreCheck- al-inf,rlist,customer-postPostCheck-In( prePreReserve- PostReserve- 把設(shè)計(jì)轉(zhuǎn)換成程序把頂層的歸約模塊轉(zhuǎn)換陳實(shí)現(xiàn)模塊Program同時(shí)每個(gè)其他的歸約模塊都對(duì)應(yīng)應(yīng)該實(shí)把頂層歸約模塊的頂層CDFD實(shí)現(xiàn)為開(kāi)始的實(shí)現(xiàn)模塊中的main方法模塊使用了這個(gè)條件過(guò)程，而所的過(guò)程其過(guò)程體則源自與它的所分解的CDFD。比如我們轉(zhuǎn)換圖16所示的頂層CDFD以及它的歸約模塊成實(shí)現(xiàn)模塊rlist:ReservatioList;rooms:Rooms;methodcreate();methodChange(change-methodCancel(cancel-methodmethodCheck- bill:CheckOutBill;methodmethodCheck-Out(room-Algorithm(Reserve-procedureReserve-procedureCheck-In-procedureCheck-Out-面向?qū)ο筠D(zhuǎn)是作為直接變換的對(duì)應(yīng)，但是又如下的區(qū)別：在設(shè)計(jì)中的每個(gè)CDFD，創(chuàng)造一個(gè)類(lèi)，這個(gè)類(lèi)方法；如果一個(gè)條件過(guò)程分解成了低層次的CDFD，則它的已轉(zhuǎn)換的方法的主體應(yīng)該是低層讓我們?cè)倌脠D16中的頂層CDFD和它的歸約作為這個(gè)方法的例子。它轉(zhuǎn)換成程序如下：methodcreate(...);methodCheck-In-methodReport-Service(...);substate:RS-class;proceduremainstate: 這個(gè)CDFD可以轉(zhuǎn)換成類(lèi)RS-class.RS-class變量substate以及它潛在的方法可以在Report-Service方法體中4SOFL演SOFCFDs的層次結(jié)構(gòu)圖可以幫助獲得系統(tǒng)的整體視圖，這就提供了一個(gè)決定哪些組件需要進(jìn)一步定義的基礎(chǔ)。寫(xiě)形式化的歸約可以），并提高CDFDsCFDs提供一個(gè)易于理解的結(jié)構(gòu)，它允許開(kāi)發(fā)者的分解，演變，修改和的階段中態(tài)的進(jìn)程或數(shù)據(jù)的規(guī)范（包括需求規(guī)格說(shuō)明和設(shè)計(jì)）。理系統(tǒng)。開(kāi)展了次的需求分析和繪圖高水平CDFDs（無(wú)定型還）之后，我們就能與經(jīng)理結(jié)構(gòu)來(lái)，盡管這被建議使用。開(kāi)發(fā)者可以通過(guò)分別畫(huà)和歸約CDFD來(lái)為現(xiàn)實(shí)世界的系統(tǒng)構(gòu)造第四，在歸約中的CDFDs和類(lèi)構(gòu)造使得SOFL語(yǔ)言能夠支持面向?qū)ο蟀阉\(yùn)用到大規(guī)模工程的一個(gè)。在歸約和設(shè)計(jì)階段，如果開(kāi)發(fā)者能夠有效的構(gòu)造建立結(jié)貢化方法可以有效的幫助構(gòu)造需求歸約而面向?qū)ο蠓椒▌t有助于系統(tǒng)設(shè)計(jì)。歸約方法同當(dāng)前正在活動(dòng)的研究和未來(lái)的研究主動(dòng)的在下面這些方面追求進(jìn)一步研究：1）將SOFL運(yùn)用到更復(fù)雜的工業(yè)系統(tǒng)中2）嚴(yán)格技術(shù)，3）基于形式化歸約的程序測(cè)試，4）CDFDs和條件過(guò)程到程序的自動(dòng)轉(zhuǎn)換5）基于現(xiàn)有的圖形原型工具對(duì)SOFL把SFL運(yùn)用到復(fù)雜系統(tǒng)可以為SOFL方法是有效性提供數(shù)據(jù)，還能傳達(dá)一下開(kāi)發(fā)問(wèn)題。SOFL如何被工業(yè)環(huán)境中的工程團(tuán)隊(duì)使用呢？OFL又如何影響工程管理和溝通？SOFL如何響件證確和本第作正與地電公合調(diào)SOFL如何運(yùn)用來(lái)開(kāi)發(fā)鐵路交叉控制系統(tǒng)。我們已經(jīng)開(kāi)始研究嚴(yán)格技術(shù)，并有兩個(gè)正在進(jìn)行的工程。第一個(gè)是為條件過(guò)程生成除了嚴(yán)格技術(shù)，我們?cè)陂_(kāi)展基于SOFL歸約的程序測(cè)試研究[13].通過(guò)已經(jīng)建立好的準(zhǔn)參考文S.Liu,V.Stavridou,andB.Dutertre,“ThePracticeofFormalMethodsinSafetyCriticalJ.SystemsandSoftware,vol.28,pp.77–87,D.Craigen,S.Gerhart,andT.Ralston,“FormalMethodsRealityCheck:IndustrialUsage,”P(pán)roc.FME’93:Industrial-StrengthFormalMethods,pp.250–267.Odense,Denmark:Springer-Verlag,D.JacksonandJ.Wing,“AnInvitationofFormalMethods,”Computer,pp.16–30,Apr. TheVDM-SLToolGroup,“UsersManualfortheIFADVDM-SLTools,”TechnicalReportIFAD-VDM-4,Inst.ofAppliedComputerScience,IFAD,Dec.19[5]A.Bloesch,E.Kazmierczak,M.Utting,“TheSuminErgo:ATutorial,”TechnicalReport96-22,SoftwareVerificationResearchCentre,TheUniv.ofQueensland,Sept.1996.J.Crow,S.Owre,J.Rushby,N.Shankar,andM.Srivas,“ATutorialIntroductiontoPVS,”P(pán)roc.WIFT‘95:WorkshopIndustrial-StrengthFormalSpecificationTechniques,Apr.1995.D.L.ParnasandD.M.Weiss,“ActiveDesignReviews:PrinciplesandPractices,”P(pán)roc.EighthConf.SoftwareEng.,pp.215–222,Aug.M.E.Fagan,“DesignandCodeInspectionstoReduceErrorsinProgramDevelopment,”IBMSystemsJ.,vol.15,no.3,pp.182–211,1976.J.C.KnightandE.A.Meyers,“AnImprovedInspectionTechnique,”Comm.ACM,vol.36,no.pp.50–61,Nov.S.Liu,“Evolution:AMorePracticalApproachthanRefinementforSoftwareDevelopment,”P(pán)roc.ThirdIEEEInt’lConf.Eng.OfComplexComputingSystems,Como,Italy,pp.142–151,IEEEPress,Sept.P.StocksandD.Carrington,“AFrameworkforSpecification-BasedTesting,”IEEESoftwareEng.,vol.22,no.11,pp.777–793,Nov.E.J.Weyuker,T.Goradia,andA.Singh,“AutomaticallyGeneratingTestDatafromaBooleanSpecification,”IEEETrans.SoftwareEng.,vol.20,no.5,pp.353–363,May1994.A.J.OffuttandS.Liu,“GeneratingTestDatafromSOFLSpecifications,”J.SystemsandSoftware,toappear.A.Bloesch,E.Kazmierczak,P.Kearney,andO.Traynor,“Cogito:MethodologyandSystemforFormalSoftwareDevelopment,”Int’lJ.SoftwareEng.andKnowledgeEng.,vol.5,no.4,pp.599–S.Liu,“FormalMethodsandInligentSoftwareEngineeringEnvironments,”TechnicalReportHCU-IS-95-006,HiroshimaCityUniv.,1995.A.Diller,“Z:AnIntroductiontoFormalMethods,”JohnWiley&Sons,J.Dawes,“TheVDM-SLReferenceGuide,”P(pán)itman,L.T.Semmens,R.B.France,andT.W.G.Docker,“IntegratedStructuredysisandFormalSpecificationTechniques,”TheComputerJ.,vol.35,no.6,1992.A.Bryant,“StructuredMethodologiesandFormalNotations:DeveloAFrameworkSynthesisandInvestigation,”P(pán)roc.ZUserWorkshop,Oxford1989.Springer-Verlag,M.D.Fraseretal.,“InformalandFormalRequirementsSpecificationLanguages:BridgingtheGap,”IEEETrans.SoftwareEng.,vol.17,no.5,pp.454–466,May1991.N.Plat,J.vanKatwijk,andK.Pronk,“ACaseforStructuredysis/FormalDesign,”P(pán)roc.VDM’91,LectureNotesinComputerScience551,pp.81–105.Berlin:Springer-Verlag,1991.S.Liu,“AFormalRequirementsSpecificationMethodBasedonDataFlowysis,”J.SystemsandSoftware,vol.21,pp.141–149,1993.S.Liu,“InternalConsistencyofFRSMSpecifications,”J.SystemsandSoftware,vol..2,pp.176,MayE.H.DürrandJ.vanKatwijk,“VDM++,AFormalSpecificationLanguageforObjectOrientedDesigns,”P(pán)roc.Conf.ToolsEuro’92inTechnologyofObject-OrientedLanguagesandSystems,Tools7.PrenticeHallInt’l,1992.S.R.L.MeiraandA.L.C.Cavalcanti,“ModularObject-OrientedZSpecifications,”C.J.vanRijsbergen,ed.,Proc.WorkshoponComputingSeries,LectureNotesinComputerScience,pp.173–192.Oxford,UK:Springer-Verlag,1990.P.CoadandE.Yourdon,Object-OrientedDesign.YourdonPressComputingSeries.EnglewoodCliffs,N.J.:PrenticeHall,1991.S.LiuandY.Sun,“StructuredMethodology+Object-OrientedMethodology+FormalMethods:MethodologyofSOFL,”P(pán)roc.FirstIEEEInt’lConf.Eng.ComplexComputerSystems,pp.137–144,Ft.Landerdale,Fla.,IEEECSPress,Nov.1995.K.E.Huff,“SoftwareProcessModeling,”A.WolfandA.Fuggetta,eds.,SoftwareProcess,vol.5,TrendsinSoftware:SoftwareProcess,pp.1–24.JohnWiley&Sons.,1996.W.W.Royce,“ManagingtheDevelopmentofLargeSoftware.Systems,”P(pán)roc.IEEEWESCON,pp.1–9,1970.ReprintedinR.H.Thayer,ed.,IEEETutorialonSoftwareEng.ProjectB.W.Boehm,“ASpiralModelofSoftwareDevelopmentandEnhancement,”Computer,pp.61–72,May1988.94C.Ho-StuartandS.Liu,“AnOperationalSemanticsforSOFL,”P(pán)roc.1997Asia-PacificSoftwareEng.Conf.,HongKong,IEEECSPress,1997,toappear.E.Yourdon,Modern ysis.PrenticeHallInt’l,C.Morgan,ProgrammingfromSpecifications.PrenticeHallInt’l,U.K.,A.Hall,“UsingFormalMethodstoDevelopanATCInformationSystem,”IEEESoftware,vol.13,no.2,pp.66–76,Mar.1996.S.LiuandC.Ho-Stuart,“Semi-AutomticTransformationfromFormalSpecificationstoPrograms,”P(pán)roc.Int’lConf.Eng.ComplexComputerSystems,pp.506–513,Montreal,Quebec,Canada,IEEECSPress,Oct.1996. IEEETRANSACTIONSONSOFTWAREENGINEERING,VOL.24,NO.1,JANUARYSOFL:AFormalEngineeringMethodologyforIndustrialApplicationsShaoyingLiu,Member,IEEEComputerSociety,A.JeffOffutt,Member,IEEE,ChrisHo-Stuart,YongSun,Member,IEEEComputerSociety,andMitsuruOhba—Formalmethodshaveyettoachievewideindustrialacceptanceforseveralreasons.Theyarenotwellintegratedintoestablishedindustrialsoftwareprocesses,theirapplicationrequiressignificant ionandmathematicalskills,andexistingtoolsdonotsatisfactorilysupporttheentireformalsoftwaredevelopmentprocess.WehaveproposedalanguagecalledSOFL(Structured-Object-based-FormalLanguage)andaSOFLmethodologyforsystemdevelopmentthatattemptstoaddresstheseproblemsusinganintegrationofformalmethods,structuredmethodsandobject-orientedmethodology.Constructionofasystemusesstructuredmethodsinrequirementsysisandspecifications,andanobject-basedmethodologyduringdesignandimplementationstages,withformalmethodsappliedthroughoutthedevelopmentinamannerthatbestsuitstheircapabilities.ThispaperdescrbestheSOFLmethodology,whichintroducessomesubstantialchangesfromcurrentformalmethodspractice.Acomprehensive,practicalcasestudyofanactualindustrialResidentialSuitesManagementSystemillustrateshowSOFLisused.IndexTerms—Structuredmethods,object-orientedmethodology,formalmethods,dataflowdiagrams,formal——————————?—————————1FORMALmethodshavenotbeenusedinindustrylargelybecauseitisdifficulttoapplytheminpracticalsettingsF,[2].Thereareanumberofreasonsforthis.First,theapplicationofformalmethodsrequireshigh ionandmathematicalskillstowritespecificationsandconductproofs,andtoreadandunderstandformalspecificationsandproofs,especiallywhentheyareverycomplex.Asoft-wareengineermustmakeasignificantcommitmenttolearn eproficientatthenecessaryskills.Second,existingformalmethodsdonotofferusableandeffectivemethodsforuseinwell-establishedindustrialsoftwareproc-ess.Manytextsonformalmethodsfocusonnotation,butarenotwellsuitedforhelpractitionersapplythemethodinapracticaldevelopmentprocess.Withisolatedexceptions,formalmethodsarestilllargelyperceivedasanacademicinventiondivorcedfromrealapplications.Athirdproblemisexpense.Experiencehasshownthataddingformalmethodstoadevelopmentprocesscanincursignifi-cantadditionalcosts,butthatwhenformalmethodsarefullyintegratedintoadevelopmentprocessandcostsmeasuredoverthefulllifecycle,costsmayactuallyde-crease.However,introductionofradicallynewprocessesS.LiuandM.OhbaarewiththeFacultyofInformationSciences,HiroshimaCityUniversity,4-1,3-chome,Ozukas-higashiAsaminami-Ku,Hiroshima731-31Japan.E-mail:shaoying@cs.hiroshima-cu.ac.jp.A.J.OffuttiswiththeISSEDepartment,GeorgeMasonUniversity,Fairfax,VA22030.E-mail:ofut@.C.Ho-StuartiswiththeSchoolofComputingScience,QueenslandUniversityofTechnology,Brisbane4001Australia.E-mail:Y.SuniswiththeDepartmentofComputerScience,TheQueen’sUniversityofBelfast,BelfastBT71NNNorthernIreland.E-mail:y.sun@qub.ac.uk.Manuscriptreceived30Sept.1996;revised6May1997.Forinformationonobtainingreprintsofthisarticle,pleasesende-mailto:,andreferenceIEEECSLogNumber105984.

requiresaveryexpensiveinitialoutlay,whichmostcom-paniescannotaffordgiventheconstraintsofschedule,budget,andlabor.Althoughthequalityoftheirsystemsisimportant,mostcompaniesneedtokeeptimeastheirpri-maryprioritytomeetthedemandsofthemarket.Thisviewissharedbyotherresearchersintheformalmethodscom-munity[3]Finally,effectivetoolsupportiscrucialforfor-malmethodsapplication,butexistingtoolsarenotabletosupportacompleteformalsoftwaredevelopmentprocess,althoughtoolssupportingtheuseofformalmethodsinlimitedareasareavailable[4],[5],[6].Tomakeformalmethodsmorepracticalandacceptableinindustry,somesubstantialchangesmustbemade.AdaptingFormalMethodsforThispaperproposeschangestosoftwareprocess,notation,methodology,andsupportenvironmentsforconstructingsystems.Fig.1illustrateschangesinthesoftwareprocess.First,formalmethodsoftenassumethataformalspecifica-tionofthesystemunderdevelopmentshouldbecompletedbeforeitisimplemented.Thisisimpractical.Somere-quirementsmustbeobtainedandrecordedinthespecifica-tionbeforedesignandimplementation,butothersarebet-tercapturedduringdesignand/orimplementation.Forthisreason,wedivideuserrequirementsintotwoparts,tobeobtainedindifferentstages.Thefirstpartistheuser’sprimaryfunctionalrequirements.Itisimportanttohaveafunctionalspecificationreflectingcompleteprimaryre-quirementsbeforedesigningthesoftwarebecausethisservesasacontractbetweenthedeveloperandtheuser,andasafirmbasisforsubsequentdevelopment.Forcriticalsystems,requirementsforcriticalpropertiessuchassafetyandsecurityarepartoftheprimaryfunctionalrequire-ments.Primaryrequirementsshouldbeconsistentandun-ambiguous.Thesecondpartissecondaryrequirementsforthesystem,suchasitsbackgroundtasks,noncriticalfunctions,0098-5589/98/$10.00?1998LIUETAL.:SOFL:AFORMALENGINEERINGMETHODOLOGYFORINDUSTRIAL Fig.1.Changesinthesoftwareandsomequalityaspects.Thesemayincludetheinterfacelayout,usability,andefficiency.Secondaryrequirementscanbecapturedduringdesignandimplementationwithtechniquessuchasprototy.Thesecondsoftwareprocesschangefollowsfromtheob-servationthatitisexpensiveanddifficulttoperformformalproofs.Wesuggestreplacingformalproofswithasystemofrigorousreviews.Thepurposeofrigorousreviewsistoensuretheinternalconsistencyofspecificationsatdifferentlevels,tovalidatethespecificationagainstuserrequirements,andtoensurethatdesignsorprogramssatisfytheirrequirementsspecificationsordesigns.Rigorousreviewsshouldbebasedonformalproofprinciples,butmustbeeasiertoconduct.Whilemostexistingreviewmethodstendtofocusonerrordetectionindesignorprograms,suchasParnasandWeiss’activedesignreviews[7]andFagan’sdesignandcodeinspections[8],KnightandMeyers’phasedinspectiontendstoensurethattheproductbeinginspectedpossessesrequiredproperties[9].Rigorousreviewsmaynotbeasconvincingasformalproofsforensuringcorrectness,butasoundandpracticalreviewtechniquemaybeautomaticallysupported,therebyreducingtimeandlaborcosts.Areviewshouldalsotakeintoaccounttherisksandcostsoffailure;andeitherjustifylackoffullformalproof;orelseadvisethatformalproofbetakenforhighlycriticalspecifications.Inanycase,reviewsshouldbebackedupbyrigoroustesting.Thethirdprocesschangeconcernsprototyandingactivities.Theseshouldnotbereplacedbyformalmeth-ods,buteachshouldbeusedasappropriate,forappropriatepurposes(moredetailsonthispointwillbegivenlater).Anevolutionaryapproachismorepracticalthanformalrefine-mentforsystemsdevelopment[10],becausethesoftwaredevelopmentprocessisanengineeringactivity,ratherthanapurelymathematicalprocess.Therefore,weneedbothmathematicalandengineeringtechnologytoachievequalityandproductivity.Forexample,formalspecificationscanserveasafoundationtogeneratetestdata[11],[12],[13].Mostexistingtoolsandsupportenvironmentscanhelpreducetheworkloadofspecificationconstructionandformalverification,butarenotabletoguidethedeveloperthrough

theentiredevelopment.Thismaybebecauseitishardtogiveatheoreticalfoundationforconstructionofinligentsupportenvironments,orbecausetheformalmethodsarenotsufficientlymaturetobesupportedinthatway.How-ever,asformalmethodsaremoredifficulttousethaninfor-malmethods,theiracceptancerequiresinligentsupportenvironments.Therearemanytoolsavailabletosupportsomekindsofmanipulationofformalspecifications,butmostarefocusedprimarilyonmanipulatingthenotationratherthaninligentsupportofrealsoftwaredevelopmentprocesses.Someworkhasbeendoneinthisdirection[14].InitialstepstowardstooldevelopmentforSOFLhavebeenmadeinourongoingprojectFM-ISEE1[15].Themostdifficultissueishowtodevelopasufficientsetofrulesinaknowledgebaseforsupportenvironmentstoguideandtoassistdevelopersthroughsystemsdevelopmentingeneral.Withregardtonotation,purelymathematicalnotationsdonotscalewellforlargecomplexsystemsandaredifficultforengineerstoreadandunderstand.Wesuggestthatanappropriategraphicalnotationwithprecisesemanticsshouldbeusedasaformalnotationtohelpmodelthehighlevelarchitectureofsystems,becauseitismorereadableandcanhelpindicatethehigherlevelsofstructure.Formalmathematicalnotationmaythenbeusedtodefinecompo-nentsofthesystem.Notationforconnectivesshouldbebasedonnaturallanguageratherthansymbols(forexam-ple,usingandratherthan?,orratherthan)toenhancereadability.Thisalsomakesiteasiertoenternotationusingthestandardkeyboard.Manyexistingformalnotations(suchasZ[16]orVDM-SL[17])usemathematicalsymbolsthatcannotbedirectlyenteredusingthestandardkey-board.Asupporttoolcanalleviatethisproblem,butusersmaystillfinditinconvenienttohavetwodifferentnota-tions;onethatcanbeenteredfromthestandardkeyboardandanotherfordisplayofspecifications.Naturallanguageshouldalsobeacomplementtoformalnotationinspecifi-cationstofacilitatetheirinterpretation.Effectiveformalspecificationrequiresabalancedmixofgraphicalnotation,naturallanguage,andmathematicalnotation,asinFig.Formalmethodsalonearenotsufficienttocopewiththecomplexityofsystemdevelopment.Anappropriateinte-grationofstructuredmethods,object-orientedmethodol-ogy,andformalmethodsmaycombinetheadvantagesofthosethreeapproachestoimprovethequalityandeffi-ciencyofthesoftwaredevelopmentprocess.Sincethisisoneofthemostimportantissuesaddressedinthispaper,itisdiscussedindetailinSection1.2.Itishopedthatthesechangeswillmeanthatformalmethodsdonotneedtobelimitedtosafety-criticalsystems,butcanbeappliedtoothercomplexcomputersystemsas1.FM-ISEEstandsforFormalMethodsandInligentSoftwareEngi-neeringEnvironments.ThisprojectisaninternationalcollaborationamongHiroshimaCityUniversityandKyushuUniversityofJapan,TheQueen’sUniversityofBelfast,UnitedKingdom,GeorgeMasonUniversity,andQueenslandUniversityofTechnology,Australia. IEEETRANSACTIONSONSOFTWAREENGINEERING,VOL.24,NO.1,JANUARYFig.2.Changesinnotation,methodology,andapplicationIntegrationofTwoapproacheshavebeenadoptedtointegrateformalmethodswithstructuredmethods.OneistousetheYour-donortheDeMarcoapproachtoconstructadataflowdia-gramanditsassociateddatadictionary,andthentorefinethedataflowdiagramintoaformalspecificationbydefin-ingdataflowsandbottomlevelprocesseswiththeformalnotations.TheexamplesofthisapproachincludeSemmensandAllen’sworkonintegratingYourdon’smethodandZ[18],Bryant’sworkonYourdon’smethodandZ[19],Fraser’sworkondataflowdiagramsandVDM[20],andPlatandhiscolleagues’integrationofdataflowdiagramsandVDM[21].Theotherapproachistoincorporatetradi-tionaldataflowdiagramnotationintoaformalspecifica-tionlanguagetoprovideamechanismforstructuringsys-temspecificationsandagraphicalviewforthesystemspecification.Inthisway,dataflowdiagramsaretreatedaspartofformalspecifications.TheexamplesofthisapproachincludeLiu’sworkondesigningtheFormalRequirementsSpecificationMethodandtheStructuredandFormalSystemDevelopmentLanguageinwhichDeMarcodataflowdia-gramsarecombinedwithVDM[22],[23].Tointegrateformalmethodsandobject-orientedology,formalmethodsareusuallyusedtospecifythefunc-tionalityofoperationsdefinedinclasses.ExamplesofthisapproachincludeVDM++[24]andObject-OrientedZ[25].Theaboveresearchattemptstomakestructuredmeth-ods,object-orientedmethodologyandformalmethodsmoreusable.However,tothebestofourknowledge,nopreviousefforthasbeenmadetointegrateallthreeap-proaches.Webelievethattheyarecomplementaryap-proachestosystemsdevelopment,andthatallthreeshouldbeintegratedforumbenefit.Tosupportthechangesinformalmethodsandto ethedeficienciesmentionedabove,weproposealan-guagecalledSOFL(Structured-Object-based-FormalLan-guage)andtheSOFLmethodology.SOFLintegratesstruc-turedmethodsbasedonextendedandformalizeddataflowdiagrams,object-orientedmethodology,andVDM-SLfor-malnotation.ThemotivationforSOFListhatexistinglan-guagesarenotwellsuitedtosupportingourproposedchangestothesoftwareprocess,notation,andmethodol-ogy,andthatexistingapproachesforintegratingdifferentmethodologiesdonotgiveaconsistentandsystematic

combinationofthedifferentkindsofnotationsthatcanbeusedtohelpunderstand,refine,verify,andimplementSOFLsupportstheuseofstructuredmethodsforre-quirementsysisandspecificationintwoways.First,byprovidingappropriate ionandfunctional sitionfacilities.Second,byprovidingausablemechanismforcommunicationbetweenthedeveloperandtheusertovalidatethespecification.Itcanhelpaprojectteamdistrib-utetasks,increasingsoftwareproductivity.Ontheotherhand,whenclasshierarchiesandinheritanceareusedap-propriay,theyincreaseinformationhidingandcompo-nentreusability.Thisisdifferentfromtheclassicalobject-orientedap-proachinwhichdatastructuresaredesignedtoreflectrealworldobjects.Therearethreedifficultieswithusinganob-ject-orientedapproachforrequirementsysis.First,itcanbedifficulttoidentifyusefulobjectswhenthedevel-operisnotfamiliarwiththeapplication.Somegraphicalnotationsexist[26],buttheyonlyhelptoexpressclasses,objectsandtheirrelations,nottoidentifyobjectsandclasses.Second,evenifobjectsareidentifiedinearlystages,thespecificdemandsfromtherestofthesystemmaystillbeunclear,soitmaynotbeclearexactlywhatareappropriatemethodsandhowtheyshouldbedefined.Structuredmethodsprovideawaytohelpidentifyusefulobjectsandtheirnecessarymethodsby posingandevolvinghighlevelspecificationstolowerlevelspecifica-tions.Anotherdifficultyconcernscommunicationbetweenthedeveloperandtheuser.Usersoftenprefertothinkintermsoftasksratherthanobjects(especiallyifnotwelltrainedinobject-orientedmethodology).SOFLusesstructuredmethodsforrequirementsandspecificationandanobject-basedapproachfordesignandimplementation.Duringboththestructuredandob-ject-baseddevelopmentofthesystem,formalmethodscanbeappliedtoprovidehighqualityspecificationsandverifi-cationsofvariouslevelsofthesystem.SOFLisintendedtoallowflexibilityinthecompletenessofspecifications,therebyallowingsystemdeveloperstobalancethebenefitsthatcanbeobtainedbyusingformalmethodsandthecon-veniencethatcanbegainedbyusinginformalapproaches(withintheSOFLframework).Forexample,ifdevelopersprocessinadataflowdiagram)atonelevel,theycanpartiallyspecifythecomponentbygiving pletepreconditionand/orpostcondition(inanextremecase,bothpreconditionandpostconditionofthecomponentmightbetrue)withdetailstobegivenmorec