欢迎来到天天文库
浏览记录
ID:38247687
大小:73.00 KB
页数:7页
时间:2019-06-06
《What is Formal Methods》由会员上传分享,免费在线阅读,更多相关内容在行业资料-天天文库。
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
此文档下载收益归作者所有