Managing Verification Activities Using SVM

BillAldrich1,AnsgarFehnker2,PeterH.Feiler3,ZhiHan2,BruceH.Krogh2,

EricLim1,andShivaSivashankar4

23

TheMathworks,Inc.,3AppleHillDrNatick,MA01760-2098

Dept.Elec.andComp.Eng.,CarnegieMellonUniversityPittsburgh,PA15213SoftwareEngineeringInstitute,CarnegieMellonUniversityPittsburgh,PA152134

Emmeskay,Inc.,44191PlymouthOaksBlvdSuite300,Plymouth,MI48170

1

Abstract.SVM(SystemVerificationManager)managestheapplica-tionofverificationmethodsformodel-baseddevelopmentofembeddedsystemsbyprovidingintegratedrepresentationsofrequirements,systemarchitecture,modelsandverificationmethods.DevelopedinJavawithinMATLAB󰀁,SVMsupportsalltypesoftoolsformodellingandverifica-tionthroughanextensibleframeworkofdataandcodingstructures.ThispaperpresentsthemainfeaturesofSVMandillustratesitsapplicationtoembeddedcontrolandsignalprocessingsystems.

1Introduction

SVM(SystemVerificationManager)supportsmodel-baseddesignofembed-dedsystemsoftwarebyprovidinganintegratedenvironmentforspecifyingandmanagingtherelationshipsbetweensystemrequirements,systemarchitectures,systemmodels,verificationmethods,andresultsofverificationactivities.Im-plementedinJavawithintheMATLAB󰀁environment,SVMisanextensibleenvironmentdesignedtosupporttheuseofmultiplemodelling,simulation,andverificationtools.SVMobjectsencapsulatetheinformationrequiredforman-agingthedevelopmentprocesswithpointerstotheactualmodelsandtoolsusedtocarryoutthedesign.Thus,SVMfacilitatesmodel-baseddevelopmentwithoutimposingconstraintsonthemodelsormethodsusedfordesignandimplementation.

SVMprovidesmultipleviewsthatallowthesystemdesignprocesstoevolvealongseveraldimensionswithoutadvocatingorenforcingaparticulardesignprocessormethodology.Requirements,forexample,canbeentered,imported,updated,andelaboratedasthesystemdevelops.Newmodelsandverificationmethodscanbeintroducedwhenevertheyareneeded.Differentrepresentations(calledvariants)ofcomponentsinthesystemarchitecturecanbedefinedandinvokedasthedesignmovesfromalgorithmdevelopmenttoexecutablecodeforthetargetprocessor.SVMprovidesseveralfeaturesformodel-baseddevel-opmentthathavenotbeenintegratedpreviouslyintoasingletool,including:requirementstraceability,systemarchitecture,modelmanagement,verificationactivities,andresultsmanagement.

Section2describesthemainfeaturesofSVM.Thesefeaturesarethenillus-tratedforanembeddedcontrollerinanautomotiveengineapplication(Sect.3)andasignalprocessingapplication(Sect.4).Section5summarizesthecontri-butionsofthisworkandplansforfuturedevelopment.

2OverviewofSVM

SVMdoesnotprescribeaparticulardevelopmentapproach.Instead,itsupportsarangeofdevelopmentprocesses.Ononehanditsupportsthedevelopmentofasystemfromrequirementsintoasystemarchitecturethatgetsrealizedthroughaseriesofmodels,andthespecificationofverificationconditionsthatmustbemetinordertoconsidergivenrequirementstobesatisfied.OntheotherhandSVMsupportsthemanagementofanexistingsetofmodelsforasystembyorganizingthemintoacommonsystemarchitecture,bykeepingarecordoftheverificationactivitiesthatareroutinelyperformedonmodelsthroughmodelanalysis,simulationruns,andmodelexecution,andbyautomatingthebookkeepingoftheverificationresults.

ThissectiondescribesSVMfeaturesfordefiningverificationactivitiesandformanagingtheirexecutionandresults.Section2.1describestherepresenta-tionofSVMrequirementsandhowrequirementsareenteredandassociatedwithmodelsandverificationactivities.Section2.2describeshowmodelsarerepre-sentedinSVMandtherelationshipsbetweenSVMmodelobjectsandtheactualmodelsinthe“native”toolenvironments.Italsodescribestherepresentationofthesystemarchitectureandtheconceptofmodelvariantswherebymultiplemodelscanbeassociatedwithcomponentsofthesystemarchitecturetoreflecttheevolutionofthesystemdevelopmentprocess,andhowconsistencybetweenmodelsandthearchitectureischeckedandmaintained.Section2.3presentstheconceptsofverificationmethodsandverificationactivities,anddescribeshowtheyaredefinedinSVMtobeassociatedwithparticularmodelsandrequire-ments.Section2.4describeshowSVMprovidesaccesstoverificationresultsandpropagatesthestatusofresultsthroughtherequirementshierarchy.2.1

RequirementsTraceability

SVMsupportsrequirements-drivenverification.Allverificationactivitiesareas-sociatedwithandinitiatedfromaspecificrequirementinarequirementtreethatisdisplayedandmanagedthroughaninteractivewindow.Therequirementsview,showninFig.1,includesthenameanddescriptionoftherequirement,alongwiththestatusofitsverification.

Requirementsareentered,viewedandmanagedinahierarchicaltreestruc-ture.Thisallowsthecascadingofrequirementsintomultiplesub-requirements,whichinturncanbefurtherpartitionedintomanageablesub-sub-requiremententities.Atypicalsafetycriticaldesignprocessinvolvessuccessivecyclesofrefin-ingrequirementsfromonelevelofabstractionintomoredetailedrequirementsatalowerlevelofabstraction.Theseprocessesarenaturallyrepresentedwith

Fig.1.SVMrequirementsviewforanembeddedcontrolapplication(seeSect.3)

arequirementshierarchy.[6].Sucharequirementtreecanbeenteredmanuallyorimportedfromanexistingrequirementsdocument.Currently,thesetofre-quirements(andallassociatedsub-requirements)beneathagivennodeintherequirementtreeinaprojectcanbeimportedfrom(andexportedto)aspread-sheetinExcelformat.Arequirementisverifiedeitherbyexecutinganydirectlyassociatedverificationactivitiesand/orbyverifyinganysub-requirements.Theverificationactivityforarequirementischosenfromthelistofregisteredver-ificationmethodsandisinstantiatedwithspecificvaluesforitsinputs.Thisoperationcreatesanassociationbetweentherequirementanditsverificationac-tivities.Typically,toverifyarequirement,atestisexecutedontheworkproductandtheresultsofthetestareanalyzedtoinferiftheverificationcriteriahavebeensatisfied.SVMallowstheusertoimporttheworkproductasasystemmodel(orasanelementwithinthesystemmodel)andthenallowstheusertopickthissystemmodelduringverificationactivitydefinition.SVMstoresandkeepstrackofsuchrelationshipstoadvisetheusertore-verifyrequirementswhenworkproductsarechanged.

Asisfrequentlypracticed,thepartitioning(orcascading)ofrequirementsintosub-requirementsgenerallyfollowsthepartitioningofthesystemintosub-systemsandcomponents.SVMallowsuserstoassociaterequirementsandsub-requirementswithnodesinthesystemarchitecture.Thisrelationshipcanbeusedtoguidetheuserinthesystemdevelopmentandverificationprocess.Aftertheverificationactivitiesaredefined,theusercaninvokeverificationatanyre-quirementnodefromthecontextmenuintherequirementsview.WhentheuserrequestsverificationonaparticularrequirementinSVM,thetooltriestoverifyallthesub-requirements(includingallnestedlevels)andtheninfersthatthere-quirementhaspassedverificationonlyifallofitssub-requirementshavepassed.Theverificationstatusistrackedanddisplayedintherequirementsviewandthisstatuscanbeoneofthefollowing-passed,failed,inprogress,TBD(ToBeDecided)orinspect.Theinspectstatusflagsverificationactivitieswhoseresultsmustbemanuallyinspectedtodetermineiftheypassed.Thisstatuscanalso

beusedwhentheverificationactivityabortsduetoanerrorintheverificationscript.

SVMmaintainsassociationsbetweendifferentobjects,suchasrequirements,verificationactivities,systemmodelsandsystemarchitecture.Theseassocia-tionsarevisuallyindicatedwithwindowsynchronizationandpropagatechangestorequirementsthatneedre-verification.WhentheSVMwindows(views)aresynchronizedandanode(orobject)isselectedinoneoftheviews,theasso-ciatedentitiesinotherwindowsgethighlighted.ChangepropagationenablesSVMtoadvisetheusertore-verifyarequirementwheneveritoroneofitsverificationactivitiesisupdatedoraddedorsub-requirementisadded.Insuchinstances,thestatusontheaffectedrequirementandallofitsancestorsarere-settoTBD.Similarly,ifthemodelsintheirnativetooldomainsarechanged,SVMassociatesthesechangestoaffectedsystemmodelsandultimatelytotherequirementswhichusethesemodelsforverification.Sincemodelsareusuallyassembledusingreusablelibrarycomponents,thisprovidesapowerfulmecha-nismtotracetheimpactofchangesatacomponentlevel(model)toverificationofrequirementsatthesystemlevel.2.2

ModelManagement

Embeddedsystemsaretypicallydesignedtoreflectasystemarchitecturethatidentifiesthefunctionalcomponentsinthesystem.Thearchitecturebecomesthereferenceforidentifyingtherolesofvariousmodelsdevelopedduringthedesignprocess.Similarly,systemrequirements,bothfunctionalandpara-functional,suchasresponsetime,latency,andtoleranceofincompleteandinaccuratedatastreams,aretypicallyexpressedintermsofthesystemanditssubsystems.Duringthedevelopmentadditionalclaimsandobservationsoffunctionalandpara-functionalsystempropertiesmaybemade.ThismakesthearchitecturealsoareferencepointfortherequirementsandclaimshierarchyasdiscussedinSect.2.1.Finally,requirementsandclaimsarevalidatedthroughverificationactivitiesthatareassociatedwithrequirementsandclaims(seesection4).Thoseverifi-cationactivitiesareappliedtomodelsthatrepresentthesystemorsubsystem,whoserequirementistobevalidated.Thus,thesystemarchitectureprovidesabridgebetweentheverificationofrequirementsandthemodelsusedintheverification-asshowninFig.2.

SVMprovidestwoviewsofthesystemarchitecture,atreeview,andablockdiagramview,bothshowninFig.3.Thetreeviewreflectsthecompositionalhierarchyofthesystem.Thegraphicalviewreflectstheinteractionsbetweensystemcomponents,typicallyrepresentedbyportsandconnections.

Wehaveenhancedthebasicsystemarchitecturedescriptionwithsemanticinformationabouttheapplicationdomaininordertosupportconsistencyanal-ysisofsystempropertiesthatotherwiseareundocumentedandresultinhiddensideeffects.Examplesofcommonproblemsaremistakingwheelspeedforcarspeed,usingmetersinsteadoffeet,orusinganabsolutecoordinatesystemin-steadofarelativeone.Figure4illustrateshowSVMidentifiesthesemismatchesinthesystemarchitecture.Semanticinformationcanalsoincludeboundson

Fig.2.SVMsystemarchitectureasreferencepoint

Fig.3.Treeandblockdiagramviewofthesystemarchitecture

valuesandratesofchangessuchasaconstraintonastreamofsetpoints,whosechangeinsuccessivedatavaluesisexpectedtostaywithinboundsacceptabletothereceivingcontroller.Systemarchitecturesdecoratedwithsuchadditionalinformationcanbecheckedforsemanticconsistencyearlyinthedevelopmentlifecycle.

Suchamodel-basedapproachtoarchitecturemodellingandanalysisispro-motedbytheModel-DrivenArchitectureinitiativeoftheObjectManagementGroup(OMG)[1]andisincorporatedintheSocietyofAutomotiveEngineers(SAE)ArchitectureAnalysis&DesignLanguage(AADL)standardforembed-dedreal-timesystemscurrentlyinballot[3].Thisstandardistargetedfortheavionics,aerospace,andautomotiveindustries.SVMmaintainsanabstractionofsuchmodelswithinformationthatisrelevanttotheverificationofsystem

Fig.4.Semanticinconsistencyinthesystemarchitecture

requirements.Theabstractionoftheseexternalmodelsrepresentsthemodelledsystemstructureandtheinteractionbetweenitssubsystems.Thisinformationisautomaticallyextractedfromtheexternalmodels.

Allmodelsandtheircomponentsrelatebacktothesystemarchitecturethatdefinesacommonhierarchyandinteractiontopology.SVMprovidesoperationsforderivingthesystemarchitecturefromasinglemodelorfromacollectionofmodels.Similarly,itprovidesoperationsforcomparingamodelagainstitsarchi-tecture,andforidentifyingdifferencesinthestructureandinteractiontopologybetweenmodels.Justasthesystemarchitecturecanbesemanticallyenriched,themodelabstractionmaintainedbySVMcanbedecoratedwithdomain-specificinformation.Semanticconsistencyisverifiedbetweenabstractedmodelsandthesystemarchitecture,withinthesystemarchitecture,andbetweentheabstractedmodelandtheactualexternalmodel.Theconceptofmodelabstractionandstaticcheckinghasbeenexploredpreviouslybythesoftwareengineeringcom-munity[2].Iftheexternalmodellingnotationdoesnotsupportthepresentationofsuchinformation,SVMprovidesthiscapabilityasanextensiontotheexter-naltool.Forexample,thecurrentreleaseofMathWorksSimulinkhasalimiteddatadictionarycapabilityfocusingontheconsistentuseofimplementationtypessuchasshortandlongintegers,etc.SVMextendsthesemodelswithinformationrelatedtotheapplicationdomain.2.3

VerificationActivities

TheverificationactivitiesassociatedwithSVMrequirementsaredefinedintwosteps.First,verificationmethods(VMs),definedbyMATLAB󰀁m-code,areregisteredwithunboundvariables.RegisteredVMsaretheninvokedandin-stantiatedasverificationactivities(VAs)bybindingtheVMvariablestothemodelsandsignalsassociatedwithaparticularrequirement.

Fig.5.Verificationmethodregistrationinterface.

Figure5showstheVMregistrationuserinterface,whichhasthreepanestodefinethevariablesintheVM(showninFig.5),theVMcodetobeexe-cuted,andthefunctionsforreviewingresultsfromtheVM(alsom-code).VMcodecaninvokeanymodelsandtoolsthroughthestandardMATLAB󰀁pro-grammingconstructs.Verificationparameters(unboundvariables)areassignednames,types,anddescriptionstoassisttheuserwhentheVMisinstantiatedasamethod.Severalpre-registeredVMsareavailablewithSVM,including:stepresponseanalysis;comparativemodelsimulation;discretemodelchecking(SMV);hybridmodelchecking(Checkmate);Dymolasimulation;batchsimu-lationondatasets;andmexcompile.UserscanaddadditionalVMs.VMsareinstantiatedasVAsfromtherequirementswindow,asshowninFig.6.TheuserselectsoneoftheregisteredVMstobeappliedfortherequirementandbindsthevariablesthatidentifythemodels,signalsanddatatobeusedfortheVA.2.4

ResultsManagement

SVMautomaticallymanagestherecordkeepingoftheexecutionofverificationactivitiesandtheirresults.Itdoessointhreeways:itmaintainstheresultstatus,itarchivestheresultsforlaterexamination,anditmanagestheimpactofchangesinmodelsandverificationmethodsbyinvalidatingpreviousverificationresultsthatarepotentiallyaffectedbythechanges.

Averificationactivityisinoneofseveralstates.Itmayneedtobeexecuted,itsexecutionmaybeinprogress,itmayhavecompletedbypassingorfailing,oritmayrequireexaminationtodeterminewhetheritissatisfied.SVMallowsverificationactivitiesofindividualrequirementstobeorganizedintoverifica-tionfolders.Thosefolderscanrepresentdifferentlifecyclephases,andcontainsdifferentlogicexpressionstoindicatetheconditionsunderwhichthecontainedsetofverificationactivitiesandfoldersisconsideredsatisfied.Thisverification

Fig.6.Definingaverificationactivityforarequirement.

resultstatusisnotonlypropagateduptheverificationfolderhierarchy,butalsouptherequirementshierarchy.Suchaccumulationofverificationresultstatusprovidesasimplevisualcueastothedegreetowhichrequirementsofasystemarebeingsatisfiedaswellasaquantificationofsuchpass/failcoverage.

Averificationactivitythattakestheformofmodelcheckingmayproducecounterexampleswhenthemodelcheckingconditionisnotsatisfied.Asimu-lationrunmayproducelogsofproducedoutput,tracesofstatechangesetc.Similarly,probesintheexecutingcodeofasystemmayproduceatrailofitsexecution.Thisinformationmaybeevaluatedduringtheexecutionofthever-ificationactivitytodeterminetheresultsstatus.SVMkeepstrackofsuchin-formationthatisproducedbyexternaltools.Itusesthefilesystemtoidentifyandarchiveresultsrelatedtoaparticularverificationmethod.Beforeexecut-ingaverificationmethodthetoolcreatesanewresultsdirectoryandmakesittheworkingMATLAB󰀁directory.Thisallowsverificationmethodstoproducecommonoutputfileswithoutconflictingwiththeresultsofotherverificationmethods.SVMuserscanlaterexaminetheseresultsthroughmanualinspectiontoreviewtheautomatedevaluationoftheverificationconditionandtodrawadditionalconclusions.

SVMnotonlyautomatestherecordingofverificationresults,butitalsocanautomatetheidentificationandautomaticexecutionofverificationactivitiesthathaveyettobeexecuted.Furthermore,SVMcanmanagetheimpactofchangesmadetomodels,librarycomponentsofmodels,toconfigurationsofmodels,toverificationmethods,toparametersanddatasetsthatareinputtotheverificationactivity.

SVMtrackschangestoexternalmodelsanddatafilesintwoways.First,ittrackssuchchangesiftheyareinitiatedthroughSVMbytheuseropeningamodelordatafilethroughSVMandmakingmodifications.Second,changesmadethroughanexternaltoolwithouttheinvolvementofSVMareidentifiedbytrackingmechanismssuchasrecordingmodificationdatesoffilesorchecksumsoffilecontentsandcomparingthemtotheactualfilesatstartupofSVMorat

userrequest.SVMalsosupportschangeimpactmanagementbyincorporatingideasexploredinpreviousresearchonthistopic[9,7,4].SinceSVMhasarecordofrelevantdependenciesitcaninvalidatetheresultstatusofanypreviouslycom-pletedverificationactivitywhoseresultispotentiallyimpactedbythechange.SVMunderusercontrolautomaticallyre-executestheseverificationactivitiestodeterminewhethertherequirementsarestillsatisfied.ThesamedependencyinformationcanbeusedbySVMtoprovidewhat-ifimpactanalysis,i.e.,topredicttheamountofreverificationnecessaryasaresultofachangebeforethechangeismade.

3AnEmbeddedControlApplication

ThissectiondealswithanapplicationfromtheDARPAprojectModelBasedIntegrationofEmbeddedSoftware(MoBIES).Thisprojectproposedtwoauto-motivecasestudies,oneofthemisanElectronicThrottleControl(ETC)system.TheETCsystemisacomponentthatreplacesthemechanicallinkbetweenthepedalandthethrottleplateinanautomobile.

ProblemStatementTheETCsystemwaspartofanOpenExperimentalPlat-form(OEP).TheOEPwasusedtoillustratethemodelbasedapproachtoproduceembeddedcode.Inthissectionwewillfocusonthemodellingphase,andillustratetheuseofmultiplemodelsandverificationfolders.

Applicationof(SVM)SystemVerificationManagerFigure1depictsthere-quirementstreefortheETCsystem.ThefirstsetofrequirementswaspartoftheinformaldescriptionoftheETCsystem.ThisdescriptionwasprovidedbytheOEPalongwithaSimulinkandStateflowmodel.Amongtherequirementswererisetime,settletimeandovershootrequirements.Theserequirementsweredefinedforasingleexecutionofthesystemwithstepinput.Satisfactionoftherequirementcantypicallybetestedbysingle(orfinitelymany)runsofthesimu-lationmodel.Forthisexamplewefindthattherisetimerequirementissatisfied,whereasthesteadystateerrorrequirementisviolated.

ThesecondsetofrequirementsdealwithasimplifiedversionoftheOEPmodel.AlthoughtheETCsystemisessentiallyjustaDCmotorandaspring,controlledbyaslidingmodecontroller,andalinearfilterfortheinput,theOEPmodelcontainmoredetails.Thismainly,becauseitservedatthesametimeasblueprintforanimplementation.Fortheverificationwemodeltheplant,theslidingmodelcontrollerandthefilter,butweomitforexampledetailsfromactuatorandsensors.Thismodelisapiecewiselineartime-invariant7th-ordersystem.

ToformallyverifyrequirementsoftheETCsystemforasetofinitialstates,reachabilityanalysisisperformedonthe7th-ordermodelusingproceduresfromRRT(ReachabilityanalysisinReducedstatespaceToolbox)[5].Complexityofreachabilitycomputationsforcontinuousandhybriddynamicsystemstypi-callygrowsdramaticallywiththedimensionofthecontinuousstatespace.To

Fig.7.Theverificationfolderscanbeusedtogroupverificationactivities.

avoidperformingreachabilityanalysisinthefull-orderstatespace,thetoolRRTcomputesanover-approximationofthesetreachablestatesusingreduced-ordermodels.TheproceduresinRRTfirstconstructareduced-ordermodelusingthebalanceandtruncation(B&T)[8]method.Itthenestimatestheupper-boundontheapproximationerrorintroducedbymodelreduction.Finally,conservativeover-approximationsofthereachablestatesarecomputed,whichincorporatetheerrorbounds.

Thereducedorderreachabilityanalysisprovidesefficientanalysisattheex-penseofbiggerover-approximationerrors.Adrasticreductionoftheordermightmayleadtoalargeapproximationerror,andthustoinconclusiveresults.Ontheotherhand,iftheprocedurefindsthatthereducedordermodelsatisfiestherequirement,weknowthatthefullordermodelsatisfiestherequirement.Wedefinemultipleverificationactivitieswithdifferentchoicesofreducedorders.Ifanyoftheseverificationactivitiesfindsthatthepropertyissatisfied,weknowthattheoverallrequirementissatisfied.TheverificationfolderReducedordercontainsallverificationactivities.ToreflectthatonlyoneoftheseactivitieshastoreturnPASS,weselecttheoptionORfromthecontextmenuSetVerificationLogic(Fig.7).

FutureWorkThecurrentimplementationSVMevaluatesallverificationactivi-ties.Ifaverificationfoldercontainsmultipleactivities,ofwhichonlyonehastopass,theSVMcouldstopassoonasoneactivitypasses.ThestatusofthefolderwillbePASSEDregardlessoftheoutcomeoftheremainingactivities.Similarly,ifallactivitieshavetopass,theevaluationmightstopassoonasoneactivityfails.AfuturereleaseoftheSVMshouldgivetheusertheoptiontoeithereval-uateallactivitiesregardlessoftheresult,ortostopevaluationassoonasthestatusofthefoldercanbedetermined.

Fig.8.SignalClassifier:ApplicationLevel.

4ASignalProcessingApplication

InthissectionweconsidertheapplicationofSVMtoasignalclassificationdevelopmentproject.ThegoalofthisprojectistoproduceefficientembeddablecodestartingfromaprototypedesignimplementedinMATLAB󰀁usingthebuilt-inlanguageandsignalprocessingfunctions.WeneedtoensurethatthefinalimplementationisabletogenerateembeddablecodeandisfunctionallyequivalenttotheprototypeMATLAB󰀁Mcodewithinanacceptabletolerance.SVMisusedtopreciselyidentifydiscrepanciesbetweentheimplementationsandtotracethesetospecificcomponentsinthedesign.

ProblemStatementThisapplicationclassifiesincomingsignalasPhaseShiftKeyed(PSK),FrequencyShiftKeyed(FSK),ornoneoftheabove(NOTA)basedonsignalfeaturessuchasbandwidth,symbolrate,kurtosis,numberofspectraltones,andnumberofphasestates.Themodel-basedimplementationisdoneinSimulinkandStateflowsothatembeddableC-codecanbeautomaticallygeneratedusingReal-TimeWorkshop.

DesignTheSimulinkmodelisarrangedinanapplication,component,andprim-itiveblockhierarchy.Thisarrangementiswellsuitedtoamodelbasedimple-mentationbecauseitclearlyillustratesthecontrolanddataflow.Figure8showsthetoplevelSimulinkdiagram.Theapplicationiscomposedoffivefeatureex-tractorcomponentsthatprocessesinputsignalstoproducesignalcharacteristicsthatareusedtodeterminesignalmodulation.Thesecomponentsarebuiltwithprimitiveblocks,eachofwhichperformsaspecificsignaloperation.

TheunderlyingimplementationoftheprimitiveblocksleveragesthesignalprocessingcapabilitiesofSimulinkandtheSignalProcessingBlocksetexten-sionproduct.Insomecasestheprimitiveblockfunctionrequiressomecustomcapabilitybeyondthebuilt-inlibraryofsignalprocessingcomponents.State-flowisusedinmanyofthesecasestoincorporatearbitrarystructuredcontrolflowsuchaswhileloopsandnestedif-thenelseconstructs.Figure9showstwo

Fig.9.SignalClassifier:ComponentLevel.

Fig.10.VerificationMethodusetocompareSimulinkimplementationagainstrefer-enceM-codeimplementation.

blockimplementations:OBFFTthatsimplyencapsulatesthebuilt-inFFT,andOBBWest,thebandwidthestimator,thatisaStateflowchart.

Applicationof(SVM)SystemVerificationManagerVerifyingtheSimulinkmodelimplementationagainstthereferenceMATLAB󰀁implementationcanbete-dious,consideringthenumberofcomponentsthatmustbeindividuallyverified.SVMhelpstheuserorganizesrequirements,verificationactivitiesandresultsallinonecentralpoint.

ToverifytheSimulinkcomponentimplementations,weneedtestinputsandoutput.WedevisedasystemshowninFig.10tocapturetheseoutputsasasideeffectofexecutingtheoverallprototypesignalclassificationapplication.ThereferenceinputsdrivetheSimulinkblockstogivetestoutputsthatare

Fig.11.Associatingverificationmethodforeachblock.

Fig.12.VerificationResults.

comparedagainstthereferenceM-functionsblockstodetermineiftheresultsmeetaspecifiedtolerance.

ThisverificationmethodisimplementedasanMfunctionregisteredwithinSVM.RegisteringagenericoperationsuchasthisenablesustoinstantiateandparameterizethefunctionfromwithintheSVMuserinterface.AsshowninFig.11eachprimitiveandcomponentblockhasaninstantiationofthemethodwithitsownsetifparametervalues.

Aftereachverificationactivity,theresultsareautomaticallyorganizedinaseparatefolderbySVMandcanbeeasilyaccessedwithintheSVMenvironment.Forexample,theOBPSDprimitiveblock,whichcomputesthepowerspectrumdensity,followsthereferenceMATLAB󰀁implementationveryclosely.Theerrorisontheorderof10-14whichisclosetofloatingpointprecision(Fig12).

Verifyingablockagainstonesignaldoesnotguaranteethattherequirementswillbemetforanentirerangeofsignals.SVMprovidesaneasymethodtorepeat

Fig.13.Cloningverificationactivityforasetofinputsignals.

theverificationforasetofsignalsbycloningtheverificationactivity,asshowninFig.13.Bybreakingdowntheverificationstomanageablemodelprimitivecomponents,theusercannoweasilylocateandtroubleshootareaswithinamodelthatcausesittodeviatefromrequirements.Theverificationactivitiesareautomaticallyorganizedwithinaverificationfoldertoallowtheusertoeasilybrowsetheresults.

Oftentimes,anupdatetoaprimitiveblockwillhavesignificantramificationstootherpartofthemodel.SVMhastheabilitytoidentifythesedependenciesandappropriatelyresettheverificationstatus.IftheuserupdatesaprimitiveblockallverificationactivitiesthatdependsonthissystemmodelwillhavetheirverificationstatusresettoTBD(tobedetermined).

FutureWorkTheconceptofcloningaverificationactivityforasetofinputsignalsdoesnotensureeverypartofamodelistested.AspartoftheSimulinkPerformanceToolspackagethereisatoolcalledModelCoverage,whichrecordsallsimulationpathsandgeneratesareportindicatinguntestedportionsofamodelforagivensetofinputsignals.TheSVMverificationmethodwillbeenhancedtoleveragethiscapabilitytogivetheuseradditionalverificationin-formationtoensurethemodelwillmeettheirspecifiedrequirements.

5Discussion

ThispaperdescribesthefeaturesofthecurrentbetaversionofSVM(availableathttp://www.ece.cmu.edu/∼webk/svm).SVMhasbeenappliedtoseveralexam-plesintheDARPAMoBIESprogram,includingtheelectronicthrottlecontrol(ETC)andasoftwareradiodigitalsignalprocessingsystem,describedinthispaper.Currentdevelopmentisfocusingonenhancingthedevelopmentenviron-mentfordefiningverificationmethodsandverificationactivities.

WearealsoinvestigatingmethodsforincreasingthecapabilityofSVMtosupportheterogeneousverificationactivities,bywhichwemeantheapplicationofmultipleformalismsandtoolstoacquireinformationaboutthedesignandsystemperformance.Thecurrentmechanismsforcombiningverificationstatusinformationintherequirementstreeareafirststepinthisdirection.Require-mentscanbesatisfiedusingawiderangeofverificationmethods,includingsim-ulation,modelchecking,theoremproving,anddesignerevaluationofempiricalresults.WeaimtoincreasethepowerofSVMbyintroducingricherrepresenta-tionsoftherelationshipsamongmodelsandverificationactivitiessothatfurtherinferencescouldbeobtainedautomatically.Towardsthatend,wearedevelop-inganontologyforhybridsystemverificationthatwillsupportcombiningandreasoningaboutinformationfromheterogeneousverificationactivities.

References

1.OMGmodeldrivenarchitecture.http://www.omg.org/mda.

2.E.M.Clarke,O.Grumberg,andD.E.Long.Modelcheckingandabstraction.InNineteenthAnnualACMSymposiumonPrinciplesofProgrammingLanguages,1992.

3.P.Feiler,B.Lewis,andS.Vestal.TheSAEArchitectureAnalysis&DesignLan-guage(AADL)Standard:Abasisformodel-basedarchitecture-drivenembeddedsystemsengineering.InIFIPWorldComputerCongress-WorkshoponArchitec-tureDescriptionLanguages(WADL04),2004.

4.P.H.FeilerandJunLi.Managinginconsistencyinreconfigurablesystems.InIEEProceedingsSoftware,pages172–179,1998.

5.Z.HanandB.H.Krogh.Usingreduced-ordermodelsinreachabilityanalysisofhybridsystems.InIEEEProcofAmericanControlConference,2004,toappear.6.L.A.Johnson.Softwareconsiderationsinairbornesystemsandequipmentcertifi-cation.Technicalreport,RTCAInc.,1992.DocumentRTCA/DO-178B.

7.JunLiandP.H.Feiler.Impactanalysisinreal-timecontrolsystems.InProceedingsofInternationalConferenceonSoftwareMaintenance(ICSM),pages443–452.IEEECSPress,1999.

8.B.C.Moore.Principalcomponentanalysisinlinearsystems:Controllability,ob-servabilityandmodelreduction.IEEETransactiononAutomaticControl,26(1),Feb1981.

9.D.E.Perry.ThelogicofpropagationintheInscapeEnvironment.InACMSIG-SOFT’ThirdSymposiumonSoftwareTesting,AnalysisandVerification,pages114–21,19.