SOFL一種為工業應用的形式化工程方形式化方法沒有取得廣泛的工業認可的原因有多種。他們沒能很好的集成到已建立的工業軟件過程當中，對他們的應用需要有很強的抽象與數學技巧，還有現存的工具不能滿意的支持完整的形式化軟件開發過程。我們提出了一種叫做SFL的語言以及對于系統開發的SOF計階段用面向SOF了SLSOF如何使用。介的時候閱讀和理解形式化歸約更難了。一個軟件工程師必須花很多精力來學些必要的技負擔的起。雖然他們的系統質量很重要，大部會優先考慮先滿足市場的需求。這個觀改進形式化方法來適應工業應用件過程中的改變。首先，形式化方法通常假定系統的形式化歸實現前要全部完成。這是不欠實際的。有些需求在設計之前必須獲得并記錄在歸約中，但是其他的卻可以再設計的時候獲取。因為這個原因，我們把用戶的需求分成兩部分，分別在不同的階段獲面的布局，可用性，有效性。次級需求可以再設計階段用原型技術來獲得。確認對用戶需求的歸約，以及確認設計和程序能夠滿足需求歸約或設計。嚴格基于形式化證明原則，但是更容易執行。但是大部分現存的方法都是集中在設計和程序階段的錯誤，比如Parnas和Weiss的活動設計[7]，Fagan的設計和代碼[8]，還有Knight，Meyers的階段傾向于檢測的產品能出來請求屬性。嚴格審在確認正確性方面或許不如形式化證明那么令人信服，但是一個不錯的且可行的技術或以自動支持，因而可以減少時間和勞動費用。也應該考慮到失敗的風險和費用；兩者都缺乏完整的形式化證明；或者建議形式化證明應該用于較次的關鍵歸約。無論何種情況，都應該支持嚴格測考慮到記號，純數學記號不能很好的擴充來支持大的復雜系統開發，對工程師們來說也因的（比如[16],VDM-S[17]）都使用數學符號這樣不能用標準鍵盤直接輸入記號。支持工具可以解決這個問題，但是用戶會覺得有兩套記號很不方便；一個用于從標準鍵盤輸入記號，另一個則用于向顯示屏輸出。自然語言對于形式化歸約中的形式化記號是完整的以至可以利用他們的解釋。有效的形式化歸約需要有個在圖形記號，自然語言，數學記號的綜合平衡，如圖2所示。也是這篇討論的重點話題，這將在1.2部分進行詳細討論。兩者方式可以采用來集成形式化方法和結構化方法。一種是使用Yourdon或者DeMarco方需求歸約方法和結構化形式化方法的工作，這個工作將MeMarco數據流圖和VDM組合起來程，記號和方法學中所改進，同時現有的方法對于集成不同的方法不能給出一個一致這是不同于經典的面向對象方法，經典面向對象中數據結構是設計用料反映現實世界的對象。在使用面向對象方法就行需求分析只要有三個的。第一，當開發者不熟悉應用領域時，定義有用的對象很。有些圖形記號工具可以使用[26]，但是這些只是幫助表定義他們并不能被確切說明。結構化方法通過分解和演化歸約到低層歸約可以給我們提供有用的對象和必須的方法。最后一個在于開發者和用戶之間的溝通。用戶通常從任務SOF使用結化方來行求分和約用面對方法設。結化SOF通過描述SOFL的語法和非形式化語義從它初步描述中來定義和改進SOFL語言。通過對一個居民公寓管理系統來證明SOFL語言的能力和可用性這邊的余下部分如下組織。第二部分闡述使用SOFL的軟件開發過程。第三部分描述使用SOFL的軟件過程軟件過程是一個已經取得很多研究者關注的領域[2]。倡導SOF的軟件過程是一個特殊化的瀑布開發模型[29]3SOFL用嚴格來驗證相對于需求歸約設計和相對于設計的程序是非常重要的。動態開發則是發現系統的動態特征，通過用戶的需要來驗證系統，以及通過原型和測試來獲取的需個層次，當前歸約的某個部分就可以構建原型并進試，這可以與系統的剩余部分的靜態開發同時進行。同樣，在某些歸約構造原型并測試后，它就能捕獲的需要和設計的構造軟件系統的SOFL方法學圖4SOFL歸約的圖5SOFL實現的案例研究背景SF學。這個局部的住宅套房公司管理許多業務和資源。業務包括前臺桌面服務，房間服務，服務，報告服務，體育服務，金融和安全服務。資源包括50個套間（200單人間，100100305020個豪宅22個餐廳和一個游泳池。這個公司通過電腦來支持前臺活動，但是沒有電腦系統來支持完整的管理。因此住宅套房公司的經理和我們合作來開發這個軟件系統的歸約。識，但是懂得管理系統。通過初試的需求分析，我們在一個次的抽象層面對這個管理系構造條件數據流圖和歸約模條件數據流條件數據流圖是一個帶箭頭的圖，由數據流，數據和條件過程組成。數據流是標有數據類型的，代表在條件過程之間轉換的一包數據。數據則是某種類型的變量來代在CDFDs和DeMarco和Yourdon數據流圖之間有四種重要的畫一個CDFD可以有助于描述一個系統結構的整體樣供了定義與歸約模塊相CDFD圖6CDFDs圖8需求歸約的頂層歸約模一個重要的議題是如何定義與CDFD相關聯的歸約模塊。我們使用下面的四規則1：每個數據流，除了在靜態數據和條件過程之間的，每個在CDFD中的數據為外部變量獲得，不必要用多于的數據來轉化中的變量。然而在過程中間轉移的數據將量則指向數據，前置后置條件則定義了功能，一個分解和評論。參數列表的語法則是為2)不同的端口被符號|分割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中條件流圖中對應歸約模參數res-req,rep-req,room-no,d-rep,check-out-bill可以由數據流不同的名字因為按出現SOFL使用VDM格式的語義，這里變量將綁定他們類型的一個值，或者是缺失，這表明還bound（res-req)或者bound(rep-req)或者bound(room-no),值表明或者res-req,rep- 或room-no有一個值。前置條件由操作語義來確保bound(res-req)或者P(rep-req,room-no),這里P（rep-req,room-no)是一個斷言依賴于或者rep-req,room-no,但是不依賴res-這個斷言需要通過rprq以及roomno來確保；條件過程僅僅定義了rprq或者roomnoifbound（rep-req)elseifroom-no>5elsebound(dummy)r-rep,rep-req和room-no綁定，這是一個明確的前置條件。這個不能直接表達，因為VDM能斷言一個值沒有綁定。然而如果（rs-req,rep-req,room-no)是明確的前置條件，那么完整的前置條件是p(res-req,ni,nil)或者p(nl,repreq,ni),或者p(ni,ni,room-no)相似的規則可言應用于后者條件。規則3：對一個條件過程如果有數據流從數據到條件過程但是沒有數據流從條件過程c-processA()extwrwrs:typeprePreA(s)extrds:TypeprePreB(S)這里~s和s代表條件過程A激活之前的值和之后的應用上面的四個規則，我們可以為圖8中的CDFD構造如下分CDFD.條件過程的分解定義了輸入時如何轉換到輸出的。分解必須滿足中給定的約束。這樣一種分解不僅是條件過程的定義，同時也可以擴展其功能。因而這就允許SOFL支在SOFL分解和經典的數據流圖之間有三個在低層外加的數據流被當做是條件過程的內部狀態變量。這些另外的數據流有一個 e-rep,events-案例研究中的經驗表明在獲得數據和條件過程的抽象和封裝方面這個規則比起Yourdon區別2.一個條件過程可以分解成數個低層次的當一個條件過程必須分解成幾個低層的彼此不連接的CFD把這些不互連的FD組織起來的可行方法是把每接的部分視為一個CFD,然后分別8ne-nformtion可以被分解成3個CFD.其中兩個在圖12和圖1312中的FD的歸約模塊在附錄中給出。句話說，歸約模塊中的常量，類型，類和的變量的周期是這個歸約模塊本身和它的繼承如何使用分這可以由助于澄清在CDFD中國的數據流，數據，和條件過程的歧義SOFL提供下面的標準來選擇要分解的過域的時候或者有過相似應用領域系統開發經驗的時候，這個方很有效。演和結構的改變。。條件過程可以通過構造相應低層的CDFD來分解從而重定義這個過程。而下面的方法在構造歸約的時候使用演化和分解師有效的。分解和演，化史交錯的，但是通常分解先開始，然后如果必要可以相應的進行演化。當在分解條件過程的時候如果發現條件過程本身的改變時必要的，則條件過程或者相應的CDFD的演化就應該實施。演化的結果是另一個層次結構的CDFD，它正確的反映了在條件過程和它的分解CDFD的分解關系。通過實施分解和演化，我們可以把頂層的CDFD轉換成一個最終的歸約，它包括在圖結構化的需求歸約轉換基于對象的設計得質量屬性比如可靠性，可讀小學，可重用性，信息封裝，還有可性。指導原則1.遵循需求歸約中的CDFD的層次結構圖把系統設計成CDFDs形式的層次結這不意味著是一個嚴格的一對一的關系。可以采取一些改變來改進設計的質量。在需求歸約中的有些過程代表了現實世界的實體而不是軟件系統的一部分，比如圖8中的utom.在絕大部分案例中需求歸約中的CF圖16中的在居民套間管理系統中的需求歸約的CFD是源自圖8和圖12中的需求歸約。作為輸入，并產生相同類的對象robjet.其他的條件過程像hknSrvie以及hk-Out-Srvie也處理其他類的對象。呆箭頭的間斷線代表控制數據流，她們沒有攜帶實際的數據，但是卻可以激活一個條件過程。圖16設計的頂層以使用基于對象的設計技術，為每個數據創造類的。在需求中的將變成在設計中的類的。某些條件過程可以作為每個類中的方法來實現。這個方法通常要改變條件過程歸約的結構，把代表數據的外部變量放入過程的輸入和輸出參數中。選擇何種方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- 把設計轉換成程序把頂層的歸約模塊轉換陳實現模塊Program同時每個其他的歸約模塊都對應應該實把頂層歸約模塊的頂層CDFD實現為開始的實現模塊中的main方法模塊使用了這個條件過程，而所的過程其過程體則源自與它的所分解的CDFD。比如我們轉換圖16所示的頂層CDFD以及它的歸約模塊成實現模塊rlist:ReservatioList;rooms:Rooms;methodcreate();methodChange(change-methodCancel(cancel-methodmethodCheck- bill:CheckOutBill;methodmethodCheck-Out(room-Algorithm(Reserve-procedureReserve-procedureCheck-In-procedureCheck-Out-面向對象轉是作為直接變換的對應，但是又如下的區別：在設計中的每個CDFD，創造一個類，這個類方法；如果一個條件過程分解成了低層次的CDFD，則它的已轉換的方法的主體應該是低層讓我們再拿圖16中的頂層CDFD和它的歸約作為這個方法的例子。它轉換成程序如下：methodcreate(...);methodCheck-In-methodReport-Service(...);substate:RS-class;proceduremainstate: 這個CDFD可以轉換成類RS-class.RS-class變量substate以及它潛在的方法可以在Report-Service方法體中4SOFL演SOFCFDs的層次結構圖可以幫助獲得系統的整體視圖，這就提供了一個決定哪些組件需要進一步定義的基礎。寫形式化的歸約可以），并提高CDFDsCFDs提供一個易于理解的結構，它允許開發者的分解，演變，修改和的階段中態的進程或數據的規范（包括需求規格說明和設計）。理系統。開展了次的需求分析和繪圖高水平CDFDs（無定型還）之后，我們就能與經理結構來，盡管這被建議使用。開發者可以通過分別畫和歸約CDFD來為現實世界的系統構造第四，在歸約中的CDFDs和類構造使得SOFL語言能夠支持面向對象把它運用到大規模工程的一個。在歸約和設計階段，如果開發者能夠有效的構造建立結貢化方法可以有效的幫助構造需求歸約而面向對象方法則有助于系統設計。歸約方法同當前正在活動的研究和未來的研究主動的在下面這些方面追求進一步研究：1）將SOFL運用到更復雜的工業系統中2）嚴格技術，3）基于形式化歸約的程序測試，4）CDFDs和條件過程到程序的自動轉換5）基于現有的圖形原型工具對SOFL把SFL運用到復雜系統可以為SOFL方法是有效性提供數據，還能傳達一下開發問題。SOFL如何被工業環境中的工程團隊使用呢？OFL又如何影響工程管理和溝通？SOFL如何響件證確和本第作正與地電公合調SOFL如何運用來開發鐵路交叉控制系統。我們已經開始研究嚴格技術，并有兩個正在進行的工程。第一個是為條件過程生成除了嚴格技術，我們在開展基于SOFL歸約的程序測試研究[13].通過已經建立好的準參考文S.Liu,V.Stavridou,andB.Dutertre,“ThePracticeofFormalMethodsinSafetyCriticalJ.SystemsandSoftware,vol.28,pp.77–87,D.Craigen,S.Gerhart,andT.Ralston,“FormalMethodsRealityCheck:IndustrialUsage,”Proc.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,”Proc.WIFT‘95:WorkshopIndustrial-StrengthFormalSpecificationTechniques,Apr.1995.D.L.ParnasandD.M.Weiss,“ActiveDesignReviews:PrinciplesandPractices,”Proc.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,”Proc.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,”Pitman,L.T.Semmens,R.B.France,andT.W.G.Docker,“IntegratedStructuredysisandFormalSpecificationTechniques,”TheComputerJ.,vol.35,no.6,1992.A.Bryant,“StructuredMethodologiesandFormalNotations:DeveloAFrameworkSynthesisandInvestigation,”Proc.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,”Proc.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,”Proc.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,”Proc.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,”Proc.IEEEWESCON,pp.1–9,1970.ReprintedinR.H.Thayer,ed.,IEEETutorialonSoftwareEng.ProjectB.W.Boehm,“ASpiralModelofSoftwareDevelopmentandEnhancement,”Computer,pp.61–72,May1988.94C.Ho-StuartandS.Liu,“AnOperationalSemanticsforSOFL,”Proc.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,”Proc.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