软件工程：alSpecifications.ppt

Chapter9,FormalSpecifications,FormalSpecification,Techniquesfortheunambiguousspecificationofsoftware,Objectives,ToexplainwhyformalspecificationtechniqueshelpdiscoverproblemsinsystemrequirementsTodescribetheuseofalgebraictechniquesforinterfacespecificationTodescribetheuseofmodel-basedtechniquesforbehaviouralspecification,Topicscovered,FormalspecificationinthesoftwareprocessInterfacespecificationBehaviouralspecification,Formalmethods,FormalspecificationispartofamoregeneralcollectionoftechniquesthatareknownasformalmethodsTheseareallbasedonmathematicalrepresentationandanalysisofsoftwareFormalmethodsincludeFormalspecificationSpecificationanalysisandproofTransformationaldevelopmentProgramverification,Acceptanceofformalmethods,FormalmethodshavenotbecomemainstreamsoftwaredevelopmenttechniquesaswasoncepredictedOthersoftwareengineeringtechniqueshavebeensuccessfulatincreasingsystemquality.HencetheneedforformalmethodshasbeenreducedMarketchangeshavemadetime-to-marketratherthansoftwarewithalowerrorcountthekeyfactor.FormalmethodsdonotreducetimetomarketThescopeofformalmethodsislimited.Theyarenotwell-suitedtospecifyingandanalysinguserinterfacesanduserinteractionFormalmethodsarehardtoscaleuptolargesystems,Useofformalmethods,FormalmethodshavelimitedpracticalapplicabilityTheirprincipalbenefitsareinreducingthenumberoferrorsinsystemssotheirmaiareaofapplicabilityiscriticalsystemsInthisarea,theuseofformalmethodsismostlikelytobecost-effective,Specificationinthesoftwareprocess,Specificationanddesignareinextricablyintermingled.Architecturaldesignisessentialtostructureaspecification.Formalspecificationsareexpressedinamathematicalnotationwithpreciselydefinedvocabulary,syntaxandsemantics.,Specificationanddesign,Specificationinthesoftwareprocess,Specificationtechniques,AlgebraicapproachThesystemisspecifiedintermsofitsoperationsandtheirrelationshipsModel-basedapproachThesystemisspecifiedintermsofastatemodelthatisconstructedusingmathematicalconstructssuchassetsandsequences.Operationsaredefinedbymodificationstothesystemsstate,Formalspecificationlanguages,Useofformalspecification,FormalspecificationinvolvesinvestingmoreeffortintheearlyphasesofsoftwaredevelopmentThisreducesrequirementserrorsasitforcesadetailedanalysisoftherequirementsIncompletenessandinconsistenciescanbediscoveredandresolvedHence,savingsasmadeastheamountofreworkduetorequirementsproblemsisreduced,Developmentcostswithformalspecification,Interfacespecification,Largesystemsaredecomposedintosubsystemswithwell-definedinterfacesbetweenthesesubsystemsSpecificationofsubsysteminterfacesallowsindependentdevelopmentofthedifferentsubsystemsInterfacesmaybedefinedasabstractdatatypesorobjectclassesThealgebraicapproachtoformalspecificationisparticularlywell-suitedtointerfacespecification,Sub-systeminterfaces,Thestructureofanalgebraicspecification,sort,imports,Inf,or,maldescr,iptionofthesor,tanditsoper,ations,Oper,ationsignaturessettingoutthenamesandthetypesof,theparameterstotheoperationsdefinedoverthesort,Axiomsdefiningtheoper,ationso,v,erthesor,t,(Gener,icP,ar,ameter),Specificationcomponents,IntroductionDefinesthesort(thetypename)anddeclaresotherspecificationsthatareusedDescriptionInformallydescribestheoperationsonthetypeSignatureDefinesthesyntaxoftheoperationsintheinterfaceandtheirparametersAxiomsDefinestheoperationsemanticsbydefiningaxiomswhichcharacterisebehaviour,Systematicalgebraicspecification,AlgebraicspecificationsofasystemmaybedevelopedinasystematicwaySpecificationstructuring.Specificationnaming.Operationselection.InformaloperationspecificationSyntaxdefinitionAxiomdefinition,Specificationoperations,Constructoroperations.OperationswhichcreateentitiesofthetypebeingspecifiedInspectionoperations.OperationswhichevaluateentitiesofthetypebeingspecifiedTospecifybehaviour,definetheinspectoroperationsforeachconstructoroperation,OperationsonalistADT,ConstructoroperationswhichevaluatetosortListCreate,ConsandTailInspectionoperationswhichtakesortlistasaparameterandreturnsomeothersortHeadandLength.TailcanbedefinedusingthesimplerconstructorsCreateandCons.NoneedtodefineHeadandLengthwithTail.,Listspecification,Head(Create)=Undefined,exception,(emptylist),Head(Cons(L,v)=,if,L,=Create,then,v,else,Head(L),Length(Create)=0,Length(Cons(L,v)=Length(L)+1,T,ail(Create)=Create,T,ail(Cons(L,v)=,if,L,=Create,then,Create,else,Cons(T,ail(L),v),sort,List,imports,INTEGER,Definesalistwhereelementsareaddedattheendandremo,v,ed,fromthefront.,Theoper,ationsareCreate,whichbr,ingsanemptylist,intoe,xistence,Cons,whichcreatesane,wlistwithanaddedmember,Length,whiche,v,aluatesthelistsiz,e,Head,whiche,v,aluatesthefront,elementofthelist,and,T,ail,whichcreatesalistb,yremo,vingtheheadfromits,inputlist.UndefinedrepresentsanundefinedvalueoftypeElem.,Create,List,Cons(List,Elem),List,Head(List),Elem,Length(List),Integer,T,ail(List),List,LIST,(Elem),Recursioninspecifications,OperationsareoftenspecifiedrecursivelyTail(Cons(L,v)=ifL=CreatethenCreateelseCons(Tail(L),v)Cons(5,7,9)=5,7,9Tail(5,7,9)=Tail(Cons(5,7,9)=Cons(Tail(5,7),9)=Cons(Tail(Cons(5,7),9)=Cons(Cons(Tail(5),7),9)=Cons(Cons(Tail(Cons(,5),7),9)=Cons(Cons(Create,7),9)=Cons(7,9)=7,9,Interfacespecificationincriticalsystems,ConsideranairtrafficcontrolsystemwhereaircraftflythroughmanagedsectorsofairspaceEachsectormayincludeanumberofaircraftbut,forsafetyreasons,thesemustbeseparatedInthisexample,asimpleverticalseparationof300misproposedThesystemshouldwarnthecontrollerifaircraftareinstructedtomovesothattheseparationruleisbreached,Asectorobject,CriticaloperationsonanobjectrepresentingacontrolledsectorareEnter.AddanaircrafttothecontrolledairspaceLeave.RemoveanaircraftfromthecontrolledairspaceMove.MoveanaircraftfromoneheighttoanotherLookup.Givenanaircraftidentifier,returnitscurrentheight,Primitiveoperations,ItissometimesnecessarytointroduceadditionaloperationstosimplifythespecificationTheotheroperationscanthenbedefinedusingthesemoreprimitiveoperationsPrimitiveoperationsCreate.BringaninstanceofasectorintoexistencePut.AddanaircraftwithoutsafetychecksIn-space.DetermineifagivenaircraftisinthesectorOccupied.Givenaheight,determineifthereisanaircraftwithin300mofthatheight,Sectorspecification,Specificationcommentary,UsethebasicconstructorsCreateandPuttospecifyotheroperationsDefineOccupiedandIn-spaceusingCreateandPutandusethemtomakechecksinotheroperationdefinitionsAlloperationsthatresultinchangestothesectormustcheckthatthesafetycriterionholds,Behaviouralspecification,AlgebraicspecificationcanbecumbersomewhentheobjectoperationsarenotindependentoftheobjectstateModel-basedspecificationexposesthesystemstateanddefinestheoperationsintermsofchangestothatstateTheZnotationisamaturetechniqueformodel-basedspecification.Itcombinesformalandinformaldescriptionandusesgraphicalhighlightingwhenpresentingspecifications,ThestructureofaZschema,Aninsulinpump,Modellingtheinsulinpump,Theschemamodelstheinsulinpumpasanumberofstatevariablesreading?dose,cumulative_doser0,r1,r2capacityalarm!pump!display1!,display2!Namesfollowedbya?areinputs,namesfollowedbya!areoutputs,Schemainvariant,EachZschemahasaninvariantpartwhichdefinesconditionsthatarealwaystrueFortheinsulinpumpschemaitisalwaystruethatThedosemustbelessthanorequaltothecapacityoftheinsulinreservoirNosingledosemaybemorethan5unitsofinsulinandthetotaldosedeliveredinatimeperiodmustnotexceed50unitsofinsulin.Thisisasafetyconstraint(seeChapters16and17)display1!showsthestatusoftheinsulinreservoir.,Insulinpumpschema,Thedosagecomputation,TheinsulinpumpcomputestheamountofinsulinrequiredbycomparingthecurrentreadingwithtwopreviousreadingsIfthesesuggestthatbloodglucoseisrisingtheninsulinisdeliveredInformationaboutthetotaldosedeliveredismaintainedtoallowthesafetycheckinvarianttobeappliedNotethatthisinvariantalwaysapplies-thereisnoneedtorepeatitinthedosagecomputation,DOSAGEschema,Outputschemas,TheoutputschemasmodelthesystemdisplaysandthealarmthatindicatessomepotentiallydangerousconditionTheoutputdisplaysshowthedosecomputedandawarningmessageThealarmisactivatedifbloodsugarisverylow-thisindicatesthattheusershouldeatsomethingtoincreasetheirbloodsugarlevel,Outputschemas,Schemaconsistency,Itisimportantt