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

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