資源描述：
《What is Formal Methods》由會員上傳分享，免費(fèi)在線閱讀，更多相關(guān)內(nèi)容在行業(yè)資料-天天文庫。
1、WhatisFormalMethods?"FormalMethods"referstomathematicallyrigoroustechniquesandtoolsforthespecification,designandverificationofsoftwareandhardwaresystems.Thephrase"mathematicallyrigorous"meansthatthespecificationsusedinformalmethodsarewell-formedstatementsinamathematicallogicandthattheformalv
2、erificationsarerigorousdeductionsinthatlogic(i.e.eachstepfollowsfromaruleofinferenceandhencecanbecheckedbyamechanicalprocess.)Thevalueofformalmethodsisthattheyprovideameanstosymbolicallyexaminetheentirestatespaceofadigitaldesign(whetherhardwareorsoftware)andestablishacorrectnessorsafetyprope
3、rtythatistrueforallpossibleinputs.However,thisisrarelydoneinpracticetoday(exceptforthecriticalcomponentsofsafetycriticalsystems)becauseoftheenormouscomplexityofrealsystems.Severalapproachesareusedtoovercometheastronomically-sizedstatespacesassociatedwithrealsystems:·Applyformalmethodstorequi
4、rementsandhigh-leveldesignswheremostofthedetailsareabstractedaway·Applyformalmethodstoonlythemostcriticalcomponents·Analyzemodelsofsoftwareandhardwarewherevariablesarediscretizedandrangesdrasticallyreduced.·Analyzesystemmodelsinahierarchicalmannerthatenables"divideandconquer"·Automateasmucho
5、ftheverificationaspossibleAlthoughtheuseofmathematicallogicisaunifyingthemeacrossthedisciplineofformalmethods,thereisnosinglebest"formalmethod".Eachapplicationdomainrequiresdifferentmodelingmethodsanddifferentproofapproaches.Furthermore,evenwithinaparticularapplicationdomain,differentphaseso
6、fthelife-cyclemaybebestservedbydifferenttoolsandtechniques.ForexampleatheoremprovermightbebestusedtoanalyzethecorrectnessofaRTLleveldesriptionofaFastFourierTransformcircuit,whereasalgebraicderivationalmethodsmightbestbeusedtoanalyzethecorrectnessofthedesignrefinementsintoagate-leveldesign.Th
7、ereforetherearealargenumberofformalmethodsunderdevelopmentthroughouttheworld.SeeWorldWideWebLibraryofFormalMethods.Thereisagrowingsetofsuccessstoriesinapplyingformalmethodstorealapplications:·FormalMethodsApplication:AnEmpiricalTaleofSoftwareDevelo
