Mixed controldata-flow representation for modellin

MIXEDCONTROL/DATA-FLOWREPRESENTATIONFORMODELLINGANDVERIFICATIONOFEMBEDDEDSYSTEMSByMauricioVareaDepartmentofElectronicsandComputerScience,UniversityofSouthampton,UnitedKingdom.March2002UNIVERSITYOFSOUTHAMPTONABSTRACTFACULTYOFENGINEERINGELECTRONICSANDCOMPUTERSCIENCEDEPARTMENTMPhil/PhDTransferReportMixedControl/Data-FlowRepresentationforModellingandVerificationofEmbeddedSystemsbyMauricioVareaEmbeddedsystemdesignissuesbecomecriticalasimplementationtechnologiesevolve.Theinteractionbetweenthecontrolanddataflowofanembeddedsystemspecificationisanimportantconsiderationand,inordertocopewiththisaspect,anewinternaldesignrepresentationcalledDualFlowNet(DFN)isintroducedandfurtheranalysedinthisthesis.Oneofthekeyfeaturesofthisinternalrepresentationisitstightcontrolanddataflowinteraction,whichisachievedbymeansoftwonewconcepts.Firstly,thestructureofthenewDFNmodelisformulatedemployingatripartitegraphasbasis,whichturnsouttobeadvantageousformodellingheterogeneoussystems.Secondly,acomplexdomainmarkingschemeisusedtodescribethebehaviourofthesystem,leadingtobetterresultsintermsofmodellingthedynamicsoftheembeddedsystemspecification.Structuraldefinitions,behaviouralrulesandgraphicalrepresentationofthenewDFNmodelispresentedinthiswork.BesidesthepotentialapplicationoftheproposedDFNmodelintherealmofem-beddedsystem’sinternaldesignrepresentation,thisthesisalsoaddressestheverificationofDFNmodelsthroughformalmethods.Behaviouralpropertiesofembeddedsystems,suchasreachability,safetyandlivenessareexpressedeitherinComputationTreeLogic(CTL)orinLinearTemporalLogic(LTL)formulae,andthenverifiedusingstate-of-the-arttools.ThisthesisalsoaddressestheimplementationofanefficientlibrarywhichundertakesthemodelcheckingprobleminDFNmodels.iExamplesofvaryingcomplexityarepresentedinordertoillustratethefeasibilityandvalidityoftheDFNmodel.Theseexamplesrangefromsimplesystemsusedtoun-derstandtheunderlyingsemanticsofthemodel,uptocomplexarrangementsmodellingreal-lifeembeddedsystems.Furthermore,anumberofrelevantandchallengingareasbasedontheDFNmodel(anditsverificationmethodology),areoutlinedasfuturework.iiContentsListofSymbolsviiChapter1Introduction11.1EmbeddedSystemsDesign.........................11.1.1Modelling..............................31.1.2Validation..............................41.1.3Synthesis..............................61.2MotivationandContributions........................71.3ThesisOrganisation.............................8Chapter2BackgroundandRelatedWork92.1EmbeddedSystemModellingTechniques.................92.1.1MCDmodels............................102.1.2MDCmodels............................112.1.3M¯Bmodels.............................122.2FormalVerificationofEmbeddedSystemmodels.............122.2.1TemporalLogics..........................132.2.2ModelChecking..........................132.2.3Automata-TheoreticAproaches..................142.3ConcludingRemarks............................14Chapter3NewInternalDesignRepresentation:DualFlowNets163.1DFNstructuralmodel............................173.1.1Structuralmodelexample.....................193.2Anewconceptinmarkingfunctions....................203.3DFNbehaviouralmodel..........................233.3.1Behaviouralmodelexample....................253.4ExamplesofApplication..........................263.4.1EmbeddedMultiplier........................26iiiChapter4FormalVerificationoftheDFNmodel304.1AlgorithmsforModelCheckingDFNmodels...............304.2ImplementationandResults........................344.3VME-buscontroller.............................35Chapter5Conclusions385.1FutureWork.................................38AppendixAComplexNumbers40Bibliography41ivListofFigures1.1TypicalEmbeddedSystemDesignFlow..................21.2RelationshipamongValidationMethods..................51.3ImpactofDesignonSystemImplementationCost[100].........83.1TheDFNphilosophy............................173.2DFNverticesinteractioninbothcontrolanddatadomain..........183.3AsimpleDFNmodel............................203.4Statespacemappedintothecomplexplane................233.5BehaviouralanalysisofaDFNmodel...................263.6EmbeddedMultiplier............................273.7Multiplieralgorithm.............................273.8DFNmodelofmultiplier..........................284.1OurModelCheckingMethodology.....................314.2Nondeterministicscheduler.........................314.3Placedefinition:datatype.........................324.4AlgorithmforaDFNControlTransition..................324.5AlgorithmforaDFNHull.........................334.6AlgorithmforaDFNGuardFunction...................344.7VerificationtimedependingonthecapacityKandthelengthL......354.8VMEbuscontroller.............................36vListofTables2.1TemporalOperators.............................13viListofSymbols=)implies()ifandonlyif2setmembership[setunion\setintersection?emptyset^logicaland_logicalor8forall9thereexistsC=setofcomplexnumbersiimaginaryunit,i.e.p1ℜ(ς)realpartofς2C=ℑ(ς)imaginarypartofς2C=jςjmodulusofς2C=\ςphaseofς2C=xpre-setofxoverthecontroldomainxpre-setofxoverthedatadomainx