Lecture17FormalModelingMethods

《Lecture17FormalModelingMethods》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、Lecture17:FormalModelingMethodsFormalModelingTechniquesDefinitionofFMWhyuseFM?ProgramSpecificationvs.RequirementsModelingExampleFormalMethods:RSMLSCRRMLTelosAlbertIITipsonformalmodelingWhatareFormalMethods?BroadView(Leveson)applicationofdiscretemathematicstosoftwareen

2、gineeringinvolvesmodelingandanalysiswithanunderlyingmathematically-precisenotationNarrowView(Wing)Useofaformallanguageasetofstringsoversomewell-definedalphabet,withrulesfordistinguishingwhichstringsbelongtothelanguageFormalreasoningaboutformulaeinthelanguageE.g.formalp

3、roofs:useaxiomsandproofrulestodemonstratethatsomeformulaisinthelanguageForrequirementsmodeling…Anotationisformalif:…itcomeswithaformalsetofruleswhichdefineitssyntaxandsemantics.…therulescanbeusedtoanalyseexpressionstodetermineiftheyaresyntacticallywell-formedortoprovep

4、ropertiesaboutthem.FormalMethodsinSoftwareEngineeringWhyformalize?RemovesambiguityandimprovesprecisionToverifythattherequirementshavebeenmetToreasonabouttherequirements/designsPropertiescanbecheckedautomaticallyTestforconsistency,exploreconsequences,etc.Toanimate/execu

5、tespecificationsHelpswithvisualizationandvalidation…becausewehavetoformalizeeventuallyanywayNeedtobridgefromtheinformalworldtoaformalmachinedomainWhypeopledon’tformalize!FormalMethodstendtobelowerlevelthanothertechniquesTheyincludetoomuchdetailFormalMethodsconcentrateo

6、nconsistent,correctmodels…mostofthetimeyourmodelsareinconsistent,incorrect,incomplete…Peoplegetconfusedaboutwhichtoolsareappropriate:specificationofprogrambehaviourvs.modelingofrequirementsformalmethodsadvocatesgettooattachedtoonetool!Formalmethodsrequiremoreeffort...a

7、ndthepayoffisdeferredWhattoformalize?modelsofrequirementsknowledge(sowecanreasonaboutthem)specificationsofrequirements(sowecandocumentthemprecisely)Specificationsofprogramdesign(sowecanverifycorrectness)VarietiesofformalanalysisConsistencyanalysisandtypechecking“Isthef

8、ormalmodelwell-formed?”Assumes“well-formedness”ofthemodelcorrespondstosomethinguseful…Validation:Animatethemodelonsma