AFRAMEWORKFORVERIFICATIONOFTRANSACTIONLEVELMODELSINSYSTEMCByRezaHajisheykhiADISSERTATIONSubmittedtoMichiganStateUniversityinpartialoftherequirementsforthedegreeofComputerScience-DoctorofPhilosophy2016ABSTRACTAFRAMEWORKFORVERIFICATIONOFTRANSACTIONLEVELMODELSINSYSTEMCByRezaHajisheykhiDuetotheirincreasingcomplexity,today'sSoC(SystemonChip)systemsaresubjecttoavarietyoffaults(e.g.,single-eventupset,componentcrash,etc.),therebytheirvahighly importanttaskofsuchsystems.However,visacomplextaskinpartduetothelarge scaleofintegrationofSoCsystemsanddifferentlevelsofabstractionprovidedbymodernsystem designlanguagessuchasSystemC.TofacilitatethevofSoCsystems,thisdissertationproposesanapproachforveri-fyinginter-componentcommunicationprotocolsinSystemCTransactionLevelModeling(TLM) programs.SystemCisawidelyacceptedlanguageandanIEEEstandard.ItincludesaC++library ofabstractionsandarun-timekernelthatsimulatesthesystem,therebyenablingtheearly developmentofembeddedsoftwareforthesystemthatisbeingdesigned.Toenableandfacilitate thecommunicationofdifferentcomponentsinSystemC,theOpenSystemCInitiative(OSCI)has proposedaninteroperabilitylayer(ontopofSystemC)thatenablestransaction-basedinteractions betweenthecomponentsofasystem,calledTransactionLevelModeling(TLM).InordertoverifySystemCTLMprograms,weproposeamethodthatincludesvemainsteps,namelyformalsemantics,modelextraction,faultmodeling,modelslicing,andmodelchecking.InordertoextractaformalmodelfromthegivenSystemCTLMprogram,weneedtospecifytherequirementsofdevelopingaformalsemanticsthatcancapturetheSystemCTLM programswhilestillfromautomationtechniquesforvand/orsynthesis.Based onthisintuition,weutilizetwomodelextractionapproachesthatconsiderthearchitectureofthegivenprogramtoo.Intheapproach,weproposeasetoftransformationrulesthathelpsus toextractaPromelamodelfromtheSystemCTLMprogram.Inthesecondapproach,wediscuss howtoextractatimedautomatamodelfromthegivenprogram.Whenwehavetheformalmodel,wemodelandinjectseveraltypesoffaultsintotheformalmodelsextractedfromtheSystemCTLMprograms.Forinjectingfaults,wehavedevelopeda tool,calledUFIT,thattakesaformalmodelandadesirablefaulttype,andinjectsthefaultsintothemodelaccordingly.ThemodelsextractedfromtheSystemCTLMprogramareusuallyverycomplex.Addition-ally,whenweinjectfaultsintothesemodelstheybecomeevenmorecomplex.Hence,weutilize amodelslicingtechniquetoslicethemodelsinthepresenceorabsenceoffaults.Wehavedevel- opedatool,calledUSlicerthattakesaformalmodelalongwithasetofpropertiesthatneedstobevandgenerateaslicedmodelbasedonthegivenproperties.Theresultsshowthatv tiontimeandthememoryusageoftheslicedversionofthemodelissmallerthanthat oftheoriginalmodel.Subsequently,insomecaseswherethevoftheoriginalformal modelsisnotevenpossible,usingourmodelslicingtechniquemakesthevpossibleina reasonabletimeandspace.WedemonstratetheproposedapproachusingseveralSystemCtransactionlevelcasestudies.Ineachcasestudy,weexplaineachstepofourapproachindetailanddiscusstheresultsand improvementsineachofthem.Copyrightby REZAHAJISHEYKHI 2016Tomyparents,MastanehandDariush.vACKNOWLEDGMENTSFirstandforemost,Ifeelindebtedtomyadvisor,ProfessorSandeepKulkarni,forhisguid-ance,encouragement,andinspiringsupervisionthroughoutthecourseofthisresearchwork.His patience,extensiveknowledge,andcreativethinkinghavebeenthesourceofinspirationforme. HewasavailableforadviceoracademichelpwheneverIneededandgentlyguidedmefordeeper understanding,nomatterhowlateorinconvenientthetimeis.ItishardtoexpresshowthankfulI amforhisunwaveringsupportoverthelastyears.IwouldliketotakeonthisopportunitytothankmydissertationcommitteemembersDr.Abdol-HosseinEsfahanian,Dr.GuoliangXing,andDr.SubirBiswaswhohaveaccommodatedmytiming constraintsdespitetheirfullschedules,andprovidedmewithpreciousfeedbackonmydissertation presentation.Also,duringmyPh.D.studies,IhadthepleasureofcollaboratingwithDr.Ali Ebnenasir.Hisvaluablecommentshelpedmealottotherightroadmapinmyresearch.Ialso wouldliketothankDr.LivinginEastLansingwithoutmygoodfriendswouldnothavebeeneasy.Iwanttothankallmyfriendsinthedepartmentandoutsidethedepartment.IwishIcouldnameyouall.Lastbutnotleast,Iwanttoexpressmydeepestgratitudetomybelovedparentsandmydearestsister.Theirloveandunwaveringsupporthavebeencrucialtomysuccess,anda constantsourceofcomfortandcounsel.Specialthankstomyparentsforabidingbymyabsence inlastveyears.viTABLEOFCONTENTSLISTOFTABLES.......................................xiLISTOFFIGURES......................................xiiLISTOFALGORITHMS...................................xivChapter1Introduction..................................11.1Motivation.......................................1 1.2ObjectivesandProposedFramework.........................3 1.3ThesisOverview....................................5 1.4BibliographicNotes..................................6Chapter2Preliminaries.................................72.1SystemC........................................72.1.1StructuralModeling..............................9 2.1.2BehavioralModeling.............................102.1.2.1Processes..............................10 2.1.2.2Events...............................112.1.3SimulationKernelandScheduler.......................122.2TransactionLevelModeling.............................14 2.3UPPAALTimedAutomata..............................192.3.1TimedAutomata...............................20 2.3.2NetworksofTimedAutomata........................21 2.3.3SymbolicSemanticsofTimedAutomata...................22 2.3.4UPPAAL...................................222.3.4.1ModelingLanguage........................23 2.3.4.2QueryLanguage..........................24 2.3.4.3AnIllustrativeUPPAALExample.................252.4SPINandPromela...................................262.4.1ModelingLanguage..............................262.4.1.1Processes..............................27 2.4.1.2Variables..............................29 2.4.1.3Messagechannels.........................302.4.2ControlFlow.................................302.4.2.1Caseselection...........................31 2.4.2.2Repetition.............................312.4.3VwithSPIN............................322.5Summary.......................................32viiChapter3RelatedWork.................................333.1FormalizingtheSemantics..............................33 3.2CheckersforSystemCDesigns............................35 3.3StaticAnalysisandStatelessModelChecking....................36 3.4ModelExtractionandModelChecking........................37 3.5Summary.......................................38Chapter4FormalSemanticsandModelExtraction..................394.1DevelopingaFormalSemantics...........................39 4.2ExtractingtheFormalSemanticsfromtheSystemCTLMProgram.........41 4.3TransformationRulesforGeneratingPromelaModels................43 4.4CaseStudy1:ExtractingPromelaModel.......................454.4.1Capturingtheexecutionsemanticsofthesimulationkernel.........46 4.4.2PropertyandFunctionalCorrectness..............484.5CaseStudy2:ExtractingPromelaModelusingTransformationRules.......494.5.1PropertyandFunctionalCorrectness..............524.6TransformationRulesforGeneratingUPPAALTimedAutomata..........53 4.7CaseStudy3:ExtractingUPPAALModelusingTransformationRules.......564.7.1PropertyandFunctionalCorrectness..............594.8CaseStudy4:ExtractingUPPAALModelofaNoCSwitch.............604.8.1PropertyandFunctionalCorrectness..............624.9UsingSTATEforExtractingTimedAutomataModels................634.9.1Assumptions.................................64 4.9.2RepresentationofSystemCTLMDesignsinUPPAAL...........654.9.2.1TheScheduler...........................66 4.9.2.2Events...............................68 4.9.2.3Processes..............................70 4.9.2.4PayloadEventQueue(PEQ)....................714.10CaseStudy5:ExtractingUPPAALModelinATCodingStyle...........73 4.11Summary.......................................77Chapter5ModelingofFaults..............................785.1FaultCategories....................................79 5.2FaultModelingforPromelaModels.........................805.2.1CaseStudy1:FaultModelingandImpactAnalysisforTwoCommunicat-ingModules..................................805.2.2CaseStudy2:FaultModelingandImpactAnalysisforMemory-MappedBuses.....................................82 5.2.2.1PerturbingMemoryContents...................82 5.2.2.2ControlSignalFaults........................835.3FaultModelingforUPPAALTimedAutomataModels...............835.3.1GenericDescriptionofFaults.........................845.3.1.1Messageloss............................84 5.3.1.2Permanentfaults..........................84 5.3.1.3Transientfaults...........................85viii5.3.1.4TimingFaults............................855.3.2AutomaticFaultInjection...........................875.3.2.1AlgorithmDescription.......................885.4Summary.......................................91Chapter6TheToolUFIT:TheFaultInjectorToUPPAALTimedAutomata....926.1InputofUFIT.....................................926.1.1Therunningexample.............................926.2InternalFunctionality.................................936.2.1BriefdiscussionaboutmodelingoffaultsinUFIT..............95 6.2.2AnalysisofResults..............................976.3CaseStudiesonModelingFaultsforUPPAALTimedAutomataModels......986.3.1CaseStudy1:FaultModelingandImpactAnalysis.............996.3.1.1Analysisofthefault........................996.3.2CaseStudy2:FaultModelingandImpactAnalysis.............1006.3.2.1MessageFaults...........................101 6.3.2.2Modelingandanalyzingfail-stopfaultsinthecasestudy.....102 6.3.2.3ModelingandanalyzingByzantinefaultsinthecasestudy....102 6.3.2.4Modelingandanalyzingstuck-atfaultsinthecasestudy.....1036.3.3CaseStudy3:FaultModelingandImpactAnalysis.............1036.3.3.1MessageFaults...........................103 6.3.3.2PermanentFaults..........................104 6.3.3.3TransientFaults..........................105 6.3.3.4TimingFaults............................1066.4Summary.......................................106Chapter7ModelSlicingTimedAutomataModels...................1087.1ModelSlicing.....................................108 7.2TheRunningExample:TheAlternatingBitProtocol................109 7.3UPPAALTimedAutomataModelSlicing......................1127.3.1Identifyingthesetofrelevantlocationsandactions(LandA).......1127.3.2Buildingtheslicedmodel...........................1147.4ApplyingtheModelSlicingontheAlternatingBitProtocol.............115 7.5Summary.......................................116Chapter8USlicer:AToolforModelSlicingUPPAALTimedAutomataModels..1198.1InternalsofUSlicer..................................1198.1.1XMLformat..................................1208.2CaseStudy1:Producer-ConsumerProgram.....................1218.2.1Slicingintheabsenceoffaults........................122 8.2.2Slicinginthepresenceoffaults.......................1238.3CaseStudy2:Memory-MappedBuses........................1248.3.1Slicingintheabsenceoffaults........................125 8.3.2Slicinginthepresenceoffaults.......................1258.4Summary.......................................126ixChapter9ConclusionandFutureWork........................1299.1Aroadmapforfutureresearch.............................131BIBLIOGRAPHY.......................................133x xi LIST OF TABLES Table 2.1: Variants of the wait statement. .................................................................................... 12 Table 2.2: Data types in Promela. ................................................................................................. 29 Table 6.1: Modeling and analyzing the impact of faults. ............................................................. 99 Table 6.2: Modeling and analyzing timing faults in the memory bus system while using LT coding style. ................................................................................................................................ 100 Table 6.3: Modeling and analyzing faults in the NoC switch while using LT coding style. ...... 101 Table 6.4: Modeling and analyzing faults in the memory bus system while using AT coding style. ............................................................................................................................................ 104 Table 6.5: Modeling and analyzing timing faults in the memory bus system while using AT coding style. ................................................................................................................................ 106 Table 8.1: Comparison of the original and sliced models in the absence of faults while using LT coding style. ................................................................................................................................ 122 Table 8.2: Comparison of the original and sliced models in the presence of faults while using LT coding style. ................................................................................................................................ 122 Table 8.3: Comparison of the original and sliced models in the absence of faults while using AT coding style. ................................................................................................................................ 126 Table 8.4: Comparison of the original and sliced models in the presence of faults while using AT coding style. ................................................................................................................................ 127 xii LIST OF FIGURES Figure 1.1: Overview of the proposed framework. ......................................................................... 3 Figure 2.1: SystemC language structure [2]. .................................................................................. 8 Figure 2.2: Structure of a SystemC design. .................................................................................... 9 Figure 2.3: SystemC scheduler [2]. ............................................................................................... 13 Figure 2.4: A simple running example for two communication modules. ................................... 15 Figure 2.5: The Initiator module. .................................................................................................. 17 Figure 2.6: The Memory, the Top, and the Main module............................................................. 18 Figure 2.7: A simple timed automaton. ........................................................................................ 21 Figure 2.8: The viking automaton [9]. .......................................................................................... 25 Figure 2.9: The torch automaton [9]. ............................................................................................ 25 Figure 4.1: The extracted functional model. ................................................................................. 47 Figure 4.2: The Initiator module of the extracted functional model. ............................................ 51 Figure 4.3: The Memory module of the extracted functional model. ........................................... 52 Figure 4.4: Transforming b transport interface into UPPAAL, the Initiator. ............................. 55 Figure 4.5: Transforming b transport interface into UPPAAL, the Target.. ............................... 55 Figure 4.6: The architecture of the memory-mapped busses model. ............................................ 57 Figure 4.7: Fault-intolerant UPPAAL timed automata model of the Initiator module. ................ 58 Figure 4.8: Fault-intolerant UPPAAL timed automata model of the Router module. .................. 58 Figure 4.9: Fault-intolerant UPPAAL timed automata model of the Memory module. ............... 59 Figure 4.10: Requirements of Memory Bus System using LT coding style. ................................ 59 Figure 4.11: Using LT coding style to model NoC switch. .......................................................... 61 Figure 4.12: The Router module. .................................................................................................. 61 Figure 4.13: The address decoding mechanism. ........................................................................... 62 xiii Figure 4.14: Properties of the extracted UPPAAL timed automata .............................................. 62 Figure 4.15: Representation of SystemC TLM Designs in UPPAAL. ......................................... 66 Figure 4.16: Timed automata modeling SystemC scheduler [47]. ............................................... 66 Figure 4.17: Timed automata template for an event object [47]. .................................................. 69 Figure 4.18: Method process template [47]. ................................................................................. 70 Figure 4.19: Thread process template [47]. .................................................................................. 71 Figure 4.20: Timed automata template of the timed ordered list [47]. ......................................... 72 Figure 4.21: Timed automata template of PEQ interface method notify [47]. ............................. 72 Figure 4.22: Timed automata template of the automaton that processes PEQ elements [47]. ..... 72 Figure 4.23: Timed automata model of the PEQ events [47]. ...................................................... 73 Figure 4.24: Non-blocking transport interface architecture. ......................................................... 74 Figure 4.25: Requirements of memory bus system using AT coding style. ................................. 75 Figure 4.26: Timing requirements of memory bus system using AT coding style....................... 76 Figure 6.1: The GUI of UFIT. ...................................................................................................... 94 Figure 6.2: Fault-. ......................................... 96 Figure 6.3: Modeling fail-. ............................. 96 Figure 6.4: Modeling Stuck-. .......................... 96 Figure 6.5: .......................... 97 Figure 7.1: The Sender automaton for the alternating bit protocol. ............................................ 110 Figure 7.2: The Faulty Buffer automaton for the alternating bit protocol. ................................. 110 Figure 7.3: The Receiver automaton for the alternating bit protocol. ........................................ 111 Figure 7.4: Building the sliced model. ........................................................................................ 115 Figure 7.5: The sliced Sender automaton for the alternating bit protocol. ................................. 117 Figure 7.6: The sliced Faulty Buffer automaton for the alternating bit protocol. ....................... 117 xiv LIST OF ALGORITHMS Algorithm 1 Automatic Fault Injection........................................................................................ 89 Algorithm 2 Timed Automata Model Slicing ............................................................................ 112 Algorithm 3 Slice Builder .......................................................................................................... 114 Chapter1 Introduction 1.1Motivation Vericationoftoday™scomplexSoC(SystemonChip)systemsisdifcultinpartduetothehugescaleofintegrationandthefactthatcapturingcrosscuttingconcerns(e.g.,systemverication)intheRegisterTransferLanguage(RTL)[76]isnon-trivial[20].Additionally,SoCsystems,inpractice,areinthepresenceoffaultsthatmakesitevenmoredifculttoverifysuchsystems.Moreimportantly,moderndesignlanguages(e.g.,SystemC[2])enabletheco-designofhardwareandsoftwarecomponents,whichmakesitevenmorechallengingtoVerifySoCsystems.Thus,enablingthesystematic(andpossiblyautomatic)vericationofSystemCprogramsinthepresenceoffaultscanhaveasignicantimpact.SystemCisawidelyacceptedlanguageandanIEEEstandard[2].ItincludesaC++libraryofabstractionsandarun-timekernelthatsimulatesthespeciedsystem,therebyenablingtheearlydevelopmentofembeddedsoftwareforthesystemthatisbeingdesigned.ToenableandfacilitatethecommunicationofdifferentcomponentsinSystemC,theOpenSystemCInitiative(OSCI)[2]hasproposedaninteroperabilitylayer(ontopofSystemC)thatenablestransaction-basedinteractionsbetweenthecomponentsofasystem,calledTransactionLevelModeling(TLM)[4].Theinteroperabilitylayerenablestwomainabstractionlevels(a.k.a.codingstyles),namelyLoosely-Timed(LT)andApproximately-Timed(AT).TheLTstyleofcodingismainlyusedwhendesignersneedfastsimulationofaprogramwithlittleconcernabouttimingissues,whereasthe1ATstyleprovidesanotionofglobaltimeduringsimulation.SinceSoCsystemsaresubjecttodifferenttypesoffaults(e.g.,single-eventupset,hardwareaging,etc.),itisdesirabletostudytheirbehaviorinthepresenceofsuchfaults.However,vericationofSystemCTLMprogramsinthepresenceoffaultsisnon-trivialasdesignershavetodealwithappropriatemanifestationsoffaultsandvericationatdifferentlevelsofabstraction.Inthisthesis,wewilldevelopasystematicandfullyautomatedmethodforaugmentingexistingSystemCTLMprogramswithvericationcapability.Therearenumerousapproachesforfaultinjectionandimpactanalysis,testingandvericationofSystemCprograms.TheseapproacheslackasystematicmethodforvericationofSystemCprogramsinthepresenceoffaults.Testingmethodscanbeclassiedintotwocategories:testpatternsandverication-basedmethods.Testpatterns[28]enabledesignerstogeneratetestcasesandfaultmodels[44]forSystemCprogramsataspeciclevelofabstractionandusetheresultstotestlowerlevelsofabstraction.Vericationapproaches[14,47,55,62,74]usetechniquesforsoftwaremodelcheckingwherenitemodelsofSystemCprogramsarecreated(mainlyasnitestatemachines)andthenpropertiesofinterest(e.g.,dataraceordeadlock-freedom)arecheckedbyanexhaustivesearchinthenitemodel.Faultinjectionmethods[20,27,64,70,75]mainlyrelyonthreetechniquesof(i)insertingafaultycomponentbetweentwocomponents;(ii)replacingahealthycomponentwithafaultyversionthereof,and(iii)injectingsignalswithwrongvaluesatthewrongtime.Then,theyanalyzetheimpactofinjectedfaultsinsystemoutputsatdifferentlevelsofabstraction(e.g.,RTLandTLM)[29].Mostoftheaforementionedapproachesenablethemodelingoffaultsandtheirimpactswithlittlesupportforsystematicvericationthatcanbecapturedatdifferentlevelsofabstraction.2Figure1.1:Overviewoftheproposedframework.1.2ObjectivesandProposedFramework OurobjectiveistofacilitatethevericationofSystemCTLMprogramsbybuildingtoolstopro-videautomationtotheextentfeasible.Ourproposedapproachexploitsmodelextraction,modelchecking,andvericationtechniquestoenableaframeworkforthevericationofSystemCTLMprograms.Specically,ourapproachconsistsofvesteps,namely,de ningformalsemantics,modelextraction,faultmodeling,modelslicing,andmodelchecking.ThesestepsarerepresentedbyProblem1,Problem2,Problem3,Problem4,andProblem5inFigure1.1,respectively.Inthisframework,westartwithaSystemCTLMprogramthatmeetsitsfunctionalrequire-ments,butdoesnotexhibittoleranceinthepresenceofaspecictypeoffaults(e.g.,transientfaults,stuck-atfaults,componentfailure,etc.),calledthefault-intolerantprogram.Existingtest-ingandvericationmethods[14,55,62,74]canbeusedtoensurethataSystemCprogrammeetsitsfunctionalrequirementsintheabsenceoffaults.Intherststep,wedeneaformalsemanticsthatcancapturethetransaction-basedsemanticsofSystemCprogramsatdifferentlevelsofab-3stractionwhilebeingamenabletoautomation(Problem1inFigure1.1).Subsequently,weextractaformalmodeloftheSystemCTLMprogramautomatically(Problem2inFigure1.1).Thereafter,ourframeworkfacilitatesthemodelingofdifferenttypesoffaultsandtheirimpactsontheformalmodel.ThesefaultswillconsidertypicalfaultsconsideredinSystemCprogramssuchastransientfaults,stuck-at,componentfailure,etc(Problem3inFigure1.1).Next,theframeworkprovidesmodelslicingtogenerateasimpliedmodelbasedonproperties/requirements/specicationsofinterest(Problem4inFigure1.1).Finally,theslicedmodelisgiventoamodelcheckerandthemodelcheckergivesuseitherflyesfl,whichmeansthesetofpropertiesissatised,orflnofl,whichmeansthepropertiesisviolated(Problem5inFigure1.1).Incasewherethepropertyisviolated,themodelcheckergivesusacounterexampletoothatcanbeusedforrevisingthemodel.Allofthesevestepsinourframeworkareautomatic.Intherestofthischapter,weexplaineachoftheaforementionedproblemsinsomedetailandgiveanoutlineforthethesis. Problem1:DevelopingaformalsemanticsthatcancapturethecommunicationprotocolsofTLMprogramswhilebeingamenabletoautomation.Inthisstep,wedevelopaformalsemanticsthatpreservesthestructure/architectureofSystemCTLMprograms.ThisformalsemanticsshouldalsoarticulatedifferentcommunicationcharacteristicsalongwithdifferentcodingstylesofSystemCTLMprograms.Problem2:AmethodforextractinganabstractmodelfromSystemCTLMprograms.Inordertoextractaformalmodelautomatically,inadditiontohavingaC++compiler,weneedtoextractarchitectureoftheSystemCTLMprogram.HavingthearchitectureandbehaviorinformationcanalsoassistustotranslatebacktheabstractmodeltotheSystemCprogram.DifferentapproacheshavebeenproposedtoextractaformalmodelfromaSystemCprogram4automatically[61,62,65,66,77].However,tothebestofourknowledge,allofthemonlyconsiderpureSystemCprogramswhileonlyoneofthemconsidersSystemCTransactionlevelModelingprograms.Problem3:Anapproachformodelingandanalyzingtheimpactoffaultsontheformalspeci cationsandthebehaviorsofSystemCTLMprogramsinthepresenceoffaults.Toanalyzetheimpactoffaults,weidentifyhowdifferenttypesofrelevantfaults(e.g.,transientfaults,messagefaults,stuckatfaults,etc.)canberepresentedandinjectedintotheabstractmodel.Problem4:Atechniqueforslicingtheformalmodel.Themodelsextractedareusuallyverycomplex.TheygetevenmorecomplexafterinjectingfaultintotheminProblem3.Hence,weutilizeprogramslicingtechniquestoslicethemodelandgenerateasimpliedversionbasedonthegivensetofproperties.Problem5:Modelcheckingtheformalmodel.Inthisstep,wegivetheslicedmodeltoamodelcheckertobemodelchecked.Ifthespecicationisviolated,themodelcheckergivesusacounterexamplethatcanbeutilizedtorevisetheformalmodel.1.3ThesisOverview InChapter2,wegiveabackgroundonSystemC,TransactionLevelModeling(TLM),UPPAALtimedautomata,andPromela.WedescribesomeofthepreviousworkrelatedtothisthesisinChapter3.InChapter4,rstwediscussabouttherequirementsofatargetformalsemantics,andthenweintroduceasetoftransformationrulesfortransformingaSystemCTLMprogramintoPromelaandUPPAALtimeautomata.Wealsointroduceatoolforextractingtimedautomata5modelsfromSystemCTLMprograms.Afterwards,weusetheextractedmodelsformodelingfaultsinChapter5.Atool,calledUFIT,formodelingfaultsisexplainedinChapter6.ThistoolinjectsdifferenttypesoffaultsintoUPPAALtimedautomatamodels.InChapter7,wediscusshowtoslicetimedautomatamodelsandproposeourtool,calledUSlicerforslicingUPPAALtimedautomatamodelsinChapter8.Finally,inChapter9,weconcludethisdissertationanddescribethepossibledirectionsforfuturework. 1.4BibliographicNotes Someoftheresultsinthisdissertationhaveappearedinpriorpublications.ThematerialsinChap-ter4arebasedonthepaperspublishedinConferencesICDCN2012(InternationalConferenceonDistributedComputingandNetworking)[25],SSS2013(InternationalSymposiumonStabiliza-tion,Safety,andSecurity)[36],NoCArc2013(NetworkonChipArchitectures)[37],andSEFM2014(InternationalConferenceonSoftwareEngineeringandFormalMethods)[39],andJournalTCS2013(TheoreticalComputerScience)[26].ThematerialsinChapter5arebasedonthepa-perspublishedinConferencesSSS2013(InternationalSymposiumonStabilization,Safety,andSecurity)[36],NoCArc2013(NetworkonChipArchitectures)[37],ICDCS2013(InternationalConferenceonDistributedComputingSystems)[38],SEFM2014(InternationalConferenceonSoftwareEngineeringandFormalMethods)[39],andNFM2015(NASAFormalMethods)[40].ThematerialinChapter6isbasedontheworkpublishedinNFM2015(NASAFormalMeth-ods)[40].Finally,thematerialinChapters7and8arebasedontheworkpublishedinDAC2016(DesignAutomationConference)[41].6Chapter2 Preliminaries ThischapterprovidesabriefbackgroundonSystemC(Section2.1),TransactionLevelModeling(Section2.2),UPPAALtimedautomata(Section2.3),andPromela(Section2.4).Theconceptsrepresentedinthischapteraremainlyadaptedfrom[2Œ5,9].2.1SystemC SystemC[2]wasintroducedbytheOpenSystemCInitiative(OSCI)in1996.TheaimoftheOpenSystemCInitiativewastodevelopanopenindustrystandardforsystem-levelmodeling,designandverication.SystemCcanbeseenasbothasystemleveldesignlanguageandaframeworkforHW/SWco-simulation.Itallowsthemodelingandexecutionofsystemleveldesignsonvariouslevelsofabstraction,includingclassicalregistertransferlevelhardwaremodelingandtransaction-baseddesign.Thisallowssystem-leveldesignfromabstractconceptdowntoimplementationinauniedframework.SystemCwithoutextensionscanonlybeusedfordigitalHW/SWsystems.Therealsoexistsanextensionforanalogandmixed-signalcomponents,namelySystemC-AMS,butthisisnotinthescopeofthisthesis.SystemCisimplementedasaC++classlibrary,whichprovidesthelanguageelementsandanevent-drivensimulationkernel.Thelanguagecomprisesconstructsformodularizationandstructuring,forhardware,softwareandcommunicationmodeling,andforsynchronizationandcoordinationofconcurrentprocesses.Fromastructuralpointofview,aSystemCdesignisa7Figure2.1:SystemClanguagestructure[2].setofmodules,connectedbychannels.Thestructurestrictlyseparatesbetweencomputationandcommunicationunits(i.e.,modulesandchannels)andishighly exibleduetoacommunicationconceptthatallowstransactionlevelmodelingandcommunicationrenement.Theevent-drivensimulationkernelregardstheSystemCdesignasasetofconcurrentprocessesthataresynchronizedandcoordinatedbyeventsandcommunicatethroughchannels.TheSystemClanguagearchitectureisshowninFigure2.1[2].TheSystemClanguagepro-videsconstructsforthemodelingofconcurrency,time,reactivity,hardwaredatatypes,hierarchyandcommunication.AsSystemCisimplementedasaC++classlibrary,theC++languagestan-dardconstitutesthebaseofthelanguagearchitecture.Abovethat,thecorelanguageofSystemCprovidesmeanstodescribethestructureandthebehaviorofasystem.Thestructureisdescribedbyusingmodules,channels,ports,andinterfaces,thebehaviorbyusingprocessesandevents.8Figure2.2:StructureofaSystemCdesign.Togetherwiththeevent-drivensimulationkernel,thecorelanguagedenesthesemanticsofSys-temC.Alongsidetothat,theSystemClanguageprovidesasetofhardwaredata-types.Ontopofthecorelanguageandthededicatedhardwaredata-types,asetofelementarychannelsisdened,whichcanbeusedformorespecicmodelsofcomputation,e.g.,FIFOsforfunctionalorsig-nalsforhardwaremodeling.ThetopmostlayeroftheSystemClanguagearchitectureconsistsofdesignlibrariesandmodelsneededformorespecicdesignmethodologiesormodelsofcompu-tation.NotethatthosearenotpartoftheSystemCstandard.TheSystemCstandard[2]comprisesthecorelanguagetogetherwiththeevent-drivensimulationkernel,thededicateddata-types,andtheelementarychannels.Inthefollowing,wedescribeboththestructureandthebehaviorofaSystemCdesignandbrie yreviewthesimulationsemantics. 2.1.1StructuralModeling Fromastructuralpointofview,eachSystemCprogramhasascmainfunction,whichistheentrypointoftheapplicationandissimilartothemainfunctionofaC++program.Inthisfunction,thedesignercreatesstructuralelementsofthesystem,calledmodules,andconnectsthemusingchannels(seeFigure2.2).Theseparationofmodulesandchannelsallowstheseparationofcom-9putationandcommunication.Togetherwitha exiblecommunicationmodelbasedonchannels,ports,andinterfaces,thisallowsTransactionLevelModeling(TLM)withSystemC.Modulesarethebasicbuildingblocksthatallowamodularandhierarchicaldesign.Eachmodulecontainspro-cesses,ports,internaldata,channels,andinterfaces.Aprocessisthemaincomputingelementofamodulethatisexecutableeverytimeaneventistriggered.Aneventisabasicsynchronizationobjectthatisusedtosynchronizebetweenprocessesandmodules.TheprocessesinaSystemCprogramareconceptuallyconcurrentandcanbeusedtomodelthefunctionalitiesofthemodule.Aportisanobjectthroughwhichamodulecommunicateswithothermodules.AchannelisacommunicationelementofSystemCthatcanbeeitherasimplewireoracomplexcommunicationmechanismlikeFIFO.Aportusesaninterfacetocommunicatewiththechannel[2].2.1.2BehavioralModeling SystemCdesignsareexecutedinadiscrete-eventsimulation.Thebasicexecutionunitarepro-cesses,whicharetriggeredbyevents.Thus,fromabehavioralpointofview,aSystemCdesigncanberegardedasanetworkofconcurrentprocesses,whichcommunicatethroughchannelsandsynchronizeonevents.Inthefollowing,wedescribethemainconceptsofprocessesandeventsandhowtheyareusedinthediscrete-eventsimulation. 2.1.2.1Processes Processesarecontainedinmodulesandusetheportsofthecontainingmoduletoaccessexternalchannels.SystemCprovidestwokindsofprocesses:methodprocessesandthreadprocesses.Amethodprocess,whentriggered,alwaysexecutesitsbodyfromthebeginningtotheendanddoesnotkeepaninternalexecutionstate.Itisnotpossibletosuspendandresumeamethodprocess.Incontrasttothat,athreadprocesscanbesuspendedatanytimebycallingawaitfunction.Itkeeps10itsinternalexecutionstateandthuscanberesumedatthepointwhereitwassuspended.Notethatathreadprocessisonlystartedonceatthebeginningofsimulation,whereasamethodprocessmaybeinvokedarbitraryoften.Thefunctionalityofprocessesisdescribedinmethods,whichcontaintheexecutablecodeofaSystemCdesign.Forexecution,themethodsareencapsulatedintoprocesses,whichcarefortheinteractionswiththeschedulerandtheevents.Asaconsequence,methodsareeitherinvokedbytheencapsulatingprocess,orcalledbyothermethods.Thisincludescommunicationmethods,whicharecalledasexternalmethodsthroughtheporttheirchannelisboundto.2.1.2.2Events Boththreadandmethodprocessesaretriggeredbyevents.Aneventisanobjectthatdetermineswhetherandwhenaprocesswouldbetriggered.Thetriggeringofaneventiscalledeventnoti ca-tion.Wheneveraneventisnotied,thistriggerstheexecutionofallprocessesthataresensitivetotheevent.Aprocessmaybesensitivetoaneventeitherstaticallyordynamically.Staticsensitivityisallowedforbothmethodandthreadprocesses,dynamicsensitivityisonlyallowedforthreadprocesses.Astaticsensitivitylistisattachedtoaprocessstaticallywithinthemoduleconstructor,wheretheirstaticsensitivitylistsconsistineachcaseonlyoftheclockevent.Astaticsensitivitylistmayalsocontainmultipleevents.Amethodprocessistriggered,wheneveraneventfromitsstaticsensitivitylistisnotied.Whilemethodprocessesareexecutedfromthebeginningtotheendwheneveraneventfromtheirstaticsensitivitylistoccurs,threadprocessesmaysuspendex-ecutionbycallingawaitfunction.Thisoverwritestheirstaticsensitivitylisttemporarilyandiscalleddynamicsensitivity.Forexample,ifaprocesscallswait(e),itbecomessensitivetotheeventeandisresumedatthenextoccurrence(i.e.,notication)oftheevente.Aprocesscanalsobedynamicallysensitivetomultipleeventsorfortheelapsingofacertainamountoftime.Table2.111showsthevariantsofwaitcallsavailableinSystemC.Asathreadprocesseitherrunsorissus-pended,theonlypossibilitytowaitforaneventfromthestaticsensitivitylistinathreadprocessistosuspenditwithanemptywait()statement.Ifaneventobjecteisnotiedbyitsowner,processesthataresensitivetotheeventstartrespectivelyresumeexecution.wait(e)waitforeventetobenotiedwait(t)waitforttimeunitstoelapsewait(t;e)waitforeventeformaximallyttimeunitswait()waitforanyeventfromthestaticsensitivitylistwait(e1&e2&e3)waitforallthreeeventstobenotiedwait(e1je2je3)waitforanyofthethreeeventstobenotiedTable2.1:Variantsofthewaitstatement.SystemCsupportsthreetypesofeventnotications.Animmediatenoti cation,invokedbye.notify(),causesprocessestobetriggeredimmediatelyinthecurrentdeltacycle.Adelta-delaynoti cation,invokedbye.notify(0),causesprocessestobetriggeredatthesametimeinstant,butafterupdatingprimitivechannels,i.e.,inthenextdelta-cycle.Atimednoti cation,invokedbye.notify(t)witht>0,causesprocessestobetriggeredafterthegivendelayt.Ifaneventisnotiedthatalreadyhasapendingnotication,onlythenoticationwiththeearliestexpirationtimetakeseffect.Thatmeansthatimmediatenoticationsoverrideallpendingnotications,delta-delaynoticationsoverridetimednotications,andtimednoticationsoverridependingtimednoticationsiftheirdelayexpiresearlier. 2.1.3SimulationKernelandScheduler SystemChasasimulationkernelthatenablesthesimulationofSystemCprograms.TheSystemCschedulerisapartoftheSystemCkernelthatselectsoneoftheprocessesthathasanactivatedeventinitssensitivitylist.Thesensitivitylistisasetofeventsortime-outsthatcausesaprocessto12Figure2.3:SystemCscheduler[2].beeitherresumedortriggered.Figure2.3illustratesthebehavioroftheSystemCscheduler.TheSystemCschedulerincludesthefollowingphasestosimulateasystem[2]:1.Initializationphase:Thisphaseinitiatestheprimaryrunnableprocesses.Aprocessisinarunnablestatewhenoneormoreeventsofitssensitivitylisthavebeennotied.2.Evaluationphase:Inthisphase,theschedulerselectsoneprocesstoeitherexecuteorresumeitsexecutionfromthesetofrunnableprocesses.Onceaprocessisscheduledforexecution,itwillnotbepreempteduntilitterminates;i.e.,arun-to-completionschedulingpolicy.Theschedulerstaysintheevaluationphaseuntilnootherrunnableprocessesexist.3.Updatephase:Thisphaseupdatessignalsandchannels.4.delta()noti cationphase:Adeltanoticationisaneventresultingfromaninvocationofthenotify()functionwiththeargumentSCZEROTIME.Uponadeltanotication,theschedulerdeterminestheprocessesthataresensitivetoeventsandtimeouts,andaddsthemtothelistofrunnableprocesses.5.Timednoti cationphase:Ifpendingtimednoticationsortimeoutsexist,thescheduleriden-13tiesthecorrespondingsensitiveprocessesandaddsthemtothesetofrunnableprocesses.2.2TransactionLevelModeling InTransactionLevelModeling(TLM),atransactionisanabstractionofthecommunication(causedbyanevent)betweentwoSystemCcomponentsforeitherdatatransferorsynchroniza-tion.Oneofthecomponentsinitiatesthetransaction,calledtheinitiator,inordertoexchangedataorsynchronizewiththeothercomponent,calledthetarget.ThephilosophybehindTLMisbasedontheseparationofcommunicationfromcomputation[4].Forexample,considertheSystemCTLMprogramofFigure2.4.Inthisexample,wehavetwomodules:initiatorandtarget(Lines6-15,and17-32).Theinitiatormoduleincludesaprocesscalledinitiate,andthetargetmodulehastheincModEightprocess.TheprocessincModEightwaitsforanoticationontheinternalevente(Line29)beforeitupdatesitslocalvariabled.Thescstartstatement(Line39)notiesthesimulationkerneltostartthesimulation.Theeventewillbenotiedwhenthetriggermethodofthetargetiscalledfromtheinitiateprocess(Line14).WhiletheprograminFigure2.4illustrateshowaninitiatorandatargetmodulecancommu-nicateusingSystemCportsandmethodinvocations,theOSCIinitiativefurtherfacilitatesTLMprogrammingbyintroducinganinteroperabilitylayer.Theinteroperabilitylayerincludesasetofcorecomponentsasfollows:CoreInterfaces.Thecoreinterfacescompriseasetofmethodsthatmainlysupporttwoab-stractionlevelssupportedbytwocodingstyles,namelyLoosely-Timed(LT)andApproximately-Timed(AT)codingstyles.TheLTstyleismainlyusedwhendesignersneedfastsimulationofaprogramwithlittlecareabouttimingconcerns.Suchastyleofcodingheavilyreliesonablockingtransportinterfacebtransport()thatshouldbeimplementedintargetmodules141classtarget_if:virtualpublicsc_interfacef2public:3virtualvoidtrigger()=0;4g;5 6classinitiator:publicsc_modulef7public:8sc_portport;9SC_HAS_PROCESS(initiator);10initiator(sc_module_namename):sc_module(name)f11SC_THREAD(initiate);12g13voidinitiate()14fport->trigger();g15g;16 17classtarget:publictarget_if,publicsc_modulef18public:19shortd;20sc_evente;21SC_HAS_PROCESS(target);22target(sc_module_namename):sc_module(name)f23d=0;24SC_THREAD(incModEight);25g26voidtrigger()27fe.notify(SC_ZERO_TIME);g28voidincModEight()f29wait(e);30d=(d+1)%8;31g32g;33 34intsc_main(intargc,char*argv[])f35initiatorinitiator_inst(Initiator);36targettarget_inst(Target);37 38initiator_inst.port(target_inst);39sc_start();40return0;41gFigure2.4:Asimplerunningexamplefortwocommunicationmodules.15andinvokedbyinitiators.TheATstyleofcodingisusedwhentimingissuesareimportanttoconsiderinsimulation.Inthisstyleofcoding,designersbenetfromanon-blockingtransportinterfacenbtransport().Thebtransport()andnbtransport()arepartofthecoreinterfacesintheinteroperabilitylayer.Thecoreinterfacesincludefourothermethods,nonetheless,wefocusonlyonthebtransport()interfaceastherestofthemarebeyondthescopeofthispaper.GenericPayload.InTLM,transactionsareobjectscapturedbyastructure,calledthegenericpayload,thatincludesasetofattributesofthetransactionobject.Sockets.Intheinteroperabilitylayer,modulescommunicatebysendingandreceivingtrans-actions.ObservethatthecommunicationbetweentheinitiatorandthetargetinFigure2.4isachievedthroughne-graineddeclarationofSystemCportsandmethodinvocations,whichrequirestheinitiatortohavesomeknowledgeoftheinternalsofthetarget.Theinterop-erabilitylayerprovidessockets,whichareprogrammingconstructsthatachievetwogoals:connectmodulesbybindinginitiatorandtargetsocketstogether,andfacilitatethetransmis-sionoftransactionsbetweenmodulesbyhidingdetails.BaseProtocol.Thebaseprotocolmaximizesinteroperabilitybyprovidingasetofrulesthatcanbeusedbytheinitiatorandtargetmoduleswhensending/receivinggenericpayloadsthroughsockets.ToillustratetheSystemCTLMprogramsusingTLMBaseprotocolandinteroperability,con-siderthefollowingexampleadaptedfrom[1].Thisexamplemodelshowon-chipmemory-mappedbussesarecapturedusingtheTLMbaseprotocol.Inthisexample(seeFigures2.5and2.6),theInitiatormodule(Lines1-32inFigure2.5)generatesatransaction,whiletheTargetmodule(Lines33-63inFigure2.6)representsasimplememory.Theinitiatormodulehasathreadprocess(Lines161structInitiator:sc_module2ftlm_utils::simple_initiator_socketsocket;3SC_CTOR(Initiator):socket("socket")4fSC_THREAD(thread_process);g5 6voidthread_process()7f8tlm::tlm_generic_payload*trans=newtlm::tlm_generic_payload;9sc_timedelay=sc_time(10,SC_NS);10 11tlm::tlm_commandcmd=static_cast(rand()%2);12 13if(cmd==tlm::TLM_WRITE_COMMAND)data=0xFF000000|0;14 15trans->set_command(cmd);16trans->set_address(0);17trans->set_data_ptr(reinterpret_cast(&data));18trans->set_data_length(4);19trans->set_streaming_width(4);20trans->set_byte_enable_ptr(0);21trans->set_dmi_allowed(false);22trans->set_response_status(tlm::TLM_INCOMPLETE_RESPONSE);23 24socket->b_transport(*trans,delay);25 26if(trans->is_response_error())27SC_REPORT_ERROR("TLM-2","Responseerror");28wait(delay);29g30 31intdata;32g;Figure2.5:TheInitiatormodule.1733structMemory:sc_module34f35tlm_utils::simple_target_socketsocket;36enumfSIZE=256g;37SC_CTOR(Memory):socket("socket")38f39socket.register_b_transport(this,&Memory::b_transport);40for(inti=0;i=sc_dt::uint64(SIZE)||byt!=0||len>4||widsocket.bind(memory->socket);73gg;74intsc_main(intargc,char*argv[])75fToptop("top");76sc_start();77return0;gFigure2.6:TheMemory,theTop,andtheMainmodule.186-29inFigure2.5)thatsendsagenericpayloadtotheTargetmodule;i.e.,theMemorymodule.InLines15-22inFigure2.5,weinitializetheattributescommand,address,data,byteenables,streamingwidth,responsestatus,andDMIhint.Tosend/receiveatransactionto/fromthememorymodule,weneedatwo-waycommunicationbetweenthemodules.Thus,wedeneaninitiatorsocketinLines2-3inFigure2.5andatargetsocketinLine35ofFigure2.6.Theinitia-torsendsthetransactionoutthroughtheinitiatorsocket(Line24inFigure2.5),andthememorycommunicateswiththeinitiatorbyrstregisteringacallbackmethodwiththesocket(Line39inFigure2.6),andthenimplementingthatmethod(Lines44-61inFigure2.6).Thememorymodulethen,inthismethod,implementsthereadandwritecommandsbycopyingdatatoorfromthedataareaintheinitiator(Lines53-58inFigure2.6).Thenalactofthememorymoduleistosettheresponsestatusattributeofthegenericpayloadtoindicatethesuccessfulcompletionofthetransaction(Line60inFigure2.6).Ifnotset,thedefaultresponsestatuswouldindicatetotheinitiatorthatthetransactionisincomplete(Lines26-27inFigure2.5).IneachTLMSystemCprogramweneedascmainfunction(Lines74-77inFigure2.6).Moreover,toconnectupthemodulehierarchy,weusetheTopmodule(Lines65-73inFigure2.6).Thetop-levelmoduleofthehierarchyinstantiatesoneinitiatorandonememory,andbindstheinitiatorsocketintheinitiatortothetargetsocketinthetargetmemory(Line72inFigure2.6).2.3UPPAALTimedAutomata TimedAutomata(TA)arestatemachinesthatenablethemodelingofreal-timesystems[5].Thenotionoftimeiscapturedbyreal-valuedclockvariables.Theclockvaluesareusedtoexpressthetimingconstraintsandcanbeassignedtolocations(vertices)andtransitions(edges)oftheTA.ThesemanticsofTAisgivenbyanin nite-statetransitionsystemwheretransitionscorrespondeither19toachangeoflocation(discretetransition)ortopassageoftime(timetransition).UPPAAL[9,10]isanintegratedtoolenvironmentformodeling,simulation,andveri cationofreal-timesystemsmodeledasnetworksoftimedautomata,extendedwithdatatypes.AsysteminUPPAALconsistsofconcurrentprocesses,eachofthemmodeledasaTA.EachprocessTAhasasetoflocationsandtransitions.Tocontroltransitionsbetweenlocations,UPPAALusesguardsthatlimitwhenprocessactionscanbeexecutedandsynchronizationchannelsthatrequiremultipleprocessestocoordinate.Inthefollowing,we rstintroducethesemanticsofTimedAutomataandNetworksofTimedAutomata.Then,wedescribesomespecialtiesandextensionsoftheUppaalmodelinglanguage. 2.3.1TimedAutomata Astypicalstateautomata,timedautomataconsistofasetofnodes,whicharecalledlocationsandwhichareconnectedbyedges.Anotionoftimeisintroducedbyasetofreal-valuedclockvariablesC:R0.Theyareusedinclockconstraintstomodeltime-dependentbehavior.Theclocksareinitializedwithzeroandthenrunsynchronouslywiththesamespeed.Asaneffectofatransition,aclockmaybereset,i.e.,settozero.Aclockconstraintisaconjunctiveformulaofatomicconstraintsoftheformx˘norx y˘nforx;y2C;˘2f;<;=;>;g;n2N.B(C)denotesthesetofclockconstraints.InTimedB¨uchiAutomata,clockconstraintsareassignedtoedgesandareinterpretedasenablingconditionsforthecorrespondingtransitions.Theycannotforcethetransitiontobetaken.Asaconsequence,aTimedB¨uchiAutomatonmaystayanin niteamountoftimeinthesamelocation.Aluretal.[5]solvedthisproblembyB¨uchiacceptanceconditions.Asubsetoflocationsismarkedasaccepting,andonlyexecutionspassingthroughanacceptinglocationin nitelyoftenareconsideredasvalidbehaviors.Amoreintuitivesolutiontotheproblemofin niteidlingisgivenbyHenzingeretal.[46]byintroducingTimedSafety20Figure2.7:Asimpletimedautomaton.Automata.InTimedSafetyAutomata,onecandistinguishtwokindsofclockconstraints:Guardsareassignedtoedgesandyieldconditions,underwhichthecorrespondingtransitionmaybetaken.Inotherwords,theyenableprogress.Invariantsareassignedtolocationsandyieldconditions,underwhichonemaystayinthecorrespondingstate.Theinvariantsmustnotbeviolated,i.e.,thelocationmustbeleftbeforeitsinvariantisinvalidated.Inotherwords,invariantsensureprogress.Intheremainderofthisthesis,werefertoTimedSafetyAutomatawheneverweusethetermtimedautomata.AsimpleexampleforatimedautomatonisshowninFigure2.7.Itconsistsoftwolocationsl0andl1thatareconnectedbytwoedgesfroml0tol1.Tol0andl1,thesameinvariantx1isassigned.Thatmeansthatinbothlocations,theautomatonmaystayatmostforonetimeunit.Theupperedgefroml0tol1hasaguardx==1,andtheclockyisresetwheneverthisedgeistaken.Theloweredgefroml0tol1hasaguardx1andnoeffect.Asaconsequence,therearetwopossibilitiestocomefromlocationl0tolocationl1:duringtimex2[0;1],theloweredgemay rewithouteffect,andatx=1,theupperedgemay reandyisreset.2.3.2NetworksofTimedAutomataNetworksoftimedautomataareusedtomodelsystemswithconcurrentprocesses.Thestateofanetworkoftimedautomataisde nedasavectorofthecurrentlocationsofalltimedautomatainthenetworkandallclockvaluations.Forsynchronization,theautomatamayinterchangeevents.An21eventissentoverachannelc,andc!andc?denotesendingandreceivinganeventrespectively[11].2.3.3SymbolicSemanticsofTimedAutomata Thesemanticstatespaceoftimedautomataisin niteduetothereal-valuedclockvariables.Thismakesitimpossibletoapplyautomaticveri cationtechniquessuchasmodelchecking,whichexplorethewholesemanticstatespace.Tosolvethisproblem,thesymbolicsemanticspresentedbyBengtssonetal.[10]abstractsfromcertainpointsoftimeandusesclockzonesinstead.Asaconsequence,astateisthenatuple(l;D)whereDisadifferenceboundmatrixrepresentingaclockzone.Theresultingabstractmodelhasa nitestatespaceandcanbemodelchecked.ThefoundationforasymbolicsemanticsoftimedautomatawaslaidbyAluretal.[6].There,thenotionofregionequivalencewasintroduced.Theideaisthattwoclockassignmentscanbeconsideredequivalent,iftheyhavenoin!uenceonthepossibletransitionsthetimedautomatoncantake.Ifonlyintegervariablesareusedinclockconstraintsthatmeansthattwoclockassignmentscanbeconsideredequivalent,whenforeachclockbotharegreaterthanagivenmaximalconstant,alsocalledclockceiling;theirintegerpartisequalandbothhaveafractionalpartofzero,ortheirintegerpartisequalandbothhaveafractionalpartgreaterthanzero.Inanycase,thetwoclockassignmentshavetobeinthesamerelationtoallotherclocks.2.3.4UPPAAL UPPAAL[9,10]isatoolsetforthemodeling,simulation,animationandveri cationofnetworksoftimedautomata.TheUPPAALmodelcheckerenablestheveri cationoftemporalproperties,22includingsafetyandlivenessproperties.Thesimulatorcanbeusedtovisualizecounter-examplesproducedbythemodelchecker.2.3.4.1ModelingLanguage TheUppaalmodelinglanguageextendstimedautomatabyintroducingparameterizedtimedau-tomatatemplates,boundedintegervariables,binaryandbroadcastchannels,andurgentandcom-mittedlocation.Timedautomatatemplatesprovidethepossibilitytomodelsimilartimedautomataonlyonceandtoinstantiatethemarbitraryoftenwithdifferentparameters.Timedautomataaremodeledasasetoflocations,connectedbyedges.Theinitiallocationisdenotedby.Invari-antscanbeassignedtolocationsandenforcethatthelocationisleftbeforetheywouldbeviolated.Edgesmaybelabeledwithselections,guards,updates,andsynchronizations.Selectionsareusedtonon-deterministicallybindagivenidenti ertoavalueinagivenrange.Updatesareusedtoresetclocksandtomanipulatethedataspace,i.e.,theyprovidetheactionstheautomatonmayperform.Processessynchronizebysendingandreceivingeventsthroughchannels.Sendingandreceivingviaachannelcisdenotedbyc!andc?,respectively.Binarychannelsareusedtosynchronizeonesenderwithasinglereceiver.Asynchronizationpairischosennon-deterministicallyifmorethanoneisenabled.Ifnocommunicationpartnerisavailable,boththesenderandthereceiverareblockediftheysynchronizeonabinarychannel.Broadcastchannelsareusedtosynchronizeonesenderwithanarbitrarynumberofreceivers.Anyreceiverthatcansynchronizemustdoso.Incontrasttobinarycommunication,aprocesssendingonabroadcastchannelisneverblocked.Urgentandcommittedlocationsareusedtomodellocationswherenotimemaypass.Urgentloca-tionsaregraphicallydepictedbythesymbol,committedlocationsbythesymbol.Leavingacommittedlocationhaspriorityoverleavingnon-committedlocations.AnUppaalmodelcomprisesthreeparts:globaldeclarations,parameterizedtimedautomata23(TAtemplates)andasystemdeclaration.Intheglobaldeclarationssection,globalvariables,con-stants,channelsandclocksaredeclared.Thetimedautomatatemplatesdescribetimedautomatathatcanbeinstantiatedwithdifferentparameterstomodelsimilarprocess.Inthesystemdecla-ration,thetemplatesareinstantiatedandthesystemtobecomposedisgivenasalistoftimedautomata. 2.3.4.2QueryLanguage Thequerylanguage,whichisusedinUPPAALtoexpressrequirementsspeci cations,isare-strictedversionofCTL[9].LikeinCTL,thequerylanguageconsistsofpathformulasandstateformulas.Stateformulasdescribeindividualstates,whereaspathformulaquantifyoverpathsofthemodel.Pathformulacanbeclassi edintoreachability,safety,andliveness.Stateformulasareexpressionsthatcanbeevaluatedforagivenstatewithoutlookingattherestofthemodel.Thisincludesbooleanexpressionsonvariables(e.g.,x4)andtestswhetheraparticularprocessisinagivenlocation(e.g.,P1.init).Adeadlockisexpressedusingthespecialstateformuladeadlock.Pathformulasexpresseitherreachability,safety,orlivenessproperties.Thereachabilityprop-ertythatsomestatesatisfyingagivenstateformula˚isexpressedbyE<>˚.Thesafetypropertiesthatastateformula˚isalwaystrueisexpressedbyA[]˚,whereasA[]˚saysthatthereexistsapathwhere˚isalwaystrue.Theclassicallivenesspropertythatsomethinggoodwilleven-tuallyhappenisexpressedbyA<>˚.Additionally,thereexistsaleadstoorresponseproperty˚ > ,whichexpressesthatwhenever˚issatis ed, willeventuallybesatis ed.24Figure2.8:Thevikingautomaton[9].Figure2.9:Thetorchautomaton[9].2.3.4.3AnIllustrativeUPPAALExample AnexampleforanUPPAALmodeltakenfromthedemomodelsincludedinthefreeUPPAALdistributionistheriddleofthefourvikings.Theriddleisasfollows:fourvikingswanttocrossabridgeatnight,buttheyhavegotonlyonetorchandthebridgecanonlycarrytwoofthem.Thus,theycanonlycrossthebridgeinpairsandonehastobringthetorchbacktotheothersidebeforethenextpaircancross.Thevikingshavedifferentspeeds,thefastestneeds5minutes,theslowest25minutes,andtheothertwo10and20minutes.Thequestioniswhetheritispossiblethatallthevikingscrossthebridgewithin60minutes.TomodelthisprobleminUPPAAL,weneedtwotimedautomatatemplates,oneforthevikingswhichisinstantiatedwiththedifferentdelays,andoneforthetorch,seeFigures2.8and2.9.Therepresentationoftimedautomataisausualautomatarepresentationwithlocationsconnectedbyedges.Inaddition,wehavetwochannelstakeandrelease,whichmodeltheinteractionbetweenthevikingsandthetorch.Furthermore,wehaveadatavariableLwhichservesasasemaphoreto25ensurethatthetorchcanonlybeononesideofthebridgeatatime,andwehaveaclockvariableyandaclockconstraintydelaywhichmodelsthetimeittakesthevikingstocrossthebridge.Avikingisontheothersideofthebridgeifitisinitssafelocation.Thequestioniftheyallcancrossthebridgein60minutescanbeformalizedasanexistentialquanti cationoverastatewhereallvikingsareintheirsafelocationandtimeislessorequalthan60minutes:E<>Viking1.safeandViking2.safeandViking3.safeandViking4.safeandtime<=60NotethattheexampleofthefourvikingsiscomparabletothequestionifapacketcanreachitsreceiverinagiventimelimitinacommunicationnetworkoraNetworkonChip(NoC)systems.2.4SPINandPromela SPIN[48]isanef cientveri cationsystemforanalyzingthelogicalconsistencyofdistributedsystems,speci callyofdatacommunicationprotocols.Ithasbeenusedtodetectdesignerrorsinapplicationsrangingfromhigh-leveldescriptionsofdistributedalgorithmstodetailedcodeforcon-trollingtelephoneexchanges.ThesystemisdescribedinamodelinglanguagecalledPROMELA(ProcessorProtocolMetaLanguage).Thelanguageallowsforthedynamiccreationofconcur-rentprocesses.Inthissection,weprovideabriefdescriptionofSPINandexplainthebasicsofPromela. 2.4.1ModelingLanguage Promelaisaveri cationmodelinglanguage.UsingPromelawecanmakeabstractionsofprotocols(ordistributedsystemsingeneral)thatsuppressdetailsthatareunrelatedtoprocessinteraction.26TheintendeduseofSpinistoverifyfractionsofaprocessbehaviorthatareconsideredsuspect.TherelevantbehaviorismodeledinPromelaandveri edusingSpin.Acompleteveri cationisthereforetypicallyperformedinaseriesofsteps,withtheconstructionofincreasinglydetailedPromelamodels.Eachmodelcanbeveri edwithSpinunderdifferenttypesofassumptionsabouttheenvironment(e.g.,messageloss,messageduplicationsetc).OncethecorrectnessofamodelhasbeenestablishedwithSpin,thatfactcanbeusedintheconstructionandveri cationofallsubsequentmodels.ThesyntaxofPromelaisbasedontheCprogramminglanguage.APromelamodelcomprises(1)asetof(concurrent)processes(2)asetofvariables,and(3)asetofmessagechannels.Thepro-cessesspecifythebehaviorofthemodelandallprocessesareglobalobjects.Also,eachPromelamodelhastocontainatleastoneprocesstobemeaningful.Thevariablesareutilizedtostoretheinformationaboutthesystembeingmodeledandcanbedeclaredgloballyorlocallywithinaprocess.Theglobalvariablesde netheenvironmentinwhichtheprocessrun.Messagechannelsareusedtomodelthetransferofdatafromoneprocesstoanother.Next,weexplainprocesses,variables,andmessagechannelsinsomedetail. 2.4.1.1Processes Thestateofavariableorofamessagechannelcanonlybechangedorinspectedbyprocesses.Thebehaviorofaprocessisde nedinaprede nedtype,calledproctype.Thistypecontainstheprocessidenti er,formalparameterlist,andlocalvariabledeclarationandstatements.Thecontentsfallsintothefollowingformoftheproftypedeclaration:proctypeprocess_identifier(formalparameter){localvariabledeclarations27andstatement}ThesemanticsofPromelaisbasedonanoperationalmodelthatde neshowtheactionsofproctypesareinterleaved.Anaction(alsoknownasaguardedcommand)isoftheformgrd!stmt,wheretheguardgrdisanexpressionintermsofthePromelamodel™svariablesandthestatementstmtmayupdatesomemodelvariables.Actionscanbeatomicornon-atomic,whereanatomicaction(denotedbytheatomicfgblocksinPromela)ensuresthattheguardevaluationandtheexecutionofthestatementarenotinterrupted.Asanillustrationforatomicactions,considerthefollowingexample.atomic{/*swapthevaluesofaandb*/tmp=b; b=a; a=tmp }Intheexample,thevaluesoftwovariablesaandbareswappedinasequenceofstatementexecutionsthatisde nedtobeuninterruptable.Thatis,intheinterleavingofprocessexecutions,nootherprocesscanexecutestatementsfromthemomentthatthe rststatementofthissequencebeginstoexecuteuntilthelastonehascompleted.Itisoftenusefultouseatomicsequencestostartaseriesofprocessesinsuchawaythatnoneofthemcanstartexecutingstatementsuntilallofthemhavebeeninitialized:init{atomic{28TypeRangebit0::1bool0::1byte0::255short 215::215 1int 231::231 1Table2.2:DatatypesinPromela.runA(1,2); runB(2,3); runC(3,1) }}Atomicsequencesmaybenon-deterministic.Ifanystatementinsideanatomicsequenceisfoundtobeunexecutable,however,theatomicchainisbroken,andanotherprocesscantakeovercontrol.Whentheblockingstatementbecomesexecutablelater,controlcannon-deterministicallyreturntotheprocess,andtheatomicexecutionofthesequenceresumesasifithadnotbeeninterrupted. 2.4.1.2Variables Table2.2summarizesthe vebasicdatatypesusedinPromela.Bitandboolaresynonymsforasinglebitofinformation.The rstthreetypescanstoreonlyunsignedquantities.Thelasttwocanholdeitherpositiveornegativevalues.Theprecisevaluerangesofvariablesoftypesshortandintisimplementationdependent,andcorrespondstothoseofthesametypesinCprogramsthatarecompiledforthesamehardware.292.4.1.3Messagechannels Messagechannelsaredeclaredeitherlocallyorglobally,forinstanceasfollows:chanqname=[16]of{byte}Thisdeclaresachannelthatcanstoreupto16messagesoftypebyte.Channelnamescanbepassedfromoneprocesstoanotherviachannelsorasparametersinprocessinstantiations.Tosendthevalueexpressionexprtothechannelqname,weusethefollowingcommandthatappendsthevaluetothetailofthechannel.qname!exprAdditionally,toreceivethevalueexpressionexprfromthechannelqname,weusethefollowingcommandthatretrievestheexpressionfromtheheadofthechannel.qname?exprMoreover,ifwewanttosendandreceivethemessageswithoutstoringthem,wecanuseren-dezvouschannels.Thesetypesofchannelsarede nedasfollows.chanqname=[0]of{byte}Considerthatrendezvouscommunicationisbinary:onlytwoprocesses,asenderandareceiver,canbesynchronizedinarendezvoushandshake. 2.4.2ControlFlow Inthissection,weidentifytwoimportantcontrol!owconstructsinPromela:caseselectionANDrepetition.302.4.2.1Caseselection Theselectionstructurecancontainmorethatoneexecutionsequence,eachprecededbyadoublecolon.Onlyonesequencefromthelistwillbeexecuted.Asequencecanbeselectedonlyifits rststatementisexecutable.The rststatementisthereforecalledaguard.Forinstance,inthefollowingselectionstructure,wehavetwoexecutionsequencesthatcanbeselectednon-deterministically.if ::(a!=b)->option1 ::(a==b)->option2 fi2.4.2.2Repetition Alogicalextensionoftheselectionstructureistherepetitionstructure.Onlyoneoptioncanbeselectedforexecutionatatime.Aftertheoptioncompletes,theexecutionofthestructureisrepeated.Thenormalwaytoterminatetherepetitionstructureiswithabreakstatement.Asanexample,thefollowingstructurerandomlychangesthevalueofthevariablecountupordownsproctypecounter() {do ::count=count+1 ::count=count-1 ::(count==0)->break31od}2.4.3Veri cationwithSPIN Givenamodelsystemspeci edinPromela,Spincaneitherperformrandomsimulationsofthesystem™sexecutionoritcangenerateaCprogramthatperformsafastexhaustiveveri cationofthesystemstatespace.Theveri ercancheck,forinstance,ifuserspeci edsysteminvariantsmaybeviolatedduringaprotocol™sexecution.Forthispurpose,asetofpropertiesneedstobegiventoSpininLinearTemporalLogic(LTL)structure.InLTL,onecanencodeformulaaboutthefutureofpaths,e.g.,aconditionwilleventuallybetrue,aconditionwillbetrueuntilanotherfactbecomestrue,etc.AnLTLformulacancontaintheunarytemporaloperators(pronouncedalways),(pronouncedeventually),andbinarytemporaloperatorsU(pronounceduntil).2.5Summary Inthissection,wepresentedtherelevantbackgroundforourframework.Tothisend,wegaveanintroductiontoSystemCprogramsandTransactionLevelModeling.WealsoexplainedtheformallanguageofUPPAALtimedautomata,whichcomeswithatoolsuiteformodeling,simulationandanimationoftimedautomataandamodelchecker.Finally,wedescribedPromelalanguagewhichistheinputofSPINmodelchecker.32Chapter3 RelatedWork ThissectiondiscussesexistingapproachesforformalanalysisofSystemCTLMprograms.Extantworkcanbroadlybeclassi edintofourcategories:methodsforformalizingthesemanticsofSys-temCTLMprograms,checkersforSystemCdesigns,staticanalysisandstatelessmodelcheckingofSystemCprograms,andmodelextractionandmodelcheckingofSystemCTLMprograms.Inthenextsections,weexplaintheresearchesineachcategoryinsomedetail.3.1FormalizingtheSemantics SeveralresearchersfocusonassigningformalsemanticstoSystemCTLMprograms.Forexam-ple,ade nitionofthesimulationsemanticsbasedonabstractstatemachinesisgivenbyM¨ulleretal.[67]andRufetal.[72].ThepurposeoftheirworkistoprovideaprecisedescriptionoftheSystemCscheduler.However,thesystemdesignitself,asbuiltfrommodules,processesandchan-nels,isnotcoveredandthereforecannotbeveri edwiththisapproach.NiemannandHaubelt[68]provideanapproachforspecifyingthesemanticsofSystemCTLMprogramsusingdeterministicCommunicatingStateMachines.Intheirapproach,onlytheautomatonthatexplicitlycapturestheschedulerhasnon-deterministicbehaviors.PatelandShukla[69]presentaformalizationofSystemCinabstractstatemachinesandreviseMicrosoftSpecExplorerforthevalidationandde-buggingofSystemCprograms.KroeningandSharygina[53]createabstractmodelsofSystemCprogramsusingLabeledKripkeStructures(LKS),whereeachSystemCthreadiscapturedbyan33LKS.ALabeledKripkeStructuresisadirectedgraphwhosenodesrepresentstatesannotatedbyatomicpropositionsthatholdinthatstate.Thearcsofthedirectedgraphdenotetransitionsbe-tweenstatesthatarelabeledbyactions.TheabstractstateoftheSystemCprogramisde nedintermsofthelocalstatesofitsthreads,theirprogramcountersandthestatusofeachthreadinSystemCscheduler.Salem[73]presentedadenotationalsemanticsfortheSystemCschedulerandforSystemCprocesses,butonlyforasynchronoussubset.Habibietal.[34,35]proposedprogramtransformationsfromSystemCintoequivalentstatemachines.Intheseapproaches,timeisignored,andthetransformationisperformedmanually.Besides,thestatemachinemodelsdonotre!ectthestructureoftheunderlyingSystemCdesigns.Traulsenetal.[77]proposedamap-pingfromSystemCtoPROMELA,buttheyonlyhandleSystemCdesignsattransactionlevel,donotmodelthenon-deterministicschedulerandcannotcopewithprimitivechannels.HarrathandMonsuez[43]introducedtheformalismofSystemCwaiting-stateautomata.ThoseSystemCwaiting-stateautomataaresupposedtoallowaformalrepresentationofSystemCdesignsatthedelta-cyclelevel.However,theapproachislimitedtothemodelingofdelta-cycles,theschedulerandcomplexinteractionsbetweenprocessesarenotconsideredandtheformalmodelhastobespeci edmanually.Man[59]presentedtheformallanguageSystemCFL,whichisbasedonpro-cessalgebrasandde nesthesemanticsofSystemCprocessesbymeansofstructuraloperationalsemanticsstyledeductionrules.SystemCFLdoesnottakedynamicsensitivityintoaccount,andconsidersonlysimplecommunications.Theconceptofchannelsisneglected.Atooltoautomat-icallytransformSystemCtoSystemCFLispresentedbyManetal.[60].However,itdoesnothandleanykindofinteractionbetweenprocesses.Karlssonetal.[52]verifySystemCdesignsus-ingapetri-netbasedrepresentation.Thisintroducesahugeoverheadbecauseinteractionsbetweensubnetscanonlybemodeledbyintroducingadditionalsubnets.Herberetal.[47]proposeanapproachtode neaformalsemanticsforSystemCthatcanhandle34relevantSystemClanguageelements,includingprocessexecution,interactionsbetweenprocesses,dynamicsensitivityandtimingbehavior.Theinformallyde nedbehaviorandthestructureofSystemCdesignsarecompletelypreserved.ThemappingfromSystemCdesignsintoUppaaltimedautomataisfullyautomated,introducesanegligibleoverhead,producescompactandcomparablysmallmodelsandenablestheuseoftheUppaalmodelcheckerandtoolsuite.3.2CheckersforSystemCDesigns TherehasbeensomeworkoncheckersforSystemCdesigns.Forexample,anapproachtochecktemporalassertionsforSystemChasbeenpresentedbyRufetal.[72].MorerelatedtoourworkistheworkofDrechsler,GroßeandK¨uhne[23,30Œ33].In[23],theydescribehowtoconvertagate-levelmodelgiveninSystemCintoBDDs.TheBDDisusedforforwardreachabilityanaly-sis.In[30],theypresentamethodwhichallowscheckingoftemporalpropertiesforcircuitsandsystemsdescribedinSystemC,notonlyduringsimulation.Apropertyistranslatedintoasynthe-sizableSystemCcheckerandembeddedintothecircuitdescription.Thisenablestheevaluationofthepropertiesduringthesimulationaswellasafterthefabricationofthesystem.In[31,32],theypresentanapproachtoprovethataSystemCmodelsatis esagivenpropertyusingboundedmodelcheckingandshowtheapplicabilityoftheapproachwiththeco-veri cationofaRISCCPUimplementedinSystemC.In[33],theyusea3-stepapproach.First,theyverifythefunctionalcor-rectnessoftheunderlyinghardwareusingboundedmodelchecking.Then,theyverifytheHW/SWinterface.Thismeansthattheyverify,thateachinstructionthroughwhichthesoftwarecanaccessthehardwarehasthespeci edeffectsonallhardwareblocksinvolved.Finally,assemblerpro-gramsareveri edbyconstrainingtheinstructionsoftheprogramasassumptionsintheproof.Inotherwords,theinstructionsofagivenassemblerprogramaretranslatedintoassumptionsandthe35knowneffectsonthehardwareareusedfortheproof.ThemainlimitationoftheworkofDrechsler,GroßeandK¨uhneisthattheirapproachesareallrestrictedtosynchronousandcycle-accuratemodelsonregister-transferlevel.Asaconsequence,theycan,inparticular,notverifymodelsusingSystemCchannels,necessaryfortransactionlevelmodeling(TLM),norcantheyhandledynamicortimingsensitivity.Withourapproach,wecanhandleSystemCdesignonlowabstraction-levelsaswellasdesignsonhighabstraction-levelsandthuswecansupportthewholedesign-process. 3.3StaticAnalysisandStatelessModelChecking Manytechniquescombinestaticanalysiswithcontrolledschedulinginordertoenablestatelessmodelchecking,wherenoexplicit-statemodelisgeneratedandpropertiesarecheckedastheprogramexecutes.Forinstance,BlancandKroening[14]presentacompilerthatusesmodelcheckingtopredictraceconditionsinSystemCprograms.Theyusetheresultsofpredictionsduringsimulationinordertoreducethenumberofinterleavings.Kunduetal.[55]staticallycomputethetotalnumberofatomicblocksinSystemCcodeandthenanalyzethedependencyofatomicblocksoneachother.AnatomicblockinSystemCisthecodebetweentwoconsecutivewait()statements.Twoblocksaredependentifoneofthemenables/disablesanotheroroneofthemwritesasharedvariablethattheotheronereads.Themainadvantageofstatelessmodelcheckingisthatthereisnoneedformodelextraction;however,theygenerallyhaveaboundednatureinthattheapproachisincomplete(i.e.,itmaymisssomeerrors).Thisinherentfeatureofstatelessmodelcheckingmakesitdif culttomodeltheimpactoffaultsontheentiresetofbehaviorsofamodelduetoitson-the-!yanalysisnature.363.4ModelExtractionandModelChecking Modelextractionandmodelcheckingmethodsuseasetofrulesforsemantics-preservingtrans-formationofSystemCprogramstothemodelinglanguageofsomemodelcheckers.Forexample,Moyetal.[66]modelaSystemCprogramastheautomata-theoreticproductofasetofsyn-chronousautomatarepresentingSystemCthreadsalongwithanautomatonrepresentingthesimu-lationschedulerofSystemC.Theyprovideanintermediateformallanguage,calledHeterogeneousParallelInput/OutputMachines,thatcancapturebothsynchronousandasynchronousautomata.Traulsenetal.[77]presentamethodfortransformingasubsetofSystemCtothePromela[3]modelinglanguageinordertoenablethemodelcheckingofasynchronoussoftwarethreadsintheSPINmodelchecker[48].MarquetandMoy[62]presentafront-endthattransformsSystemCprogramstoanintermediatelanguageinLLVM[57],whichisaframeworkthatprovidesreusablecomponentsforcompilerconstruction.Marquetetal.[61]presentamodelextractionschemefromSystemCtoPromelawheretheyprovideasetoftransformationrulesforthesynchronizationprim-itivesofSystemC(i.e.,waitandnotifystatements).Moreover,theyavoidexplicitmodelingoftheSystemCscheduler,andpresentasetofinvariantconditionsforvalidatingthatthetransformationrulesaresemantics-preserving.Cimattietal.[21]presentamodelcheckingapproachsupport-ingtwotechniques;onemethodthatgeneratessequentialCprogramsfromSystemCcodewhereSystemCthreadsanditsschedulerarecapturedasfunctionsandsafetypropertiesarecheckedasassertions,andtheotherisahybridtechniquewhereexplicit-statemodelingisusedtocapturethebehaviorsoftheSystemCschedulerandSystemCthreadsaremodeledsymbolically.Herberetal.[47]proposeatoolsetbasedonanautomatictransformationofaSytemCTLMprogramintoasemanticallyequivalenttimedautomatamodel.Theyusethistransformationtotestasetofsafetyandlivenessproperties.However,thisworkdoesnotconsiderfaultsandtheir37impactsonthemodel.Theirtoolset,calledSTATE(SystemCtoTimedAutomataTransformationEngine),takesaSystemCTLMprogramasaninputandtransformsitintoformallyequivalentUPPAALtimedautomataastheoutput.Hence,itispossibletoverifysafety,liveness,andtim-ingpropertiesofthegivenSystemCTLMprogramusingUPPAALmodelchecker.ThistoolsethandlesallSystemCelementssuchasprocesses,interactionbetweenthem,dynamicsensitivity,andtimingbehavior.Inthetransformation,eachmethodismappedtoasingleautomatonandinteractionsbetweenprocessesaremodeledbychannels.Asafront-end,STATEusesKaSCPar(KarlsruheSystemCParser)[52]thatgetsaSystemCTLMprogramandgeneratesanAbstractSyntaxTree(AST)inXML.Theback-endofSTATEutilizestheASTandgeneratesUPPAALtimedautomatainXML.ThetransformationpreservesthebehavioralsemanticsandthestructureofagivenSystemCdesign.Inparticular,itcapturesthesemanticsoftheTLMcoreinterfaces,includingthepayloadeventqueue(PEQ). 3.5Summary Therehasbeenaconsiderableamountofworkintheareaofformalveri cationofSystemCde-signs.However,allofthepresentedapproacheshavetheirlimitations.TheyareeitherrestrictedtosubsetsofSystemCthatprecludethemfromtheapplicationduringthewholedesignprocess,ortheylackformalfoundation,ortheyrequirealotofmanualeffort.Tothebestofourknowledge,acomprehensiveco-veri cationframeworkthatsupportsfullyautomaticveri cationtechniquesandyieldsahighdegreeofreliabilityduetotheuseofformalmethodsdoesnotexist.Withourapproach,weprovidesuchaframework.38Chapter4 FormalSemanticsandModelExtraction Inthischapter, rst,weintroducetherequirementsofdevelopingaformalsemanticsinSection4.1.TheserequirementsneedtocapturetheessentialsoftheSystemCTLMmodelswhilestillbene tingfromautomationtechniquesforveri cationand/orsynthesis.Then,inSection4.2,wediscusstheessentialsoftransformationrules.Consideringtheserequirements,weproposeasetoftransformationrulesinSections4.3totransformaSystemCTLMprogramintoaPromelamodel.Thereafter,inSection4.6,weproposeasetofrulestotransformaLoosely-Timed(LT)SystemCTLMprogramintoatimedautomatamodel.Theseruleshelpusextractatimedautomatamodelwhichissimpli ed.Wealsointroduceatool-set,calledSTATE(SystemCtoTimedAutomataTransformationEngine),inSection4.9thatweusetoextracttimedautomatamodelsfromAp-proximatelyTimed(AT)SystemCTLMprograms.Toillustrateourmodelextractionideas,weapplythemon vecasestudiesandexplaineachofthemindetailinSections4.4,4.5,4.7,4.8,and4.10. 4.1DevelopingaFormalSemantics Sinceveri cationandsynthesisofSystemCprogramsisingeneralundecidable,weneedtheirabstractrepresentationsthatenableautomatedanalysisandrevision.Toutilizesuchanabstractrepresentation,weneedtodevelopaformalsemanticsofSystemCTLMprograms.Theobjectivesofthisformalsemanticsare(1)enablingderivationofformalmodelsofSystemCTLMprograms39atdifferentlevelsofabstractionandinthepresenceofdifferenttypesoffaults,and(2)analysisandrevisioninthepresenceoffaults.Itisdesirablethatthisformalsemanticssatis esthefollowingrequirements:Preservethestructure/architectureoftheSystemCTLMprogram.ArticulatedifferentcommunicationcharacteristicsintheSystemCTLMprogram.ExpressdifferentcodingstylesintheSystemCTLMprogram.Permitef cientanalysiswithavailabletool-chains.Ofthese,the rstrequirementismotivatedbythefactthattransactionbasedmodelingassistsinsimplifyingthedesignofSystemCprograms.Weintendtopreservethispropertywhiledevelopingtheformalsemantics.Thiswillalsosimplifythetaskofsynthesiswhereweintendtoobtainthecorrespondingfault-tolerantSystemCTLMprogram.Thesecondrequirementismotivatedbythefactthatthesemanticsshouldbeexpressiveenoughtoarticulatedifferentcommunicationcharacteristics.Sincetransactionsarecentraltothemodelbaseddesignmethodology,communicationcharacteristicsamongmodulesareseparatedfromthedetailsoftheimplementationoffunctionalunits.Thisseparationencapsulateslow-leveldetails,e.g.,busmodels,oftheinformationexchange.Regardingthethirdrequirement,ourfocusisonAT(Approximately-Timed)andLT(Loosely-Timed)models.TheATmodelissuitableforperformancemodelingandarchitectureexplorationwhiletheLTmodelismainlyusedwhendesignersneedfastsimulationofaprogramwithlittlecareabouttimingconcerns.TheATmodelallowsustokeeptheprocessesinthegivenmodelsynchronizedtoacommonclock.Inthismodel,eachprocessrunsataspeci ctimeandthistimecorrespondstotheactualtimewhenthecorrespondingactivityisscheduledtooccurinthe40realsystem.Thiscreatesfutureeventsthatarecreatedinresponsetotheeventthatiscurrentlyprocessed.Also,generally,thismodelutilizesnonblockingtransportinterfacenbtransport()formaximalconcurrency.Bycontrast,theLTcodingstyleallowsprocessestorunasfastaspossiblewithsomefairnessforallinitiatorssothattheycanperformtheirtransactions.Thisallowsfortemporaldecoupling.EventhoughLoosely-Timed,thismodelallowstimeasaninterrupt.More-over,generally,thiscodingstyleutilizesblockingtransportinterfacebtransport()forsimplifyingsystemexecution.Anotherimportantissuefordevelopingtheformalsemanticsisthatitrestrictsthesetofveri- cationback-endsthatcanbeapplied.Theseback-endscanbeeitherinthecategoryofsymbolicmodelcheckerslikeLustre[42],SMV[18]orEsterel[13]tool-chains,oroneofthetimed-modelcheckerslikeIF[16]orUPPAAL[56],oranexplicit-statemodelcheckerlikeSPIN[48].4.2ExtractingtheFormalSemanticsfromtheSystemCTLMProgramInordertoextractanabstractformalmodelfromtheSystemCTLMprogram,weneedasetoftransformationrules.Thisformalmodelfacilitatesveri cationofthesemanticpropertiesdevel-opedinSection4.1.Forthispurpose,webuildontheideasfrom[68],whereeachSystemCTLMprogramhasthreebasicprocesses,Behavior,InitiatorandTarget.ThebehaviorprocesscapturesthemainfunctionalityoftheTLMmodule.Aninitiatorandatargetprocessparticipateintrans-actions.TheexecutionoftheTLMprogramswitchesbetweentheseprocesses.TheextractedmodelwouldpreservethisstructureoftheTLMprogrameitherwithrulesthatmodelthesched-ulerexplicitlyorimplicitly.Withexplicitscheduler,theschedulerismodeledasaspecialprocesswhereaswithimplicitscheduler,theschedulingdecisionswouldbehardcodedintheextracted41model.Whiletheformerismoregeneralandwouldbeusefulinthecontextoffaultsthataffectthescheduler,thelatterwouldbeusefulinimprovingperformanceofveri cationand/orrepairoftheSystemCTLMprogram.OurmodelextractionfocusesonboththeLTcodingstyleandtheATcodingstyle.SincetheSystemCsimulationkernelhasarun-to-completionschedulingpolicy,athread/processcannotbeinterrupteduntilitiseitherterminatedorwaitsforanevent.WeusethispolicytobuildupourmodelextractionwhilehavingLTcodingstylebymodelingtheschedulerimplicitly.Animplicitschedulerissuf cientforthecasewherethegivenSystemCTLMprogramcontainsasmallnum-berofprocesses,doesnotutilizefeaturessuchastimednoti cations,andtheschedulingdecisionsaresimple.Forcomplexalgorithms,theschedulerismodeledexplicitly.Notethatthisexplicitschedulercapturestheschedulingpolicyanddoesnotdirectlydependupontheinputprogram.Hence,ourmodelswouldprovidetypicalschedulers,e.g., rst-come- rst-servescheduler,prioritybasedscheduler,usedinpractice.Ontheotherhand,forATstyleitismoredesirabletomodeltheschedulerexplicitly,sincetimingissuesareimportanttoconsiderinprogramexecution.Typ-ically,encodingtheschedulerexplicitlyinducesadditionalcommunicationsbetweenprocesses,comparedtotheoriginalSystemCsemantics.Thiscanleadustoadditionalcommunicationsthatmaypreventveri cationtoolstoperformpowerfuloptimizations.Next,wepresenttwosetsoftransformationrules.The rstsetofrulesisusedforgeneratingPromelamodelsfromSystemCTLMprogramswrittenbasedontheTLMbaseprotocolforinter-operability.ThesecondsetofrulesisusedtogenerateUPPAALtimedautomatafromtheSystemCprograms.424.3TransformationRulesforGeneratingPromelaModels Ourobjectiveinthissectionistode neasetofrulestotransformtheprocessesexplainedinSection4.2,i.e.,Behavior,Initiator,andTarget,toPromela.WespecifyatransformationruleasXj--Y,whereXisaSystemCconstruct,andYisaPromelacodesnippet.Theinitiatorandthetargetsocketshavetobedeclaredandconstructedexplicitly.Thefollowingrule,Rule1,enablesthetransformationofsockets:Rule1: tlm_utils::simple_initiator_socketsocket|--chansimple_initiator_socket=[0]of{mtype,trans}NoticethatwemodelthesocketsassynchronouschannelsinPromela,sincethetransmissionofatransactionfromaninitiatortoatargetcanbeconceivedasanaccesstoamemory-mappedbussystem.Thisisdonesynchronouslyandneednottobebuffered.Rule2transformsthedeclarationofaSystemCthreadtoaproctypeinPromelaasfollows:Rule2: SC_THREAD(thread_process)|--proctypethread_process()Moreover,thegenericpayloadhasastandardsetofbusattributes:command,address,data,byteenables,streamingwidth,andresponsestatus.Aftersettingtheattributes,thegenericpayloadispassedthroughthesocketsbetweentheinitiatorandthetarget.Rule3transformsthedeclarationofthegenericpayloadinaSystemCTLMprogramtoPromela.NotethatintheSystemCpartofthisrule,transisapointeroftypetlmgenericpayload.Rule3: tlm::tlm_generic_payload*trans=newtlm::tlm_generic_payload;43|--typedeftrans{tlm_commandcmd;intaddress; intdata_ptr; intdata_length; intstreaming_width; bytebyte_enable_ptr; booldmi_allowed; tlm_responseresponse_status};Ontheright-handside,transisde nedasastructureinPromela,wheretheaddressattributeisthelowestaddressvaluefrom/towhichdataistobereadorwritten,thedataptrattributepointstoadatabufferwithintheinitiator,thedatalengthattributegivesthelengthofthedataarrayinbytes,thestreamingwidthattributespeci esthewidthofastreamingburstwheretheaddressrepeatsitself,andthesetdmiallowedmethodisusedtoindicatetotheinitiatorthatitcanusethedirectmemoryinterfacefordatatransfer.ATLMcommandiseitheraTLMreadcommandorTLMwritecommandoraTLMignorecommand.Thus,wemodelitwiththeRule4,whereeachTLMcommandisde nedasastructureinPromela:Rule4: tlm::tlm_commandcmd=static_cast|--typedeftlm_command{bitcmd[2];};Furthermore,aTLMresponsecouldhavesevendifferentvalues.Tocoverallthesesevenvaluesinthetransformedprogram,wepresentRule5thatde nesastructurefortheTLMresponse.We44encodethesevaluesinthethreebitsoftheresponsearray.Rule5: TLM_OK_response=1, TLM_incomplete_response=0, TLM_generic_erro_response=-1, TLM_arrdess_error_response=-2, TLM_command_error_Response=-3, TLM_burst_error_response=-4, TLM_byre_enable_error_response=-5|--typedeftlm_response{bitresponse[3];};Rule6transformsaforwardsubmissionofatransactiontoamessagetransmissioninasocketchannelinPromela.Rule6: socket->b_transport(*trans,delay)|--simple_initiator_socket!t;tisatransactionoftypetransthatissenttothechannelsimleinitiatorsocket.4.4CaseStudy1:ExtractingPromelaModel Inthissection,weextractthePromelamodeloftheSystemCTLMprogramexplainedinFig-ure2.4.TheextractedPromelamodelMincludestwoproctypesnamedInitiatorandTarget(seeFigure4.1).Moreover,weconsideraseparateproctypetomodelincModEight.ToenablecommunicationbetweentheInitiatorandtheTargetmodulesinthemodelM,wedeclareasyn-chronouschanneltgtIfPort(seeFigure4.1).Tostartatransaction,theInitiatorsendsthemessage45startTranstotheTargetviatgtIfPortchannelandwaitsuntiltheTargetsignalstheendofthetransactionwithamessageendTrans.ThePromelacodeinFigure4.1capturesthespeci cationofchannelsandtheInitiator,TargetandincModEightproctypes.TheincModEightproctypemodelstheBehaviorprocessoftheTarget.ThemtypeinFigure4.1de nesanenumerationonthetypesofmessagesthatcanbeex-changedinthesynchronouscommunicationchannelsif2TgtBehandtgtIfPort.TheInitiatorandtheTargetareconnectedbythechanneltgtIfPortandtheTargetisconnectedtoitsBehaviorproctype(i.e.,incModEight)viathechannelif2TgtBeh.Initially,theInitiatorsendsastartTransmessagetotheTarget.UponreceivingstartTrans,theTargetsendsthemessageinctoincMod-Eighttoincrementthevalueofdmodulo8.TheincModEightproctypesendsincComplttoTargetafterincrementingd.Correspondingly,theTargetproctypesendsaendTransbacktotheInitiatorindicatingtheendofthetransaction.4.4.1CapturingtheexecutionsemanticsofthesimulationkernelNotethat,wehavenotexplicitlymodeledtheschedulerandthewayitwouldrunthisprogramhasbeenimplicitlycapturedbythewaywemodelthewait()statement.Sincethesimulationkernelhasarun-to-completionschedulingpolicy,athread/processcannotbeinterrupteduntilitiseitherterminatedorwaitsforanevent.TherearetwothreadsintheprogramofFigure2.4:onethatisassociatedwiththemethodinitiate()oftheinitiatorclass(seeLine11inFigure2.4)andtheotherimplementsthebodyoftheincModEight()methodofthetargetclass(seeLine24inFigure2.4).The rststatementoftheincModEight()methodisawait()statementonadeltanoti cationeventbecauseinLine27ofFigure2.4thenotify()methodisinvokedontheSCZEROTIMEevent.Thus,initiallyonlytheinitiatorthreadcanexecute,whichincludesaninvocationofthetrigger()methodofthetargetclassviaaportintheinitiator(seeLine14inFigure2.4).Afterwards,461mtype=finc,incComplt,startTrans,endTransg//Messagetypes2chanif2TgtBeh=[0]offmtypeg//Declareasynchronouschannel3chantgtIfPort=[0]offmtypeg4byted=0;5intcnt=0;//usedtomodeltheoccurrenceoffaults6 7activeproctypeInitiator()f8byterecv;9waiting:tgtIfPort!startTrans;10tgtIfPort?recv;11initRecv=recv;//initRecvisusedtospecify12//desiredrequirements13ending:(recv==endTrans)->fin:skip;14g15 16activeproctypeTarget()f17byterecv;18waiting:tgtIfPort?recv;19tgtRecv=recv;//tgtRecvisusedtospecify20//desiredrequirements21starting:(recv==startTrans)->if2TgtBeh!inc;22if2TgtBeh?recv;23(recv==incComplt)->tgtIfPort!endTrans;g24 25activeproctypeIncModEight()f//ModelstheBehaviorprocess26//oftheTarget27byterecv;28waiting:if2TgtBeh?recv;29(recv==inc)->d=(d+1)%8;30if2TgtBeh!incComplt;gFigure4.1:Theextractedfunctionalmodel.theinitiatorthreadterminates.ThesimulationkernelcontextswitchestheTargetattheendofthecurrentsimulationcycleupontheoccurrenceofdeltanoti cation.WehavecapturedthissemanticsusingthesynchronouschannelsinthePromelamodel.Thatiswhywedonotexplicitlyhaveaproctypeformodelingthebehaviorsofthesimulationkernel.Ofcourse,thisdoesnotmeanthatsuchanapproachwouldworkforallSystemCprograms.Forexample,inmodelswhereprocessesaretriggeredbytime-outs,weneedtoexplicitlymodelthebehaviorsoftheschedulerintheTimedNoti cationphasewhensensitiveprocessesareaddedtothesetofrunnableprocesses.474.4.2PropertySpecicationandFunctionalCorrectness InordertoensurethattheextractedmodelcorrectlycapturestherequirementsoftheSystemCprogram,wede neasetofmacrosthatweusetospecifydesiredrequirements/properties.WeonlyconsidertherequirementsrelatedtothecommunicationbetweentheInitiatorandtheTarget.TheSystemCprogramofFigure2.4hastwotypesofrequirements.First,oncetheInitiatorstartsatransaction,thenthattransactionshouldeventuallybecompleted.Second,itisalwaysthecasethatiftheInitiatorreceivesamessagefromtheTargetafterinstantiatingatransaction,thenthatmessageisanendTransmessage.Moreover,iftheTargetreceivesamessage,thenthatisastartTransmessage.Sincethesecondrequirementshouldalwaysbetrueintheabsenceoffaults,itde nesaninvariantconditiononthetransactionbetweentheInitiatorandtheTarget(denotedbytheinvmacrobelow).ToformallyspecifyandverifythesepropertiesinSPIN[48],we rstde nethefollowingmacrosintheextractedPromelamodel.#definestrtTrinitiator@waiting #defineendTrinitiator@fin #definefinish(initRecv==endTrans) #definestart(tgtRecv==startTrans) #defineinitEndinitiator@ending #definetgtStarttargetTrigger@starting #defineinv((!initEnd||finish)&&(!tgtStart||start))ThemacrostrtTristrueifandonlyifthecontrolofexecutionoftheInitiatorisatthelabelwaiting(seeFigure4.1).Likewise,themacroendTrcapturesstateswheretheInitiatorisatthelabel n.Usingthesetwomacros,wespecifythe rstrequirementasthetemporallogicexpression(strtTr)endTr),whichmeansitisalwaysthecase(denotedby)thatiftheInitiatoriswaiting(i.e.,hasstartedatransaction),thenitwilleventually(denotedby)reachthelabel n48(seeLine13inFigure4.1);i.e., nishthetransaction.Wespecifytheinvariantpropertyastheexpressioninv.Thispropertyrequiresthatinvisalwaystrue(intheabsenceoffaults).UsingSPIN,wehaveveri edtheabovepropertiesfortheextractedmodelofFigure4.1.4.5CaseStudy2:ExtractingPromelaModelusingTransfor-mationRulesInordertoextractaPromelamodelfromtheSystemCTLMprogramofSection2.2(Figures2.5and2.6),weusethesameideasexplainedinSection4.4.Moreover,weusethesetoftransforma-tionrulesofSection4.3,whichhelpsustomodelinteroperability.TheextractedPromelamodelMhastwoproctypesnamedInitiator(Lines16-44inFigure4.2)andMemory(Lines46-73inFigure4.3).ToenablecommunicationbetweentheInitiatorandtheMemoryinthemodelM,weuseRule1ofthetransformationrulestodeclareasynchronouschannelsimpleinitiatorsocket(seeFigure4.2).ThebindingoftheinitiatorandthetargetsocketsinLine72ofFigure2.6iscapturedasachannelinthePromelamodel(Line12inFigure4.2).Asaresult,inthePromelamodel,wedonotexplicitlygenerateanythingcorrespondingtothetargetsocketintheMemorymodule.WemodeltheactualmemorybyanarrayofbytesinLine14ofFigure4.2.UsingRule3,theinitiatorcreatesatransactionbysettingtheattributesofthegenericpayload(Lines21-27inFigure4.2).Notethat,dataptrisapointerintheSystemCprogram,whereasinthePromelamodelwetreatitastheactualdatathatshouldberead/written.SincewecannotusepointersinPromela(unlessweuseccodeblockswhichcomplicatesthemodel),weusedataptrastheactualdata.Fromthepointofviewofmodeling,ifwecouldmodelpointersinPromela,allwewoulddowastoaccessthememorycontents.Thatiswhywetreatdataptrastheactualdatavalue.After49settingtheattributesofthegenericpayload,theInitiatorsendsthemessageinitTtotheMemoryviasimpleinitiatorsocketchannel(Line28inFigure4.2)andwaitsuntiltheMemorysignalstheendofthetransactionwithamessagethatcontainsagenericpayloadwithresponsestatusattributebeingequalto1.Considerthat,tosendthemessageinitTviathesimpleinitiatorsocketchannel,weuseRule6totransformthebtransportmethodoftheTLMprogramtomodelM.TheInitiatormoduleinFigure4.2de nesarandomvalue,either0or1,forcmdattributetosendthemessageinitT(Lines22-23inFigure4.2).InordertodeclarethecmdattributeinthePromelamodelM,weuseRule4ofthesetoftransformationrules.Whenthecmdis0,theInitiatorisrequestingareadcommand.Thus,theMemorymodule,aftercheckingaddressrangeandunsupportedfeatures,returnsthecontentsofthataddressinmemory(Line64inFigure4.3).WhenthecmdattributeofthemessagememTequals1,theInitiatorisrequestingawritecommand.Thus,theMemorywritesthevalueofdataptrattributeintothememorycellwhoseaddressequalstheaddressattributeofthereceivedmessagememT(Line65inFigure4.3).Afterreadingfrom/writingtothememorysuccessfully,theMemorymodulesetstheresponsestatuseattributeofmemTmessageto1(Line68inFigure4.3).Thismeans,accordingtothetransfor-mationRule5,theresponsestatusattributeequalsOK.Finally,theInitiator,afterreceivingOKresponse,completesthecurrenttransaction(Lines41-44inFigure4.2).501typedeftlm_responsefbitresponse[3];g;2typedeftlm_commandfbitcmd[2];g;3typedeftransftlm_commandcmd;4intaddress;5intdata_ptr;6intdata_length;7intstreaming_width;8bytebyte_enable_ptr;9booldmi_allowed;10tlm_responseresponse_status11g;12chansimple_initiator_socket=[0]oftrans;13intcnt=0;//usedtomodeltheoccurrenceoffaults14transinitT;transmemT;bytemem[255];15 16activeproctypeInitiator()f17tlm_responseres;18transrecv;19intsentData;intrecvData;20waiting:21if22::initT.cmd=0;initT.data_ptr=0;//read23::initT.cmd=1;initT.data_ptr=0;sentData=initT.data_ptr;//write24fi;25initT.address=0;initT.data_length=4;26initT.streaming_width=4;initT.byte_enable_ptr=0;27initT.dmi_allowed=false;initT.response_status=0;28simple_initiator_socket!initT;simple_initiator_socket?recv;29ending:30if31::(recv.response_status==-2)->32atomicfprintf("response_statusis:",recv.response_status);33gotowaiting;g34::else->skip;35fi;36if37::(initT.cmd==0)->recvData=recv.data_ptr;38::else->skip;39fi;40transComplete:41if42::(recv.response_status==1)->fin:skip;43::else->skip;44fi;gFigure4.2:TheInitiatormoduleoftheextractedfunctionalmodel.5146activeproctypeMemory()f47intdata;48boolfaultsOccur=false;49 50waiting:51simple_initiator_socket?memT;52 53starting:54if55::((memT.address>=256)||(memT.byte_enable_ptr!=0)56||(memT.data_length>4)||(memT.streaming_width<4))57->atomicfmemT.response_status=-2;58simple_initiator_socket!memT;59gotowaiting;g60::else->skip;61fi;62 63if64::(memT.cmd==0)->memT.data_ptr=mem[memT.address];65::(memT.cmd==1)->mem[memT.address]=memT.data_ptr;66fi;67 68memT.response_status=1;69data=mem[memT.address];70 71simple_initiator_socket!memT;72 73gFigure4.3:TheMemorymoduleoftheextractedfunctionalmodel.4.5.1PropertySpecicationandFunctionalCorrectness. ToensurethattheextractedmodelMcapturestherequirements/propertiesoftheTLMprogram,wespecifytherequirementsthatshouldholdintheabsenceoffaults.Forthispurpose,wede neamacrothatcapturestherequirementsrelatedtothereadandwriteactionsintheMemorymodule.InFigures2.5and2.6,iftheInitiatorreceivesamessagefromtheMemoryafterrequestingawritecommand,thesentdataoftheInitiatormustbethesameasthewrittendataintheMemorywhenthetransactioniscomplete.Inaddition,aftersendingareadcommand,thedataptrinthatmessageshouldbeequaltothereadvalueintheMemory.Weconsiderthispropertyasan52invariant,sinceitshouldbealwaystrueintheabsenceoffaults.Wede nethefollowingmacroandverifyitinSPIN[48].#defineinv1((!(Initiator@transComplete&&(initT.cmd==1))||(Initiator:sentData==Memory:data))&&(!(Initiator@transComplete&&(initT.cmd==0))||(Initiator:recvData==Memory:data)))ThisinvariantrepresentsthatwhentheexecutionisatthecompletelabeloftheInitiatorandwehaveawriteaction,thesentDataoftheInitiatorandwrittendataintheMemoryareequal.Likewise,whenwehaveareadaction,therecvDataintheInitiatorandthereaddatafromMemoryarethesameatthecompletelabelintheInitiator.Wespecifytheinvariantpropertyastheexpressioninv1.Thispropertyrequiresthatinv1isalwaystrue(intheabsenceoffaults).UsingSPIN,wehavemodelcheckedtheabovepropertiesfortheextractedmodelofFigures4.2and4.3. 4.6TransformationRulesforGeneratingUPPAALTimedAu-tomataInordertoextracttheUPPAALtimedautomatainLoosely-Timedcodingstyleprogramsusingbtransportinterface,weutilizetherulesfromSection4.3,whereasetoftransformationrulesisproposed.However,theserulesgenerateuntimedPromelamodelsfromuntimedSystemCTLMprograms,whileweneedtoextractUPPAALtimedautomatafromtimedTLMprograms.Hence,weutilizethefollowingrulessimilartothoseinSection4.3,wheretimedanduntimedmodelsare53thesame:Rule1:tlm_utils::simple_initiator_socketsocket;|-- chansimple_initiator_socket[0];Rule2:tlm::tlm_generic_payload*trans=newtlm::tlm_generic_payload;|-- typedefstruct{tlm_cmdcmd;intaddress;intdata_ptr; intdata_length;intstreaming_width; intbyte_enable_ptr;booldmi_allowed; tlm_responseresponse_status;}trans;Rule3:tlm::tlm_commandcmd=static_cast|-- typedef{bitcmd[2];}tlm_command;whereinatransformationruleXj Y,XisaSystemCTLMconstruct,andYisaUPPAALcodesnippet.Rule1enablesthetransformationofsockets.Rule2transformsthedeclarationofthegenericpayloadinaSystemCTLMprogramtoUPPAAL,andRule3transformsthedeclarationofaTLMcommand.InordertostudytimingbehaviorsofSystemCTLMprograms,wealsoneedtoconsidertimingconstraintsoftheprograms.Hence,weintroducenewrulesthatconsiderthesetimingconstraints.Rule4andRule5areintroducedforextractingtheUPPAALmodelinLTcodingstyle,i.e.,with54simple_initiator_socket!A2A1x >= delayFigure4.4:TransformingbtransportinterfaceintoUPPAAL,theInitiator.simple_initiator_socket?B2B1x>=delayFigure4.5:TransformingbtransportinterfaceintoUPPAAL,theTarget.btransportinterface.Inatransactionusingbtransportinterface,weneedtoconsiderthetimingsinceoneofthesendingargumentsisdelay.IfthetransactionisfromtheInitiatortotheTarget,thisargumentdescribesthepointoftimeinthefuturewherethecommunicationactuallystarts,andillustratestheendingtimeofthecommunicationintheresponse.TotransformabtransportinterfaceintoUPPAAL,wede neRule4,whereasynchronizationchannelsimpleinitiatorsocketisused(inFigures4.4and4.5)tosynchronizetheInitiatorandTargetofatransaction.Figures4.4and4.5illustratetheInitiatorandTargetofthetransactionrespectively.Thecommunicationstartsatdelaytimingpoint.Hence,theInitiatordoesnotsynchronizewiththeTargetbeforethattime.Wetakethisconstraintintoaccountbyde ningtheguardx>=delayattheInitiator,wherexshowsthecurrentsimulationtimesctimestamp().Inaddition,theTargetacceptsthesynchronizationafterthedelaytimingpoint.Weconsiderthisconstraintbyde ningtheguardx>=delayattheTarget.Itmeansthecommunicationstartsafterdelaytimingpoint.Rule4:socket->b_transport(*trans,delay)|-- Figures4.4and4.5Moreover,inordertoguaranteedeterministicexecutionandincreasethetimingaccuracy,aSystemCTLMprogramthatusesLoosely-Timedcodingstylebene tsfromexplicitsynchroniza-tionpointsbyutilizingcallstowait()function.Thisfunctionisasynchronization-on-demand55methodthatyieldsthecontroltotheSystemCscheduler.TotransformthisfunctionintotheUP-PAALmodel,wede neavariableglobal-clockthatplaystheroleoftheglobaltimeinaSystemCTLMprogram.TotransformthewaitfunctionintotheUPPAALmodel,wede neRule5asfollows:Rule5:wait(x)|-- global-clock=global-clock+x;x=0;Hence,whenthewaitfunctioniscalled,weaddthedelayargumentsobtainedfromRule4totheglobal-clockvariableandresetthelocalclockx.4.7CaseStudy3:ExtractingUPPAALModelusingTransfor-mationRulesInthisexample,weextendtheexampleexplainedinSection2.2tohavethreemodules:Initiator,Router,andMemory.TheInitiatormodulegeneratesatransactionwhiletheMemory(target)modulerepresentsarandomaccessmemory.TheRouterisaTLM2.0interconnectcomponentthatisplacedbetweentheInitiatorandtheMemory.Aninterconnectcomponentisacomponentthatforwardstransactionsfromanincomingtargetsockettoanoutgoinginitiatorsocket(seeFigure4.6forthearchitecture).Inthisexample,theinitiatorsocketoftheInitiatormoduleisboundtothetargetsocketoftheRouterandtheinitiatorsocketoftheRouterisboundtothetargetsocketoftheMemorymodule.TheInitiatorhasathreadprocess(similartothatinFigure2.5)thatstartsthecommunicationbysendingagenericpayloadalongwithadelayparametertotheRouter.TheRouterutilizesitstargetsocketandthebtransportinterfacetoreceivethetransactionfrom56Figure4.6:Thearchitectureofthememory-mappedbussesmodel.theInitiator.Afterdecodingtheaddress,ifitisneeded,theRouterforwardsthetransactiontotheMemory.Finally,theMemoryusesthebtransportinterfacetoreceivethetransactionfromtheRouter.BasedontheInitiator™srequest,theMemoryeitherreadsfromorwritestothedataattributeofthegenericpayloadandsendsbackthecorrespondingresponse.WeusetherulesandapproachesexplainedinSection4.6toextracttheUPPAALtimedau-tomatamodel.Next,inFigures4.7,4.8,and4.9weidentifythefault-freeversionoftheprogramthatformsthebasisofmodelsgeneratedfortimingfaults.InextractedUPPAALmodels,thegreentextsshoweithertheguardsorsynchronization,thebluetextsshowtheupdates,andthepinktextsrepresentthenamesandinvariants.Figure4.7representstheInitiatormodelwiththestartingstateL1.WeutilizeRules2and3totransferthegenericpayloadandTLMcommand(read/write)intotheUPPAALtimedautomata.Hence,StatesL2andL3representplaceswherethecmdattributeshowswriteandreadcommandsrespectively.Aftergeneratingthetransaction,weuseRule1tode neasynchronizationchannelsendSocketbetweentheInitiatorandRouter,anduseRule4totransferbtransportinterfaceintotheUPPAALmodel.Asaresult,inFigure4.7,theInitiatorsynchronizesitselfwiththeRoutermoduleandchangesitsstatefromeitherL2orL3toL4.TheInitiatorcannotsendthetransactionlaterthandelay1timingpoint,sincethecommunicationactu-allystartsatthatpoint.InstateL6,theRouterreceivesthetransactionandchangesitsstatetoL7.Then,theRoutersynchronizeswiththeMemoryviatargetSocketchannelandchangesitsstatetoL8.Notethatthetransactionisnotactuallysentfromthechannel,sincethechannelsinUPPAALareonlyforsynchronizationpurposes.Then,weuseRules1and4totransferthebtransport57interfaceandtimingconstraintsintheMemory.Iftheguardx>=delayistrue,theMemoryreceivesthetransactionandchangesitsstatetoL11.TheMemorycannotsenditsresponselaterthandelay1+delay2,wheredelay2showsthedelayargumentoftheresponsemessagetotheInitiator.Afterexecutingthewriteorreadaction,ifthereisnoerror,theMemorychangesitsstatetoeitherL12orL13,andsynchronizesitselfwiththeRouterviatargetSocketchannel.TheRouter,receivestheresponsefromtheMemory,and,usingthesendSocketchannel,sendstheresponse.Finally,theInitiatorreceivestheresponseandcaninitiateanothertransaction.sendSocket?sendSocket!sendSocket!x = 0x = 0current = shared, RcvdData = shared.datashared = currentshared = current, SentData = current.datadata =-1, setTrans(current,readCmd,0, data,4,4,0,false, inComplete)data =5, setTrans(current,writeCmd, 0, data,4,4,0,false,inComplete)x <=delay1x <= delay1x<1errorL5L4L3L2L1current.response_status == responseErrorcurrent.response_status == responseOKx<=delay1+delay2x>=delay1x>=delay1Figure4.7:Fault-intolerantUPPAALtimedautomatamodeloftheInitiatormodule.sendSocket!targetSocket?targetSocket!sendSocket?L9L8L7L6Figure4.8:Fault-intolerantUPPAALtimedautomatamodeloftheRoutermodule.58targetSocket!targetSocket!targetSocket!targetSocket?mem[shared.address] = shared.data, shared.response_status=responseOK, RcvdData=shared.data shared.data = mem[shared.address], shared.response_status =responseOK, SentData=mem[shared.address]GetInfo()x<=delay1+delay2x<=delay1+delay2x>=delay1L13L12errorL11L10x<=delay1+delay2x<=delay1+delay2cmd == writeCmd cmd==readCmdaddress >=outOfBound|| data_length >4 || streaming_width <4|| byte_enable_ptr !=0|| cmd>1x>=delay1Figure4.9:Fault-intolerantUPPAALtimedautomatamodeloftheMemorymodule.4.7.1PropertySpecicationandFunctionalCorrectness Toensurethattheextractedtimedautomatamodelcapturestherequirements/propertiesoftheSystemCTLMprogram,wespecifytherequirementsthatshouldholdintheabsenceoffaults.Forthispurpose,wede nethefollowingspeci cationsinasubsetofCTL(ComputationalTreeLogic)inFigure4.10thatcapturestherequirementsrelatedtothetimingconstraints.Theserequirementsshouldbealwaystrueintheabsenceoffaults.SPEC1:A[]notdeadlock SPEC2:Init.L1-->(Init.L4andx>=delay1) SPEC3:Init.L1-->(Memory.L11andx>=delay1) SPEC4:(Memory.L12orMemory.L13)-->(Init.L5andx<=delay1+delay2)SPEC5:Init.L1-->(Init.L5andx<=delay1+delay2)Figure4.10:RequirementsofMemoryBusSystemusingLTcodingstyle.The rstrequirementSPEC1representsthattheextractedmodelisfreeofdeadlock.ThesecondrequirementSPEC2illustratesthattheInitiatormodulewillnotsendthetransactiontowardstheMemorymodulebeforethetimingpointdelay1.TheSPEC3showsthatiftheInitiatorsendsatransaction,theMemorywillnotreceiveitbeforethetimingpointdelay1.Also59iftheMemorysendstheresponsetotheInitiator,itshouldnotbereceivedafterthetimingpointdelay1+delay2.ThisrequirementisrepresentedinSPEC4.Finally,theSPEC5showsthatiftheInitiatorstartsatransaction,itshouldnotbe nishedafterthetimingpointdelay1+delay2.UsingUPPAAL,wehavemodelcheckedtheabovepropertiesfortheextractedmodelofFigures4.7,4.8,and4.9. 4.8CaseStudy4:ExtractingUPPAALModelofaNoCSwitch Inthisexample,weextendtheexampleexplainedinSection2.2tomodelaNetworkonChipswitch.Weassumethattheswitchhaseightprocessingcoresthatcommunicateusingarouter.Tomodelthisswitch,weassumewehavememorymappedbusseswithfourInitiatorsandfourTargetsandaRouterasaninterconnectcomponentbetweentheInitiatorsandTargets(SeeFigure4.11).EachInitiatormodulegeneratesatransactionandsendsittooneoftheTargetmodulesthroughtheRouterusingbtransportinterface.TheRouterreceivesatransaction,decodestheaddressattributeinthetransaction,andforwardsittotheappropriateTargetusingthedecodedaddress.TheRouteralsoneedstomanagethereturnpathfromtheTargetstotheInitiators.Inotherwords,theRouterisacomponentthatforwardstransactionsfromanincomingtargetsockettoanoutgoinginitiatorsocket.Inthisexample,therearefourincomingtargetsocketsconnectedtofourinstancesoftheInitiator,andfouroutgoinginitiatorsocketsconnectedtofourinstancesoftheTarget.SocketsbelongingtotheInitiatorsareboundtothetargetsocketsoftheRouter,andeachofthefourinitiatorsocketsbelongingtotheRouterisboundtoasocketbelongingtoadifferentTarget.Eachinitiator-to-targetsocketconnectionispoint-to-point.Weusethesetofrulesin4.6toextracttheUPPAALtimedautomatamodelfromtheSystemCTLMmodel.Next,inFigures4.12and4.13,weidentifythefault-freeversionofthismodel60Figure4.11:UsingLTcodingstyletomodelNoCswitch.thatformthebasisofmodelsgeneratedfordifferenttypesoffaults.TheextractedmodelsoftheInitiatorsandTargetsarethesameasthoseinSection4.5.AdrDecode?AdrDecode!Init2Router[InitID]!Router2Target[TargetID]?Router2Target[TargetID]!Init2Router[InitID]?L9L8L11L10L7L6x<=delay1+delay2x>=delay1Figure4.12:TheRoutermodule.Figure4.12representstheRouterautomatonandFigure4.13showstheaddressdecodingmechanismusedintheRoutermodule.TheRouterreceivesatransactionthroughoneofthechannelsInit2RouterandchangesitsstatetoL7.Thistransactionshouldnotbereceivedbeforedelay1timingpoint.NotethatintheRouterautomaton,wecannotusethesamechanneltocom-municatewithInitiatorssincetheirsocketconnectionsarepoint-to-pointintheSystemCTLM61AdrDecode!AdrDecode?shared.address = shared.address - TargetSize, TargetID = TargetID + 1L13L12shared.address > TargetSizeshared.address < TargetSizeFigure4.13:Theaddressdecodingmechanism.model.Afterreceivingthetransaction,theRouterdecodestheaddress(LocationsL12andL13inFigure4.13),obtainstheTargetID,andforwardsthetransactiontotheappropriateTarget.TheRouterthenwaitstoreceivetheresponseoftheTargetfromthesamechannel(L10)andsendsitbacktotheappropriateInitiator(L11).4.8.1PropertySpecicationandFunctionalCorrectness Toensurethattheextractedmodelcapturestherequirements/propertiesoftheSystemCTLMprogram,wespecifythepropertiesthatshouldholdintheabsenceoffaults.Forthispurpose,wede nethefollowingCTL(ComputationalTreeLogic)speci cationsinFigure4.14.SPEC1:A[]notdeadlock SPEC2:Init[id_i].CurrTrans.cmd==readCmd-->(Target[id_t].SentData==Router.RcvdData) and (Router.SentData==Init[id_i].RcvdData)SPEC3:Init[id_i].CurrTrans.cmd==writeCmd-->(Init[id_i].SentData==Router.RcvdData) and (Router.SentData==Target[id_t].RcvdData)SPEC4:Init[id_i].L1-->(Init[id_i].L2)or(Init[id_i].L3)SPEC5:(Init[id_i].L2)or(Init[id_i].L3)-->Init[id_i].L1Figure4.14:PropertiesoftheextractedUPPAALtimedautomata.ThecorrectnessofrequirementSPEC1inFigure4.14impliesthatinallpathsoftheextractedautomatamodel,wedonothaveanydeadlock.TherequirementsSPEC2andSPEC3repre-62sentthatthecommunicateddatabetweentheInitiatorandRouter,andtheRouterandTargetarethesameintheabsenceoffaults.TheSPEC4andSPEC5showthattheInitiatorwilleven-tuallygenerateatransactioneitherwithawriterequest(LocationL2)orareadrequest(LocationL3),andwilleventuallycomebacktotheinitialstatetogenerateanothertransaction.ThesetworequirementstogetherimplythattheInitiatormoduleisnotblocked.Wecanextendthesetofrequirementsandde nethesamerequirementsasSPEC4andSPEC5forallmodulesintheex-tractedmodel.UsingUPPAALmodelchecker,wehavemodelcheckedtherequirementsofFigure4.14. 4.9UsingSTATEforExtractingTimedAutomataModels InordertoconsiderconcurrencyinSystemCTLMprograms,weneedtoutilizeApproximately-Timedcodingstyle.AnApproximately-Timedmodelbreaksdowntransactionsintoanumberofphasescorrespondingmuchmorecloselytothephasingofparticularhardwareprotocols(e.g.,theaddressanddataphasesofanAHB(AMBAAdvancedHigh-performanceBus)readorwrite).Onthecontrary,aLoosely-Timedmodel,forwhichweproposedourtransformationrulesinSection4.6,utilizestransactionscorrespondingtoacompletereadorwriteacrossabusornetworkinphysicalhardware.Itprovidestimingattheleveloftheindividualtransaction.Also,inthemodelextractionproposedinSection4.6,theSystemCschedulerhasbeenmodeledimplicitly.Inotherwords,thewaytheextractedmodelwouldruntheSystemCprogramisimplicitlycapturedbythewaywemodelthewait()statement.Sincethesimulationkernelhasarun-to-completionschedulingpolicy,athread/processcannotbeinterrupteduntilitiseitherterminatedorwaitsforanevent.Ontheotherhand,forApproximately-Timedmodels,weneedtomodeltheSystemCschedulerexplicitlytobeabletomanageconcurrenttransactions.Inaddition,itisnecessarytoconsider63otherSystemCelementsaswellasTLMcomponents,e.g.events,wait-notifymechanism,andPayloadEventQueue(PEQ),inthemodelextraction.Forthispurpose,weuseSTATE(SystemCtoTimedAutomataTransformationEngine)tool-set[47]totransformaSystemCTLMprogramtoitsequivalentUPPAALtimedautomatamodel.Inthefollowing,we, rst,stateafewassumptionsthatde nesthesubsetofSystemCTLMprogramssupportedbySTATE.Then,werepresentthetimedautomatatemplatesthatSTATEextractsfordifferentSystemCTLMelements.Thematerialsinthefollowingsectionsaremostlyadaptedfrom[47]. 4.9.1Assumptions SystemCsupportsaverydiversesetofmodelsofcomputation.Atthesametime,asanextensionofC++,itinheritsthefullsemanticscaleoftheC++language.Together,thisillustratesthatSystemCisanoutstandinglyexpressivelanguages.TomakeitnonethelesspossibletotransformSystemCdesignsintothemorerestrictedUPPAALmodelinglanguage.Therefore,toutilizeSTATE,weneedtoassumethatagivenSystemCdesignful llsthefollowingrestrictions.UPPAALsupportsnodynamicvariableorprocesscreation.Thus,dynamicobjectorprocesscreationarealsoforbiddenintheSystemCdesign,i.e.,astaticstructureisrequired.ThisisaminorrestrictionbecausedynamicprocesscreationisnotapartofSystemClanguagede nitionandcanonlybeusedthroughthecorrespondingC++functions.Asaconsequence,onlyinstantiationsandinitializationsareallowedinconstructorsandinthescmainmethod.WhileSystemCallowshierarchicalscopes,thepossibilitytode nescopesislimitedtoglobalandlocalvariablesinUPPAAL.Toavoidnamecon!icts,weassumethatnovari-ableisshadowed(i.e.,eachvariablehasauniqueidenti erinitsscope).Itisneededtoassumethatnooverloadingofmethodsisused.Thisassumptionaswellastheprevious64assumptiondonotrestrictthesetofpossibleinputdesignsbutrequiresomerenamingandcodeduplicationatthemost.TheUPPAALmodelinglanguageonlyprovidesthedatatypesintandbool.Mostcomplexdatatypescanbemappedintointegers,buttheuseofpointersisgenerallyimpossibleinUPPAAL.Thus,weneedtoassumethattheSystemCdesigndoesnotuseanypointers.Asaconsequence,dynamicmemorymanagementisalsoexcluded.4.9.2RepresentationofSystemCTLMDesignsinUPPAAL ThegeneralideaofrepresentingaSystemCTLMprograminUPPAALtimedautomataisthateachmethodismappedtoasingletimedautomatatemplate.Processautomataareusedtoencapsulatethesemethodsandcarefortheinteractionswitheventsandthescheduler(seeFigure4.15).Theschedulerisexplicitlymodeledandaprede nedtemplateisusedforeventsandotherSystemCconstructssuchasprimitivechannels.Theinteractionsbetweentheprocessesandthescheduleraremodeledbytwosynchronizationchannels,activateanddeactivate.Theinteractionsbetweenprocessesandeventobjectsaremodeledbywaitandnotify.Theinteractionsbetweentheeventobjectsandtheschedulerareusedtosynchronizetheirtiming.Theschedulerinformstheeventobjectswhenadelta-cycleiscompletedtoreleasedelta-delaynoti cations,andconversely,theeventobjectsinformtheschedulerwhentimeisadvancedduetoatimednoti cation.Inthefollowing,weexplainthetimedautomatatemplatesthatSTATEgenerateforeachoftheSystemCstructuresinFigure4.15.TheseautomataareneededinanApproximately-Timedmodeltoprovideconcurrency.65Figure4.15:RepresentationofSystemCTLMDesignsinUPPAAL.Figure4.16:TimedautomatamodelingSystemCscheduler[47].4.9.2.1TheScheduler TheschedulercontrolstheexecutionofSystemCdesigns.Thebasicexecutionunitsareprocesses.Theschedulerworksindelta-cycles,i.e.,inevaluateandupdatephases.Intheevaluatephase,pro-cessesthatarereadytorunareexecutedinnon-deterministicorder.Intheupdatephase,primitivechannelsareupdatedbytakingovernewvalues.Iftherearenomoreprocessesreadytorunwhenadelta-cycleis nished,timeisadvancedtothenextpendingeventThetimedautomatonthatSTATEgeneratesfortheschedulerisshowninFigure4.16.Ini-66tializationisimplicitinUPPAAL,i.e.,processesandmethodsareexecutedoncebeforethemainsimulationloop.Asaconsequence,theschedulerstartsintheevaluationphasedepictedbythelocationevaluate.Ifthereareanyprocessesthatarereadytorun,theschedulersendsanactiva-tioneventactivate!.Processesthatarereadytorunreceivethiseventandresumetheirexecution.STATEusesabinarychannelfortheactivationtoensurethatonlyoneprocessisexecutedatatimeandthatprocessesareexecutedinanon-deterministicorder.Toensurethattheschedulersendstheactivationeventonceforeachprocessthatisreadytorun,eachprocessincrementsacounterreadyprocswhentriggered,anddecrementsthecounterwhensuspendingitself.Whentherearenomoreprocessesthatarereadytorun,i.e.,readyprocs==0,theschedulerstartstheupdatephasebygoingtolocationupdate.Intheupdatephase,updaterequestsareexecutedinnon-deterministicorderusingtheactiva-tioneventupdatestart.Immediatenoti cationisnotallowedduringtheupdatephase.Iftherearenomoreupdaterequests,theschedulerstartsthenextdelta-cycle(seelocationnextdeltainFigure4.16).Whenleavingtheupdatephase,theschedulerinformseventobjectswithpendingdelta-delaynoti cationsthatadelta-cycleis nishedbysendingdeltadelay!.Iftherearedelta-delaynoti cations,thecorrespondingprocessesareimmediatelytriggeredandbecomereadytorun.Theywillbeexecutedinthenextdelta-cycle,whichisstartedbytheschedulerwithouttimeprogress.Iftherearenoprocessestriggeredbydelta-delaynoti cations,i.e.,readyprocs==0,simulationtimemustbeadvancedtotheearliestpendingtimednoti cation.Therearetwotypesoftimednoti cationsinSystemC:eventsmaybenoti edwithadelaybycallinge.notify(t),andprocessesmaybedelayedforagiventimeintervalbycallingwait(t).InSystemC,thetimingbehavioriscompletelymanagedbythescheduler.Inthetimedautomaton,wehavethepossibilitytowaitlocallyforagiventime.Therefore,itismoresuitabletomodeltimewithinprocessesandeventobjects.Towaitfortheearliestpendingtimednoti cationinthe67scheduler,STATEletstheprocessesandeventswithtimedbehaviorsendabroadcastsynchroniza-tionadvancetime!whentheirdelayexpires.Theschedulerreceivesadvancetime?andstartsanewdelta-cycle,i.e.,executesprocessesthatbecamereadytorunthroughthetimednoti cation.ThetimedautomatonmodelingtheschedulerbehavesexactlyliketheSystemCscheduler.ThebinarychannelsusedtocontrolprocessexecutionandchannelupdatesguaranteethatUPPAALmodelcheckerconsiderseverypossibleserialization.Thelocationsusedfortheexecutionofdelta-cyclesareurgentandthustakenosimulationtime.Itisensuredthatnoschedulingphaseisstartedbeforetheprecedingphaseiscompletedusingthecountersreadyprocsandupdateprocsandcommittedlocationsineventnoti cations.Thecountersguaranteethatpendingexecutionsarecompletedbeforethenextphaseisstarted.Theuseofcommittedlocationsineventnoti cation(whichisrepresentedinFigure4.17)ensuresthateventtriggeringisprioritizedoverstatechangesinthescheduler. 4.9.2.2Events Ifaneventobjecteisnoti edbyitsowner,processesthataresensitivetotheeventresumeexecu-tion.SystemCsupportsthreetypesofeventnoti cations.Animmediatenoti cation,invokedbye.notify(),causesprocessestobetriggeredimmediatelyinthecurrentdeltacycle.Adelta-delaynoti cation,invokedbye.notify(0),causesprocessestobetriggeredatthesametimeinstant,butafterupdatingprimitivechannels,i.e.,inthenextdelta-cycle.Atimednoti cation,invokedbye.notify(t)witht>0,causesprocessestobetriggeredafteracertaindelayt.Ifaneventisnoti edthatalreadyhasapendingnoti cation,onlythenoti cationwiththeearliestexpirationtimetakeseffect.Thatmeansthatimmediatenoti cationsoverrideallpendingnoti cations,delta-delaynoti- cationsoverridetimednoti cations,andtimednoti cationsoverridependingtimednoti cationsiftheirdelayexpiresearlier.68Figure4.17:Timedautomatatemplateforaneventobject[47].ThemodelingofeventobjectsarerepresentedinFigure4.17[47].Thetimedautomatatem-plateisinstantiatedforeacheventobjectdeclaredinagivenSystemCdesign.Itstemplatepa-rametersarethesynchronizationchannelsnotifyimm,notifyandwait,andtheintegervariablet.Initially,theeventjustwaitstobenoti ed.Ifitisimmediatelynoti ed,itreceivesnotifyimm?,andimmediatelysendswait!onabroadcastchannel.Iftheeventobjectisnoti edbyadelta-delayoratimednoti cation,itreceivesnotify?andcopiestheparameterttoalocalvariablendelay,whichyieldsthenoti cationdelay.Atthesametime,alocalclockxisreset.Thecommittedlocationthatisnowreachedisusedtoreinitializendelayandtoresetxifasubsequentdelta-delayortimednoti cationoverridesthenoti cationdelay.Wethenhavetowaituntil:animmediatenoti cationoverridesthecurrentpendingnoti cation,wereceivedeltadelay?fromtheschedulerifndelay==0,orthecurrentdelayexpires,i.e.,x==ndelay&&ndelay!=0.Subsequently,wesendwait!andgobacktotheinitiallocation.Whenatimednoti cationex-pires,wehavetoinformtheschedulertostartthenextevaluationphasebysendingadvancetime!.69Duetotheuseofabroadcastchanneladvancetime!,onlythe rstadvancetimeisreceivedbytheschedulerifthedelaysofmultipleeventsexpireatthesametime.4.9.2.3Processes ProcessesarethebasicexecutionunitinSystemC.Eachprocessisassociatedwithamethodtobeexecuted.Therearetwotypesofprocesses:methodprocessesandthreadprocesses.Amethodprocess,whentriggered,alwaysexecutesitsmethodbodyfromthebeginningtotheend.Itistriggeredbyasetofeventsgiveninastaticsensitivitylist.ThetimedautomatatemplateSTATEusestowrapamethodprocessisinFigure4.18.Itwaitsforanyoftheeventsfromthesensitivitylistbysynchronizingonsensitive?.Ifoneoftheeventsfromthesensitivitylistoccurs,itmarksitselfasreadytorunbyincrementingreadyprocsandbywaitingfortheactivateevent.Then,ittransferscontroltoitsassociatedmethod.Whenthemethodreturns,itdeactivatesitselfbysendingdeactivate!totheschedulerandbydecrementingreadyprocs.Then,itreturnstotheinitialpositionandwaitsuntilitistriggeredbyoneoftheeventsfromthesensitivitylistagain.Figure4.18:Methodprocesstemplate[47].Athreadprocessmaysuspenditsexecutionanddynamicallywaitforeventsoragiventimedelay.Itistriggeredonlyonceatthebeginningofthesimulationandrunsautonomouslyfromthattimeon.ThetimedautomatatemplateSTATEusestostartathreadprocessisgiveninFigure4.19.70Itjustwaitstobeactivated,transferscontrol!owtoitsassociatedmethodanddeactivatesitselfifthemethodreturns.Notethatthecontroltransferchannelisaparameteroftheprocesstemplates,andthusthesametemplatecanbeinstantiatedforarbitrarymanyprocessdeclarations.Figure4.19:Threadprocesstemplate[47].4.9.2.4PayloadEventQueue(PEQ) APEQisatime-orderedlistofeventnoti cations,whereeachnoti cationisassociatedwithatransactionobject(i.e.,apayloadandaphase)andadelay.Theactualdelayofeacheventnoti cationiscalculatedfromthecurrentsimulationtimeandtheannotateddelay.ThePEQisconnectedtoacallbackmethodpeqcb,whichisexecutedwheneveranoti cationinthePEQexpires.APEQcanbeusedbycallingitsnotifymethodwithatransactionobjecttandadelayd.ThiswillcausethecallbackmethodassociatedwiththePEQtobeexecutedwithtindtimeunits.STATEmodelsthePEQwithfourdifferenttimedautomata,namelytimed-orderedlist(Figure4.20),interface(Figure4.21),eventfetchandcallbackinvocation(Figure4.22),andPEQeventautomata(Figure4.23).The rstautomatonisanordered-listwheretuplesofapayload,adelayandaphasecanbestoredandsortedbytheirdelayexpirationtime.TheinterfaceautomatoniscalledbyinitiatorsandtargetstoinsertanewPEQnoti cation.Thethirdautomatonremoves71Figure4.20:Timedautomatatemplateofthetimedorderedlist[47].Figure4.21:TimedautomatatemplateofPEQinterfacemethodnotify[47].elementsfromthePEQiftheirdelayexpiresandinvokesthecallbackmethodassociatedwiththePEQ(peqcb).Thelastautomatonmodelstheeventobjectnoti cation.Figure4.22:TimedautomatatemplateoftheautomatonthatprocessesPEQelements[47].72Figure4.23:TimedautomatamodelofthePEQevents[47].4.10CaseStudy5:ExtractingUPPAALModelinATCodingStyleInthissection,wepresentacasestudythatfocusesonanon-chipmemory-mappedcommunicationbusesbetweenanInitiatorandaMemorymodule.ThiscasestudyutilizesApproximately-Timed(AT)codingstyleandTLMbaseprotocol.WeutilizeSTATEtool-settoextractatimedautomatamodelfromthegivenSystemCTLMprogram.Inthiscasestudy,adaptedfrom[1],theInitiatorandtheMemoryusenon-blockingtrans-port(nbtrasport)interfaceforinteraction.ThenbtransportinterfaceisintendedtosupporttheATcodingstyleandisparticularlysuitedformodelingpipelinedtransactions.Itbreaksdowneachtransactionintofourphases,namelyBEGINREQ,ENDREQ,BEGINRESP,andENDRESP,whereeachphasetransitionisassociatedwithatimingpoint(seeFigure4.24).TheInitiatorgeneratesatransactionandstartsthecommunicationbysendingaBEGINREQusingtheforwardpathnbtransportfwtotheMemoryandwaitstoreceiveENDREQorBE-GINRESPfromthebackwardpathnbtransportbw.Afterthat,theInitiatorcan nishthe73Figure4.24:Non-blockingtransportinterfacearchitecture.transactionbysendingENDRESP.TheInitiatorcanalsostartanothertransactionbysendinganewBEGINREQ.Notethatduringthe rsttwophaseswecannothavepipelinedtransactions.Inotherwords,thereisatmostoneBEGINREQpendinginthesystem,whilewecanhavemultipletransactionswithBEGINRESPphasespendinginthesystem.Inthisexample,duringanalysis,werestrictthenumberofpipelinedtransactionsbytwo.Eachtransactioninannbtrasportinterfacehasthreearguments:genericpayload,delay,andphase.Thegenericpayloadisthetransactionobjectbeingsent.Thedelayrepresentsthetimingannotationofthecommunication.Thephase,whichisanewargumentinnbtransport,indicatesthestateofthetransaction,e.g.,BEGINREQforstartingatransaction,andreturnsanenumerationvaluetoindicatewhetherthereturnfromthefunctionalsorepresentsaphasetransition.WeutilizeSTATEtool-set,explainedinSection4.9toextracttheUPPAALtimedautomatamodel.Nonetheless,theUPPAALmodelgeneratedbyconsideringallpossiblecomponentsistoolargetoperformexhaustiveanalysis.Hence,forevaluatingthemodel,weneedtoutilizemodelslicingtechniquestoonlyconsidercomponentsthatareimportantforverifyingtheprop-74erty/requirementofinterest.ToensurethattheextractedmodelcapturestherequirementsoftheSystemCTLMmodel,wespecifyasetofrequirementsthatshouldholdintheabsenceoffaults.Wedividetheserequirementsintotwocategories:1)whentimingconstraintsarenotimportantandwewanttoensurethatmessage,permanent,andtransientfaultsdonotperturbthemodel,and2)whentrainingconstrainsarebeingveri edtoensurethattimingfaultsdonotperturbthemodel.Theserequirementsshouldbealwaystrueintheabsenceoffaults(SeeFigures4.25and4.26).SPEC1:A[]notdeadlock SPEC2:Init.SentBeginReq-->(Memory.RcvdBeginReq) SPEC3:(Memory.SentEndReqorMemory.SentBeginResp)-->(Init.EndResp)SPEC4:Init.SentBeginReq-->(Init.Initial) SPEC5:Init.CurrTrans.cmd==readCmd-->(Target.SentData==Init.RcvdData)SPEC6:Init.CurrTrans.cmd==writeCmd-->(Init.SentData==Target.RcvdData)SPEC7:(Init.SentBeginReqorInit.EndReq)and (Memory.RcvBeginReqorMemory.SentBeginResp) --> Init.CurrTrans.phase==Memroy.CurrTrans.phaseFigure4.25:RequirementsofmemorybussystemusingATcodingstyle.InFigure4.25,the rstrequirementrepresentsthatthereisnodeadlockintheextractedmodelintheabsenceoffaults.ThesecondRequirementshowsthatiftheInitiatorstartsatransaction,theMemorymodulewilleventuallyreceivethetransaction.AlsoiftheMemorysendsaresponsewitheitherENDREQorBEGINRESPphases,theInitiatorwilleventuallybeableto nishthetransactionbysendingENDRESP.Thisisshowninthethirdrequirement.Theforthrequirementchecksifastartedtransactionwilleventually nishandtheInitiatorcanstartanothertransaction.ThisrequirementalongwiththesecondrequirementimplythattheInitiatorisnotblocked.The fthandsixthrequirementsrepresentthatthecommunicateddatabetweentheInitiatorandMem-oryarethesameintheabsenceoffaults.Thelastrequirementhelpstochecktheexecutionorderingoftransactionswhiletheyareexecutedinpipeline.UsingUPPAAL,wehavemodelcheckedthe75abovepropertiesfortheextractedmodel.SPEC'1:A[]notdeadlock SPEC'2:Init.Initial-->(Init.SentBeginReqandx>=delay1)SPEC'3:Init.Initial-->(Memory.RcvdBeginReqandx>=delay1)SPEC'4:(Memory.SentEndReqorMemory.SentBeginResp)-->(Init.EndRespandx<=delay1+delay2)SPEC'5:Init.Initial-->(Init.RcvdBeginRespandx<=delay1+delay2)SPEC'6:Payload.ID==peq_fetch$trans.ID-->sc_time_stamp==Payload.delay+Payload.Initialsc_timeFigure4.26:TimingrequirementsofmemorybussystemusingATcodingstyle.InFigure4.26,the rstrequirementSPEC™1representsthatthereisnodeadlockintheex-tractedmodelintheabsenceoffaults.TheSPEC™2andSPEC™3showthattheInitiatorshouldnotsendthetransactionwithBEGINREQphasebeforedelay1timingpoint,andtheMemoryshouldnotreceivetheBEGINREQrequestbeforedelay1timingpointrespectively.TheSPEC™4checksthatiftheMemorysendseitherENDREQorBEGINRESP,theInitiatorwilleventu-ally nishthecommunicationbyENDRESPnotlaterthandelay1+delay2timingpoint.WeensureiftheInitiatorreceivestheresponsenotlaterthandelay1+delay2timingpointbycheck-ingSPEC™5.TheSPEC™6representsthateachtransactionisexecutedattherighttimingpoint.Thisrequirementhelpstochecktheexecutionorderingoftransactionswhiletheyareexecutedinpipeline.Forinstance,iftransactionT1shouldbeexecutedatxandtransactionT2shouldbeexecutedaty,whilex+sctimestamp()>y+sctimestamp0(),T2isexecuted rst,wheresctimestamp()illustratesthesimulationtimewhenatransactionisbeingsent.UsingUPPAAL,wehavemodelcheckedtheabovepropertiesfortheextracted.764.11Summary Inthischapter,weexplainedtherequirementsthatweneedtosatisfywhileextractingaformalmodelfromthegiveSystemCTLMprogram.WeproposestwosetsoftransformationrulesforextractingformalmodelsfromSystemCTLMprograms.The rstsetofrulestransformstheSystemCprogramintoaPromelamodel.Thesecondsetofrulesgeneratealoosely-timedtimedautomatamodelthatalsoconsiderthenotionoftimeinthemodelextractionprocess.Additionally,weintroduceatool-set,STATE,fortransformingconcurrentSystemCTLMprogramsintotimedautomatamodels.However,someofthemodelsgeneratedbySTATEarecomplexandneedfurthersimpli cationtobeveri able.Finally,weillustratedourmodelextractionideaswith vecasestudies.77Chapter5 ModelingofFaults ThepreviouschapterpermitsmodelextractionofthegivenSystemCTLMprogram.ThiswillallowustoanalyzethegivenSystemCTLMprogramtoverifyitsdesiredpropertiesaswellastoidentifyanybugsinit.Inthissection,wegiveabriefdescriptionoffourtypesoffaultsconsideredinthisdissertation.Thesetypesoffaultsarebasedonthediscussionin[58]thatidenti esfaultsthataretypicallyrelevanttoaSystemCTLMprogram.Inourwork,wedistinguishbetweenfaultsandbugswiththefollowingintuition.Afaultissomethingthatweexpecttohappeninaprogramandweexpecttheprogramtoprovidedesiredbehaviorevenifitoccurs.Examplesofsuchfaultsincludefaultssuchasmessageloss(causedduetonoise),maliciouscomponents,transients,etc.Bycontrast,abugissomethingthatweexpecttoavoid.Examplesincludeuninitializedvariables,bufferover!ow,incorrectuseofblockingornonblockinginterfaces,incorrectuseoftimed/untimedconstructs.Withthisdistinction,intuitively,wewanttoensurethattheprogramworkscorrectlyeveniffaultsoccur.Ourworkfocusesontheformer,i.e.,itassumesthatthedesignerhasdecidedthatitisdif cult/impossibletopreventthefaultsfromoccurringand,hence,itmustbetolerated.Inthefollowing, rst,weexplainthefaultsthatweconsiderinthisdissertationinSection5.1.Then,inSection5.2,wedescribemodelingoffaultsinPromelamodels.FormodelingfaultsinUPPAALtimedautomatamodels,weproposeanalgorithminSection5.3andusethisalgorithmtoinjectdifferenttypesoffaultsintothetimedautomatamodelsextracted.TheanalysisofthemodelsinthepresenceoffaultsaredescribedinSections6.3.1,6.3.2,and6.3.3.785.1FaultCategories Inthisdissertation,weconsiderfourdifferenttypesoffaults.Thesefaultsareasfollows.1.Messagefaults.SinceinSystemCTLMprogramstransactionsareperformedviamessagepassing,oneofthecommonfaultsisamessagefault.Thesefaultsincludemessagecor-ruption,lossandduplication.Inourcasestudies,weconsidermessageloss.Modelingofmessageduplicationissimilar.And,modelingofmessagecorruptionispossibleusingtheapproachfortransientfaults.2.Permanentfaults.Bypermanentfaults,wemeanthattheimpactofthefaultislong-lasting(possiblyforever).Inthispaper,weconsiderstuck-atfaultscausedinhardware,componentfailure,andByzantinefaults.Thestuck-atfaultscauseasignaltogetsstuckata xvalue(logical0,1,orX)andcannotswitchitsvalue.Inacomponentfailurefault,thecomponentfailsfunctionallyandtheothercomponentscannotcommunicatewithit.TheByzantinefaultisonewherethefaultycomponentcontinuestorunbutproducesincorrectresults.Byzantinefaultsencompassbothomissionfailuressuchasfailingtoreceivearequestandfailingtosendaresponse,andcommissionfailuressuchasprocessingarequestincorrectlyandsendinganincorrect/inconsistentresponsetoarequest.3.Transientfaults.TransientfaultsarethemostcommontypesoffaultsthatareprevalentinSoCsystems[19,49].Theyperturbthestateofsystemcomponentswithoutcausinganypermanentdamage.Itisanticipatedthatmostofthesefaultsoccuronlyonce(orasmallnumberoftimes).InthispaperweconsiderSingleEventUpsets(SEUs).Sucheventsmayinducesofterrorsinstorageelements(e.g.,SRAM,sequentiallogic)duetoalphaparticlesgeneratedbytheradioactivedecayofpackagingandinterconnectmaterials.794.Timingfaults.Atimingfaultoccurswhenaneventhappens(ordoesnothappen)inaspe-ci ctimeinterval.Suchtimingfaultscouldperturbthestateofasystemtoanillegitimatecon guration.Forinstance,considerareadtransactionbetweenaninitiatorandamemory,wheretheinitiatorsendsanaddressandareadsignaltofetchadatumfromaspeci cmem-orycell.Ifthereadsignalonthememorysideisactivatedlaterthanrequired(ordeactivatedearlierthanrequired),thereadoperationcannotbeperformedproperly.Wewillinvestigatehowwewillmodelsuchtimingfaultsandtheirimpactsonsystemfunctionalities.5.2FaultModelingforPromelaModels Inthissection,wemodeltransientfaultsandinjectthemintothePromelamodelsextractedinSections4.4and4.5.Transientfaultscanhappenatdifferentplacesoftheextractedmodel.Theycanchangetheaddress,data,phase,etc.Tomodeltransientfaults,thedesignerneedstoidentifyvariablesofconcernasfarastransientfaultsareconcerned.Bydefault,weconsiderthatallvariablescouldbecorrupted. 5.2.1CaseStudy1:FaultModelingandImpactAnalysisforTwoCommu-nicatingModulesInthissection,weusetheextractedmodelexplainedinSection4.4andanalyzethismodelinthepresenceoftransientfaults.Tomodelthetransientfaultthataffectsagivenvariable,wemodelitasalimited-timecorruptionofthatvariableatanyreachablestateintheprogram.Tothisend,westartwithafault-intolerantmodelinPromela,sayM,andasetofactionsthatdescribetheeffectoffaultsonM,denotedF.OurobjectiveistocreateamodelMFthatcapturesthebehaviorsofMinthepresenceoffaultsF.TheSystemCprogramofFigure2.4issubjecttothetypeof80faultsthatcorruptthemessagescommunicatedbetweentheInitiatorandtheTarget.Tomodelthisfault-type,weincludethefollowingproctypeintheextractedPromelamodel:activeproctypeF(){do::(cntatomic{tgtIfPort!startTrans;cnt++;} ::(cntatomic{tgtIfPort!endTrans;cnt++;} ::(cnt>=MAX)->break;od;}TheconstantMAXdenotesthemaximumnumberoftimesthatfaultscanoccur,whereeachtimeanerroneousmessageisinsertedintothechanneltgtIfPort.Thecntvariableisaglobalintegerthatweaddtotheextractedmodelinordertomodeltheoccurrenceoffaults.Formodelingpurposes,weneedtoensurethatfaultseventuallystop,therebyallowingtheprogramtoexecuteandrecoverfromthem.(Asimilarmodelingwhereonedoesnotassume niteoccurrencesoffaultsbutratherreliesonafairnessassumptionthatguaranteesthattheprogramwilleventuallyexecuteisalsopossible.However,itisoutsidethescopeofthisreport.)SincefaultscansendmessagestothetgtIfPortchannel,itispossibletoreachastateoutsidetheinvariantwherethemodeldeadlocks.Forinstance,considerascenariowherefaultFinjectsendTransinthechannel.Then,theTargetreceivesendTransinsteadofstartTrans.Assuch,theTargetnevercompletesthetransactionandneversendsanendTransmessagetotheInitiator,whichiswaitingforsuchamessage;henceadeadlock.815.2.2CaseStudy2:FaultModelingandImpactAnalysisforMemory-MappedBusesInthissection,wemodeltransientfaultssimilartothatexplainedinSection5.2.1,andapplyitonthecasestudyexplainedinSection4.5.Toillustratethetransientfaults,weconsidertwoinstances(1)perturbingmemorycontentswithoutcausinganypermanentdamage,and(2)perturbingtheread/writecommandofthegenericpayload. 5.2.2.1PerturbingMemoryContents Tomodeltransientfaultsthatperturbmemorycontents,wede nethefollowingproctypethatmodelstheimpactofthisfault-typeintheextractedmodelinFigure4.3:activeproctypememFaults(){do::(cnt1atomic{mem[memT.address]=0;cnt1++;} ::(cnt1atomic{mem[memT.address]=1;cnt1++;} ::(cnt1atomic{mem[memT.address]=2;cnt1++;} ::(cnt1atomic{mem[memT.address]=3;cnt1++;} ::else->break;od;}NoticethatwhilethememarrayisdeclaredinsidetheMemorymoduleinLine62ofFigure2.6,inthemodelofFigure4.2,wede neitasaglobalarraysowecanaccessitscontentsfrominsidethememFaultsproctype.Tohave niteoccurrenceoffaults,wede neaconstantMAX1thatdenotesthemaximumnumberoftimesfaultscanoccur.Moreover,weusethecnt1variabletomodeltheoccurrenceoffaultssimilartowhatwedidinSection5.2.1.825.2.2.2ControlSignalFaults Inordertomodeltheeffectofthetransientfaultsthatperturbthecmdofthegenericpayload,weaugmentthemodelofFigures4.2and4.3withthethefollowingproctype:activeproctypecmdFaults(){do::(cnt2atomic{memT.cmd=0;cnt2++;} ::(cnt2atomic{memT.cmd=1;cnt2++;} ::else->break; od;}TheconstantMAX2isthemaximumnumberoftimesfaultscanoccur,andthecnt2showstheoccurrenceoffaults.Thecondition(cnt2,etc.Tomodelthetimingfaults,weintroduceanewvariabledelaytandanewtransitionTttothefault-freeUPPAALmodelthatcanmodelbothearlyandlatetimingproblems.Themaximumvalueofdelayt(defaultvalueis1)isidenti edbythedesigner.TheUPPAALmodelisfurthermodi edtonon-deterministicallyincreasethedelayargumentinatransactionbydelaytinallprocesses.Toautomatethefaultinjection,wetargetthetransitionswithaguard(s).Weinjectthenewtransitionintothemodeltobeinparallelwiththeoriginaltransitionbetweentwolocations,sayLiandLj.Choosingtheoriginaltransition,themodelcontinuesitsexecutionwithoutfaults,whilechoosingthenewtransitioninjectsthetimingfaultsintothemodel.Hence,weintroducerulesofthefollowingformthatutilizethevariabledelayttode netheguard(s)ofthetransitionTt:1)if(x>c)!x>c+delayt2)if(xstatements<=location>flandfistatements<=transition>fl.Thestatementscanbeaname,aninvariant,oratype(e.g.,urgent,committed)forlocations,andasource,atarget,orlabelsfortransitions.Thesourceandtargettagsrepresentthepositionofthetransition.Thelabeltagshowswhetherthetransitionhasasynchronizationchannel,anassignmentoperation,oraguardcondition.TheAlgorithm1utilizesthreefunctionsFind,Remove,andChange.ThefunctionFindtakesamodelMandalabelLandreturnsatransitionTthathaslabelLinmodelM.ThefunctionRemovetakesatransitionTandasynchronizationchannelchandremovesthechannelchfromT.ThefunctionChangetakesatransitionTandavariablevandreturnsatransitionwithachangedvalueofv.88Algorithm1AutomaticFaultInjectionInput:Afault-intolerantTimedAutomatamodelMinXMLformat,variablevsubjecttofaults,typeoffault,andcounterc.Output:Afault-affectedTimedAutomatamodelM0inXMLformat.1:AddMoreFaults true,cnt 0;2:while(AddMoreFaults=true)do3:MessageLoss:4:T Find(M,kind=TransitionKind);5:T0 T;6:T0 Remove(T0,channel);forT0 Change(T0,channel)g7:AddMoreFaults false;8:Fail-stop:9:T Find(M;true);10:ifThasanassignmentstatementthen11:add(downc 1)toT™ssetofassignments;12:else13:addanassignmentstatementtoT,andadd(downc 1)toitssetofassignments;14:endif15:ifThasaguardstatementthen16:add(downc=0)toT™ssetofguards;17:else18:addaguardstatementtoT,andadd(downc=0)toitssetofguards;19:endif20:AddMoreFaults false;21:ByzantineFault:22:T Find(M,kind=TransitionKind);23:T0 T;24:T0 Change(T0,v);fNoneedtochangeAddMoreFaultsg25:Stuck-atFault:26:T Find(M,kind=TransitionKind);27:T Change(T,v);28:AddMoreFaults false;29:TransientFault:30:T Find(M,kind=TransitionKind);31:if(cntc)then32:T Change(T,v);33:else34:AddMoreFaults false;35:endif36:TimingFault:37:T Find(M,kind=TransitionKind);T0 T;38:T0 Change(T0,v);AddMoreFaults false;39:endwhileBasedonthetypeofthefault,thealgorithmscanstheXML le, ndsthecorrespondingpart,andchangesitasnecessaryforthefault.Formessageloss(Lines3-7),weidentifywherethemessagelossoccursby ndingatransitionTthathasalabelkind=synchronization.ThislabelrepresentsthatTissynchronizingwithothermodules.UtilizingT,wecreateT0byremovingitssynchronizationchannel,andinjectitinparallelwithTintothemodel.Inthecasestudies,weapplythisapproachtogenerateseveralfault-affectedmodels,eachmodelconsidersthecase89whereonespeci cmessagemaybelost.Thiscanbetriviallygeneralizedtogenerateamodelthatsimultaneouslylosesmultiplemessages.TomodeltheotherapproachofmodelingmessagelossdescribedinSection5.3.1,thesynchronizationchannelofT0shouldbechangedtoafaultychannel(bycallingfunctionChange).Afterinjectingthefault,weuseavariableAddMoreFaultstoterminatethealgorithm.Tomodelafail-stopfault(Lines8-20),weuseanarbitrarytransitionT.IfThasalabelkind=assigment,whichmeansThasanassignmentstatement,weadddown"1toitssetofassignments.Ifitdoesnot,wede neanewlabelkind=assigmentandadddown"1toitssetofassignment.Thisstepisrepeatedbyeverytransitioninthecomponentsubjecttofail-stopfault.Alsoweaddtheguarddown=0tothesetofT™sguards.Formodelingtheeffectsoffailingaspeci ccomponent,thelocationsoftransitionT(sourcelabelforthestartinglocationandtargetlabelfortheendinglocation)needstobegiventothealgorithm.IfthefaultisaByzantinefault(Lines21-24),weinjectanewtransitionT0inparalleltotheoriginaltransitionT,whichhasanassignmentlabel.Thevalueofthevariablev,whichissubjecttofaults,iscorruptedinT0.ChoosingT0,thefaultisinjectedtothemodel,whilebychoosingT,themodelcontinuesitsnormalexecution.Theoccurrenceofthisfaultdoesnotterminatethealgorithm,whileinjectingastuck-atfault(Lines25-38)terminatesthealgorithm.Fortransientfaults(Lines29-35),wede neacounterthatcontrolsthenumberofoccurrenceofthefault.Whenthecounterisgreaterthantheinputc,thealgorithmterminates.Tomodeltimingfaults(Lines36-38),weinjectanewtransitionT0inparalleltotheoriginaltransitionT,whichhasaguardlabel.Then,we ndtheguardthathasaclockvariableinitandchangetheguardusingthevariabledelaytde nedbythedesigner.905.4Summary Inthispaper,wefocusedonanalyzingtheeffectofdifferenttypesoffaultsthatareofconcernintheSystemCTLMprogram.Wedifferentiatedfaults(thatneedtobetolerated)andbugs(thatneedtobeprevented)andfocusedontheformer.WebeganwiththeextractedmodelfromthegivenSystemCTLMmodel.Weconsideredfourtypesoffaults,messagefaults,permanentfaults,transientfaults,andtimingfaults.Formodel-ingfaultsinPromelamodels,weconsideredtransientfaultsandinjectedthemintothePromelamodelsextractedfromtheSystemCTLMprograms.ForUPPAALtimedautomatamodels,weconsideredfourtypesoffaultsintroducedinSection5.1.Foreachtypeoffaults,weutilizedagenericapproachtotransformtheUPPAALmodeltoobtainafault-affectedmodel.Subsequently,thismodelwasusedinPromelaandUPPAALtoobtainacounterexample.Wewereeitherabletoverifythattheoriginalspeci cationissatis edor ndacounterexampledemonstratingthevi-olationoftheoriginalspeci cation.Moreover,thetimeforevaluatingtheeffectoffaultswascomparable(0-57%)totheveri cationintheabsenceoffaults.InordertodemonstrateourapproachforPromelamodels,weconductedtwocasestudiesandstudiedthePromelamodelsinthepresenceofdifferenttransientfaults.TheanalysisofUPPAALtimedautomatamodelsinthepresenceoffaultsisdiscussedinthenextchapter.91Chapter6 TheToolUFIT:TheFaultInjectorTo UPPAALTimedAutomata Inthischapter,weexplainourtool,UFIT.ThistoolisdevelopedbasedonAlgorithm1explainedinChapter5.Inthefollowingsections, rst,weexplaintheinputofUFIT.Thereafter,usingaruntimeexample,weintroducehowUFITworksandinjectdifferenttypesoffaultsintotheexample.Finally,wedemonstratedourapproachwithseveralcasestudies.6.1InputofUFIT TheinputofUFITisafault-intoleranttimedautomatamodelinXMLformatandasetofparam-eters.WedescribetheseparametersandourfaultmodelingapproachusedinUFITutilizingarunningexamplefromtheliteratureofUPPAALtimedautomata,theFischer™smutualexclusionprotocol[?,9](Figure6.2).6.1.1Therunningexample Fischer™sprotocolisdesignedtoensuremutualexclusionamongseveralprocesses(5processeshere)competingforacriticalsectionusingtimingconstraintsandasharedvariableid.IneachprocessP,theprocessgoestoarequestlocationreqifitistheturnfornoprocesstoenterthecriticalsection(id==0).Afterxtimeunitsinreq(0xk),Pgoestothewaitlocationand92setsidtoitsprocessID.Finally,afteratleastktimeunits,Pentersthecriticalsectioncsifitisitsturn.TheFischer™sprotocolsatis esthefollowingsetofrequirements/propertiesintheabsenceoffaults:SPEC1:A[]notdeadlock SPEC2:P(i).req-->P(i).wait SPEC3:A[]P1.cs+P2.cs+P3.cs+P4.cs+P5.cs<=1whereSPEC1checkswetherthesystemisdeadlock-free.ThelivenesspropertySPEC2checksthatwheneveraprocesstriestoenterthecriticalsection,itwillalwayseventuallyenterthewaitinglocation.ThesafetypropertySPEC3checksformutualexclusionofthelocationsc.6.2InternalFunctionality Togeneratethefault-affectedmodel,inadditiontothefault-freemodel,weneedtospecifythetypeofthefaultsandasetofparameters(seeFigure6.1).ThefaulttypesthatUFITconsidersareasfollows.Messagefaults,whereamessagemaybelostwhileforwardingfromonemoduletoanother;Fail-stopfaults,whereamodulefailsfunctionallyandtheothermodulescannotcommuni-catewithit;Byzantinefaults,wherethefaultycomponentcontinuestorunbutproducesincorrectresults;Stuck-atfaults,whereasignalgetsstuck-ata xedvalue(logical0,1,orX)andcannotswitchitsvalue,and93Figure6.1:TheGUIofUFIT.94Transientfaults,wherethestateofsystemcomponentsisperturbedwithoutcausinganypermanentdamage.Inadditiontothefaulttype,thefollowingthreediscretevariablescanbespeci ed:Variablesubjecttofaults.Wearenotallowedtoincreaseordecreasethevalueoftheclockvariable;Modulesubjecttofaults.Weassumeanymodulecanbesubjecttofaults,andNumberoffaults.Thenumberofoccurrencesofthetransientfaultsthatmaytakeplaceduringthecomputationneedstobede ned.Thedefaultsettingvalueis1.Remark6.1Ifanyoftheabovevariablesisnotspeci ed,UFITwillsetavalueforthemarbitrar-ily.Forinstance,ifthemodulesubjecttofail-stopfaultsisnotspeci ed,UFITwillfailoneofthemodulesrandomly. 6.2.1BriefdiscussionaboutmodelingoffaultsinUFIT Giventheparametersandthefaulttype,intuitivelywemodelthefaultsasfollows.Tomodelamessagefault,weinjectanewtransitionintothemodulesubjecttofaultsinparalleltoatransitionthathasasynchronizationchannel.Thesetofassignments/guardsofthenewtransitionissimilartothatoftheoriginaltransitionexceptthatthesynchronizationchannelischanged.Tomodelafail-stopfault,wede neavariabledownthatshowsifamoduleisfailed(down=1).Forexample,Figure6.3illustratesthatautomatonP1isfailedsinceP1cannotgotolocationwaitandhastostayatlocationreqforever.Tomodelstuck-atfaults,UFIT ndsthelocationofthevariablesubjecttofaultsandchangesittoarandomvalue.Forexample,inFigure6.4,thevalueofidisstuckat5,therebyP1cannotenterthecriticalsection.Formodelingbyzantinefaults,UFITaddsa95x=0x=0, id=1x=0id=0x<=kwaitreqAcsid==0x<=kid==0x>k && id==1Figure6.2:Fault-freemodelofFischer™smutualexclusionprotocol.x<=kwaitreqx = 0, id = 1x = 0Ax = 0, down=1csid = 0id==0 && down==0x>k && id==1 && down==0down==0x<=k && down==0id==0 && down==0Figure6.3:Modelingfail-stopfaultforFischer™smutualexclusionprotocol.transitioninparalleltothatoftheoriginalautomatonthatupdatesthevariablesubjecttofaultsandchangesitsvaluearbitrarily.Figure6.5showsinjectingabyzantinefaultsthatchangesthevalueofid,ifthefaultsoccur.Modelingoftransientfaultsissimilartothatofbyzantinefaultsexceptthattheoccurrenceoftransientfaultsislimited.UFITutilizesthenumberoffaultsde nedintheGUItolimitthenumberofoccurrenceofthistypeoffaults.x=0x=0, id=5x=0id=0x<=kwaitreqAcsid==0x<=kid==0x>k && id==1Figure6.4:ModelingStuck-at5faultforFischer™smutualexclusionprotocol.96x=0, id=5x=0x=0, id=1x=0id=0x<=kwaitreqAcsx<=kid==0x<=kid==0x>k && id==1Figure6.5:ModelingByzantinefaultforFischer™smutualexclusionprotocol.6.2.2AnalysisofResults Inthissection,weanalyzethefault-affectedmodels.Also,inadditiontoFischer™sprotocol,weincludetheresultsoftwootherexamplesadaptedfrom[9]:thetraingateandvikingsproblems.Thetraingateproblemisarailwaycontrolsystemwhichcontrolsaccesstoabridgeforseveraltrains.Thebridgeisacriticalsharedresourcethatmaybeaccessedonlybyonetrainatatime.Thesystemisde nedasanumberoftrainsandacontroller.Themodelsatis esthefollowingpropertiesintheabsenceoffaults:SPEC1:A[]notdeadlock SPEC2:E<>Train(0).Crossand(forall(i:id_t)i!=0implyTrain(i).Stop)SPEC3:A[]forall(i:id_t)forall(j:id_t)Train(i).Cross&&Train(j).Crossimplyi==jSPEC4:Train(0).Appr-->Train(0).CrosswhereSPEC2showsthattrain0cancrossbridgewhiletheothertrainsarewaitingtocross.SPEC3illustratesthatthereisnevermorethanonetraincrossingthebridge(atanytimein-stance),andSPEC4providesthattrain0(similarlyanyothertrain)approachesthebridge,itwilleventuallycross.IntheVikingsproblem,fourVikingswanttocrossabridgeatnight,buttheyhaveonlyone97torchandthebridgecanonlycarrytwoofthem.Thus,theycanonlycrossthebridgeinpairsandonehastobringthetorchbacktotheothersidebeforethenextpaircancross.Eachvikinghasdifferentspeed.Thequestioniswhetheritispossiblethatallthevikingscrossthebridgewithinacertaintime.Thisexampleiscomparabletothequestionifapacketcanreachitsreceiverinagiventimelimitinacommunicationnetwork/NetworkonChip(NoC)system.TheTAmodelsatis esthefollowingpropertiesintheabsenceoffaults:SPEC1:A[]notdeadlock SPEC2:E<>Viking1.safe SPEC3:E<>Viking1.safeandViking2.safeandViking3.safeandViking4.safewhereSPEC2illustratesthatthe rstvikingeventuallygetstotheothersideoftheriverandSPEC3showsthatallthevikingsareintheirsafelocation.TheresultsofanalyzingtheexamplesinthepresenceoffaultsareasshowninTable6.1.Inthistable,ifrequirementxissatis ed,weincludesinthetable,otherwisev.6.3CaseStudiesonModelingFaultsforUPPAALTimedAu-tomataModelsInthissection,weuseUFITtoinjectdifferenttypesoffaultsintothreecasestudiesinSections6.3.1,6.3.2,and6.3.3.The rsttwocasestudiesaremodeledinLoosely-Timed(LT)codingstyleandthelastcasestudyisusingApproximately-Timed(AT)codingstyle.98ProtocolCauseAffectedLocationsSPECTotalTime1234(ms)Fischer™sprotocolFault-freemodelŒsssŒ1250Fail-stopProcessP1vvsŒ143TransientProcessP1vssŒ79Stuck-atProcessP1vssŒ81ByzantineProcessP1vssŒ149Train-GateprotocolFault-freemodelŒssss218Fail-stopControllervvsv35Train0vvsv362MessagelossTraintoControllervssv210ControllertoTrainvssv241VikingprotocolFault-freemodelŒsssŒ25Fail-stopViking0vvvŒ23TorchvvvŒ15MessagelossVikingtoTorchvvvŒ17Byzantine(L=1)TorchvsvŒ29Stuck-at0TorchvssŒ15Stuck-at1TorchvsvŒ15Transient(L=1)TorchvsvŒ14Table6.1:Modelingandanalyzingtheimpactoffaults.6.3.1CaseStudy1:FaultModelingandImpactAnalysis Inthissection,wemodeltimingfaultsandanalyzetheirimpactsonthemodelextractedinSection4.7.AsdescribedinSection5.3,weusedelayttoinjectadelaytotheextractedmodel.Forinstance,intheextractedtimedautomatoninFigure4.7,byinjectingthedealyt,wechangetheguardofthetransition(L4,L5)tox+delaytdelay1+delay2.Asaresult,theguarddoesnotbecometrueandtheprogramgetsstuckatlocationL4.ThisfaultviolatesSPEC1,SPEC4,andSPEC5ofFigure4.10.6.3.1.1Analysisofthefault IftheInitiatorexecutedtoolate,itisunabletoreceivetheresponsesentbytheMemoryontime(atthedelaytimingpointsetbytheMemoryintheresponse).AlsoiftheMemorysetsthedelay99timingpointbutsendsittoolatetotheInitiator,theInitiatordoesnotreceiveitontime.Wemodelitbyinjectingthetimingfaultsintooneofthelocations(L4,L5),(L12,L10),(L13,L10).Injectingthefaultsintotheselocationsviolatesrequirements1,4,and5ofFigure4.10.Table6.2representsmoreexperimentsbasedonthecausesofsometimingfaultsintheSystemCTLMprogramandtheirpossibleinjectinglocationsintheUPPAALmodel.Ifarequirementisviolated,weshowitbyxv,andifitissatis edweshowitbyxs,wherexistherequirementnumberde nedintheFigure4.10.Forexample,whentheMemoryexecutedtoolateandtheaffectedlocationis(L4,L5),therequirementsSPEC1,SPEC4,andSPEC5areviolated,whileSPEC2andSPEC3aresatis ed.Theaveragetimeforcheckingalltheserequirementsis8ms.CauseAffectedLocationsRequirementStatusTotalTime(ms)Initiatorexecutedtoolate(L4,L5)1v;2s;3s;4v;5v8(L12,L10)1v;2s;3s;4v;5v7(L13,L10)1v;2s;3s;4v;5v7Initiatorexecutedtooearly(L2,L4)1v;2v;3v;4s;5v4(L3,L4)1v;2v;3v;4s;5v4Memoryexecutedtoolate(L4,L5)1v;2s;3s;4v;5v8(L12,L10)1v;2s;3s;4v;5v7(L13,L10)1v;2s;3s;4v;5v7Memoryexecutedtooearly(L10,L11)1v;2s;3v;4s;5v5Table6.2:ModelingandanalyzingtimingfaultsinthememorybussystemwhileusingLTcodingstyle. 6.3.2CaseStudy2:FaultModelingandImpactAnalysis Inthissection,wepresenttherulestotransformthefault-freemodelexplainedinFigures4.12and4.13intothefault-affectedmodel.Foreachtypeoffaults, rst,weidentifyagenericapproachformodifyingtheUPPAALmodel.Then,weidentifytherevisedmodelandevaluateitscorrectness.1006.3.2.1MessageFaults Inourextractedmodel,weconsideranarbitrarynumberofmessagelossfaultsthatcanloseanyofthemessagesinthesystem.Hence,weintroduceatransitionwithoutanysynchronizationchanneltomodelamessageloss.Weinjectthistransitionatdifferentcomponents.Forexample,weinjectanewtransitionintotheRouterinFigure4.12betweenLocationsL9andL10.Asaresult,theRouterusesthistransitionandchangesitsstatetoL10andwaitstoreceivetheresponsefromoneoftheTargets.ThedesiredTarget,however,doesnotreceiveanymessagesfromtheRouterandwaitsatitsinitialstate.CauseAffectedLocationsRequirementStatusTotalTime(ms)Fault-freemodelŒ1s;2s;3s;4s;5s13MessagelossInitiatortoRouter1v;2v;3v;4s;5v12RoutertoTarget1v;2v;3v;4s;5v12TargettoRouter1v;2v;3v;4s;5v13RoutertoInitiator1v;2v;3v;4s;5v13ComponentfailureInitiator1v;2v;3v;4z;5v13Router1v;2v;3v;4s;5v13Target1v;2v;3v;4s;5v14ByzantineInitiator1s;2z;3z;4s;5s14Router1s;2z;3z;4s;5s14Target1s;2z;3z;4s;5s14Stuck-atInitiator1s;2z;3z;4s;5s14Router1s;2z;3s;4s;5s14Target1s;2z;3s;4s;5s14Table6.3:ModelingandanalyzingfaultsintheNoCswitchwhileusingLTcodingstyle.WemodelthemessagefaultswhilethemessageissentbetweenInitiator-Router,Router-Target,Target-Router,andRouter-Initiator.TheresultsareasshowninTable6.3.Inthis,andsubsequenttables,ifrequirementxissatis ed,weincludexsinthetable.Ifitisviolated,weincludexv.Iftheanswerismorecomplicated,weincludexzandexplaintheresultinthetext.Also,SPEC5isforallpossibleInitiators.Hence5smeansthattherequirementforalltheInitiatorsissatis ed,101and5vmeansthattherequirementinatleastoneoftheInitiatorsisviolated.TheresultsinTable6.3illustratethattheaveragetotaltimeinthefault-affectedmodel(14ms)iscomparabletothatinthefault-freemodel(13ms).NotethatrequirementSPEC5isde nedfortheInitiatormodulesandcanbede nedfortheRouterandTargetsinthesameway.AsdiscussedinSection5.1,weconsiderthreetypesofpermanentfaults,fail-stop,Byzantinefaultsandstuck-atfaults.Next,weexplainmodelingofpermanentfaultsontheextractedUPPAALmodel. 6.3.2.2Modelingandanalyzingfail-stopfaultsinthecasestudyInthisexample,weconsiderthreetypesoffail-stopfaults:Initiator,Router,andTargetfailures.TheresultsforfailureofdifferentcomponentsisasshowninTable6.3.Asexpected,arouterfailurecausesallpropertiestobeviolated.However,failureofinitiatorortargetdoesnotleadtothewholesystemfailure.Speci cally,regardingtheInitiatorfailure,thelocationofthefaultinjectionaffectssatisfactionofSPEC4.Ifthefaultoccursaftersettingtheattributesinthesendingtransaction,thefaultdoesnotviolateSPEC4.Ifthefaultoccurswhilesettingtheattributes,therequirementSPEC4isviolated.Hence,weshowitas4z.6.3.2.3ModelingandanalyzingByzantinefaultsinthecasestudyInthiscasestudy,weconsiderthecasewherethevariableofconcerniscmd.Forthispurpose,weinjectthefaultsintheInitiatorsuchthatthecmdattributeisnon-deterministicallychanged.Inotherwords,faultcausestheinitiatortobehavemaliciouslybycorruptingthecmdvariablefrom0to1andviceversa.TheeffectsofthesefaultsontheprogramareasshowninTable6.3.AsshowninTable6.3,theresultingprogramsatis esSPEC1,SPEC4andSPEC5andthesatisfactionofSPEC2andSPEC3dependsupontheeffectofByzantinefault.Speci callywhencmdis102changedfrom0to1(respectively1to0),SPEC2(respectivelySPEC3)isviolatedandSPEC3(respectively,SPEC2)issatis ed.WehavealsoconsideredByzantinefailureattheRouterandTarget.TheresultsareasshowninTable6.3. 6.3.2.4Modelingandanalyzingstuck-atfaultsinthecasestudyModelingofthestuck-atfaultsissimilartothatinByzantinefaultsexceptthatoncethefaultoccurs,theaffectedvariablescannotchange.Weconsiderthestuck-atfaultforthevariablecmdto1inTable6.3,whichmeanstheInitiatorisalwaysrequestingawriteaction.Asaresult,whenawriteactionisrequested,theeffectsofstuck-atfaultscannotbefoundandSPEC3issatis ed.6.3.3CaseStudy3:FaultModelingandImpactAnalysis Inthissection,wemodelandanalyzetheimpactofallfourtypesoffaultsexplainedinSection5.1onthemodelextractedinSection4.10. 6.3.3.1MessageFaults ThemodelingofmessagelossinthiscasestudyissimilartothatinSection6.3.2withtheex-ceptionthattheprogramisusingnbtransportfwandnbtransportbwforforwardingandre-ceivingtransactions.Therearefourtypesofmessagesinthissystem,BEGINREQ,ENDREQ,BEGINRESPandENDRESP.Hence,weconsiderthecasewhereanyoneofthesemessagesislost.ThesefaultsaremodeledbyidentifyingthelocationswherethemessageissentandaddingnewtransitionsasdescribedinSection6.3.2.1.TheexperimentalresultsarerepresentedinTable6.4.Asanillustration,considerthecasewhentheENDRESPislost.Inthiscase,theInitiatorwouldnotgetblockedandisabletoinitiateanewtransaction,sincewehavepipelinedtransactions103inthesystem.ThisrequirementcorrespondstosatisfactionofSPEC1andSPEC4inFigure4.25.ThesepropertiesarevalidatedinTable6.4inthepresenceofamessagelossofENDRESP.CauseAffectedLocationsRequirementStatusTotalTime(s)Fault-freemodelŒ1s;2s;3s;4s;5s;6s;7s5MessagelossInitiator-sendingBEGINREQ1v;2v;3s;4v;5v;6v;7s4Initiator-sendingENDRESP1s;2s;3s;4s;5s;6s;7s4.5Memory-sendingENDREQ1v;2s;3v;4v;5v;6v;7s4.2Memory-sendingBEGINRESP1s;2s;3v;4s;5v;6v;7s4.2ComponentfailureInitiator1v;2v;3v;4v;5v;6v;7s4Memory1v;2v;3v;4v;5v;6v;7s4ByzantineInitiator1s;2s;3s;4s;5z;6z;7s5.5Memory1s;2s;3s;4s;5z;6z;7s5.5Stuck-atInitiator-stuck-at11s;2s;3s;4s;5z;6s;7s5.5Memory-stuck-at11s;2s;3s;4s;5z;6s;7s5.5Initiator-stuck-at01s;2s;3s;4s;5s;6z;7s5.5Memory-stuck-at01s;2s;3s;4s;5s;6z;7s5.5TransientInitiator-cmdattribute1s;2s;3s;4s;5z;6s;7s5.5Memory-cmdattribute1s;2s;3s;4s;5z;6s;7s5.5Initiator-phaseattribute1z;2z;3z;4z;5v;6v;7v5.7Memory-phaseattribute1s;2s;3s;4s;5z;6z;7v5.7Table6.4:ModelingandanalyzingfaultsinthememorybussystemwhileusingATcodingstyle.6.3.3.2PermanentFaults Wemodelfailureofcomponents,Byzantinefaults,andstuck-atfaultsinthiscasestudy.Thestructuralchangesperformedforthesefaultstoobtainthefault-affectedUPPAALmodelissimilartothatinSection6.3.2.Inparticular,theByzantineandstuck-atfaultsaremodeledlikethatinSection6.3.2.Inmodelingcomponentfailure,eithertheInitiatorortheMemorycanfail.ThelocationofinjectingthevariabledownccanbedifferentanddoesnotchangetheresultsofTable6.4.FailureofoneofthecomponentsblocksthewholesystemandonlythelastrequirementexplainedinFigure4.25issatis ed,sincethemessageorderingisnotchanged.104InByzantinefaults,weconsiderthecasewherethevariableofinterestisthecmdvariable.And,theByzantinecomponentcanchangeitfrom0to1andviceversa.TheeffectsofthesefaultsonthemodelareasshowninTable6.4.Inthisexample,weconsiderthestuck-atfaultforthevariablecmdtoeither0or1.Whencmdisstuck-at1(respectively0)SPEC6(respectively,SPEC5)inFigure4.25istriviallysatis ed.6.3.3.3TransientFaults Tomodeltransientfaults,thedesignerneedstoidentifyvariablesofconcernasfarastransientfaultsareconcerned.Bydefault,weconsiderthatallvariablescouldbecorrupted.Inthiscasestudy,weconsiderthecasewheretransientfaultscanchangethecommandorphase.Tomodelthetransientfaultthataffectsagivenvariable,wemodelitasaone-timecorruptionofthatvariableatanyreachablestateintheprogram.(ThemodelingoftransientfaultsaresimilartoByzantinefaultsexceptthatthetransientfaultsoccuronlyonce.Bycontrast,aByzantinecomponentcansendincorrectdatacontinuously.)Toillustratethetransientfaults,weconsidertwoinstances:(1)wherecmdattributeiscorrupted,and(2)wherephaseargumentiscorrupted.Regardingatransientfaultthataffectscmd,satisfactionofSPEC5andSPEC6inFig-ure4.25dependsuponwhethercmdiscorruptedfrom0to1orfrom1to0.Hence,Table6.4representsitas5zand6z.Regardingatransientfaultthataffectsphaseattribute,satisfactionofSPEC1,SPEC2,SPEC3andSPEC4inFigure4.25dependsupontheactualeffectofthetransientfault.Forexample,ifBEGINREQisperturbedtoENDRESPthenSPEC3isviolated.However,ifENDRESPisperturbedtoBEGINREQthenSPEC3issatis ed.Hence,Table6.4representsthisas1z;2z;3zand4z.1056.3.3.4TimingFaults Tomodelthetimingfaults,weutilizethesameapproachasthatexplainedinSection6.3.1.Table6.5representsseveralexperimentresultsbasedonthecausesandlocationsofthetimingfaults.Forexample,iftheInitiatorexecutedtooearly,theaffectedlocationsintheUPPAALmodelwouldbeintheInitiatorautomatonandeitherbeforesendingatransactionwithphaseBEGINREQorbeforereceivingthetransactionwithphaseENDREQ.AlsotheaveragetimeforverifyingtherequirementsareverysimilartothatforverifyingtherequirementsofFigure4.26intheabsenceoffaults.CauseAffectedLocationsRequirementTotalStatusTime(s)InitiatorexecutedBeforesendingbeginreq1v;2v;3v;4s;5v;6s11.8tooearlyBeforereceivingendreq1v;2s;3s;4v;5v;6s12InitiatorexecutedAfterdispatchingfrompeq1v;2s;3s;4v;5v;6v16.9Whileinsertingintopeq1v;2s;3s;4v;5s;6v16.9toolateBeforesendingendresp1v;2s;3s;4v;5s;6s17MemoryexecutedWhileinsertingintopeq1v;2s;3s;4s;5v;6v14.2tooearlyDuringthe2ndinsertionintopeq1v;2s;3s;4v;5v;6v16.1MemoryexecutedAfterthe2nddispatchfrompeq1v;2s;3s;4v;5v;6v16.9toolateWhileinsertingintopeq1v;2s;3s;4v;5s;6v16.9Table6.5:ModelingandanalyzingtimingfaultsinthememorybussystemwhileusingATcodingstyle. 6.4Summary Inthischapter,wepresentedthetoolUFITandexplainedhowitmodelsdifferenttypesoffaultsintimedautomatamodels.Foreachtypeoffaults,weutilizedagenericapproachtotransformtheUPPAALmodeltoobtainafault-affectedmodel.Subsequently,thismodelwasusedinUPPAALtoconcludetolerancetofaultsortoobtainacounterexample.Wewereeitherabletoverifythat106theoriginalspeci cationissatis edor ndacounterexampledemonstratingtheviolationoftheoriginalspeci cation.Moreover,thetimeforevaluatingtheeffectoffaultswascomparable(<165%)totheveri cationintheabsenceoffaults.UFITmodelsonetypeoffaultsatatime.Wecanalsoinjectmultiplefaulttypesintothemodelbygivingthefault-affectedmodelobtainedfromUFITtoUFITandinjectanewtypeoffaults.107Chapter7 ModelSlicingTimedAutomataModels Inthischapter,wepresentamodelslicingtechniqueforreducingtheveri cationtimeandspaceoffault-freeandfault-impactedtimedautomatamodelsextractedfromSystemCTLMprograms.Speci cally,wefocusontheuseofmodelslicingconsideredin[51]toslicetimedautomatamodels.Forthispurpose, rst,weexplainabriefhistoryofmodelslicing.Then,weintroducearunningexamplethatweutilizetoexplainourmodelslicingtechnique.Finally,wediscussourslicingalgorithmandillustrateitwiththerunningexample.7.1ModelSlicing Programslicingisasourcecodeanalysisandmanipulationtechnique,inwhichasubprogramisidenti edbasedonauser-speci edslicingcriterion.Thecriterioncapturesthepointofinterestwithintheprogram,whiletheprocessofslicingconsistsoffollowingdependenciestolocatethosepartsoftheprogramthatmayaffecttheslicingcriterion[78].Programslicinghasbeensuccess-fullyappliedinthecontextofmodelcheckingofuntimedsystems.MillettandTeitelbaum[63]studyslicingofPromelamodelsandproposethesocalledimpreciseslice.However,theydonotformalizetheirslicingmethods.Hatcliffetal.[45]presentaformalstudyofslicingsequentialprogramspreservingLTLandextendtheirtechniquestoconcurrentJavaprograms[71].SlicingisalsopresentintheIFproject[16]concerningtimedsystems.Nonetheless,itisde nedforitsuntimedsubsetonly[15].108Theclosestrelatedworkonusingstaticanalysisintimedsystemveri cationconcernstheconceptofin uenceinformation[17].ThetechniquecanbeunderstoodasslicingI/OTimedComponents,timedsafelyautomataextendedwithinterfaces.Theapproachdoesnotusethenotionofslicingcriterion,and,instead,itpreservesthebranchingstructureofatransitionsystemuptothepropositionalassignmentgivenovertheexternalobserver.Anotherrelatedmethodsaretheactive-clockreductiontechnique[22]andmoregeneralrelevantguardabstraction[8]fortimedsafetyautomata.Sincetheyfocusonclocksreductiontheyareorthogonaltooursandcanbecombinedwithit.Finally,JanowskaandJanowskiin[50]targettheslicinginthecontextoftimedsystemsconsideringreductionofintermediatelanguageofVerics[50].Theformalismisaspeci cationlanguagewithnoexplicitclockvariables,butrestrictingthetimeoftransitionsexecutionsbymeansofdelays. 7.2TheRunningExample:TheAlternatingBitProtocol Inthissection,wepresentaversionofthewell-knownalternatingbitprotocol[7]asarunningexampletoexplainourslicingtechniquebetter.Thisprotocolprovidesreliablecommunicationoveranetworkservicethatsometimesloosesmessages.Itusesaone-bitsequencenumber(whichalternatesbetween0and1)ineachmessageandanacknowledgmenttodeterminewhetherthemessagemustberetransmitted.Thesystemconsistsofthreeautomatarunninginparallel,Sender,ReceiverandFaulty-Buffer,asshowninFigures7.1,7.2,and7.3.TheSendertransmitsportionsofdata,whichrepresentssomecomputationsperformedinrealsystems.InourexampletheyaresucceedingnumbersmoduloN.SendersendseachportionaccompaniedwiththebittoFaulty-Buffer.Thenitwaitsforanacknowledgment.Ifthevalueoftheacknowledgmentisthesameasthevalueofthebit,thenthemessageistreatedasdeliveredandthe109Figure7.1:TheSenderautomatonforthealternatingbitprotocol.Figure7.2:TheFaultyBufferautomatonforthealternatingbitprotocol.110Figure7.3:TheReceiverautomatonforthealternatingbitprotocol.valueofthebit!ips.Otherwisethemessageisretransmitted.Themessageisalsoretransmitted,ifnoacknowledgmentcomeswithinTtimeunits(thetimeoutismodeledbytheclockx).ReceiverwaitsuntilitgetsthemessagefromFaulty-Buffer,thenitacknowledgesreceiptofthemessageandcomparesitssequencenumberwiththebitvalue.Iftheyareequal,itchangesthevalueofthebitandacceptsthemessage.Otherwiseitwaitsforanothermessage.Faulty-BufferacceptsamessagefromSenderoranacknowledgmentfromReceiverandforwardsitrespectivelyorloosesit.Theclockyisusedtomodeltransmissiondelays,whicharebetweendandDtimeunits.Forthealternatingbitprotocol,wede neaproperty˚asfollows:˚=A[](Sender:sndinit!sbit==rbit)Thispropertyveri esthatifSenderisinthelocationsinit,thevalueofSender™sbitisequaltothevalueofReceiver™sbit.Theimportantpointtonotehereisthatthispropertydoesnotdependonthevalueofvariablessdata,bdata,andrdata.1117.3UPPAALTimedAutomataModelSlicing Inthischapter,weexplainourmodelslicingalgorithm.OurslicergetsanUPPAALtimedautomatamodelalongwithasetofpropertiesasinputsandgenerateaslicedversionofthetimedautomatamodelasasoutput.Ourslicer,similarto[51],usesatwostepapproach.Inthe rststep(Algorithm2),thesliceridenti esthelocations,sayL,andactions,sayA(includingguards,updates,andassignments),thatneedtobepreservedintheslicedautomata.Thisisarecursiveprocedurewheretheinitialsetofstatesthatneedtobepreservedaredeterminedbythepropertyunderconsideration,say˚(Lines1-2inAlgorithm2).Forexample,ifthepropertyunderconsiderationispleadstoqthenalocationthataccessespandqmustbepreservedintheslicedautomata.Next,weexplainthesetwostepsindetail.Algorithm2TimedAutomataModelSlicingInput:UPPAALmodelM=(Q;q0;X;T),property˚;Output:SlicedUPPAALmodelM0;1:Linit=locationsin˚andtheirimmediatepredecessors;2:Ainit=enablingactionsde ningvariablesin˚;3:L:=Linit;A:=Ainit;4:while(LorAgetsupdated)do5:UtilizethedependenciestoupdateLandA;endwhile6:returnM0=slicer-builder(L;A;M);7.3.1Identifyingthesetofrelevantlocationsandactions(LandA)InordertoidentifyLandA, rst,ouralgorithmneedstocheckifthemodelcontainsanyarraysandfunctions.Intuitively,theUPPAALmodelmayhavetwotypesarearrays:(a)anarrayofautomataand(b)anarrayofvariables.Whenwehaveanarrayofautomatawithnentriesthenessentially,wereplaceitbyndifferentautomata.Ineachautomaton,weneedtoreplicatelocalvariablesbuttheglobalvariablesremainthesameinallnautomata.Similarly,forhandlingan112arrayofvariableswithnentries,wereplaceitbyndifferentvariables.Subsequently,weneedtoreplaceeveryentryineveryautomatonthatusesthearraysothatthearrayreferenceisreplacedbytheappropriatevariable.Italsorequiresreplicatingthelocalvariablesineachautomaton.ThisisacceptablesinceUPPAALalreadydoesthisintheveri cationprocess.Regardingfunctions,weconsiderthesyntacticcodeinvolvedineachfunctiontoidentifyvari-ablesthatareaccessedduringthatfunction.Sinceourgoalistoslicethemodel,wedonotneedtoevaluatethefunction(thiswouldbedonebyUPPAALaspartofveri cation).Instead,weneedtoidentifyifthefunctionisaccessing/changinganyvariablesofinterest.Thiscanpotentiallyintro-ducesomefalsedependencies,i.e.,dependenciesthatdonotexistinrealitybutaresuspectedbytheslicer.However,thisisacceptableaswellsinceanyerrorscausedinthisfashionwouldresultinalarger(butstillcorrect)model.Afterconsideringarraysandfunctions,ouralgorithmutilizesthepropertyunderconsiderationandgeneratesthesetofinitialrelevantlocationsandinitialrelevantactions,sayLinitandAinit,respectively.TheLinitconsistsofthelocationsinandtheirimmediatepredecessors.TheAinitconsistsofalltheactionsthatupdateanyofthevariablesincludedin.Asaninstance,forthealternatingbitprotocolinFigures7.1,7.2,and7.3,Ainit=fsbit=1 sbit;rbit=1 rbitgandLinit=fsinit;scheckg.Subsequently,thesliceridenti esadditionallocations,variables,guards,andstatementsthatneedtobepreserved.Thereasonsforpreservingadditionaldetailsintheslicedmodelinclude(1)controldependency,(2)datadependency,and(3)timedependency(Line5inAlgorithm2).Asanillustrationofcontroldependency,assumethatlocationq1ispreservedinpreviousiteration.Now,iftheUPPAALmodelincludesastatesuchasq2suchthat(1)thereisacomputationfromq2thatreachesq1and(2)thereisacomputationfromq2thatneverreachesq1.Then,q2mustalsobepreservedsinceweneedtoknowwhetherthepathfollowedfromq2willreachq1ornot.113And,decidingwhetherq1isreachedornotcanaffectsatisfaction(orviolation)ofthepropertyofinterest.Asanillustrationoftimedependency,considerthecasewhereq1ispreservedinthepreviousiteration.Supposethereisapathfromq2toq1andthetimespentinstateq2canbenonzerothenq2mustalsobepreserved.(Byde nition,timespentinstatesthataremarkedurgentinUPPAALis0.)Algorithm3SliceBuilderInput:ThesetsoflocationsLandactionsA,andModelM;Output:SlicedtimedautomatamodelM0=(Q0;q00;X0;T0);1:Q0=R;2:if(q02L)thenq00=q0;3:elseq00=the rstreachablelocationinLfromq0;endif4:T0=Sout(L)s.t.actionofeachout(L)2A;5:if(target(out(L))62L)then6:target(out(L))=the rstreachablelocationinL;endif7:returnM0;7.3.2Buildingtheslicedmodel Whenthesetofrelevantlocationsandactions(L;A)isready,inthesecondstep,theslicerbuildsarevisedmodelthatonlyincludestherelevantlocationsandactions(Algorithm3).Whilebuildingtheslicedmodel,iftheinitiallocationofanautomatonisnotincludedinL,the rstreachablelocationinLbecomesthenewinitialstate(Lines2-3inAlgorithm3).Also,ifthetargetofanoutgoingtransitionofalocationinLisnotincluded,the rstreachablelocationinLbecomesthetargetofthatoutgoingtransition(Lines5-4inAlgorithm3).Asanillustration,considerFigure7.4whereq1andq4arerelevantlocationsthatneedtobepreservedandq2andq3arelocationsthatarenotrelevant.Inthatcase,theoutgoingtransitionofq1goesintoq4.Moreover,theactionsofeachtransitionarethosewhichareincludedinA(Line4inAlgorithm3).Theproofofcorrectnessofthemodelslicingapproachisdiscussedin[51].114Figure7.4:Buildingtheslicedmodel.Thesetoflocationsofeachautomatonoftheslicedsystemconsistsofrelevantlocationsoftheoriginalautomaton.Ifanautomatonhasnorelevantlocations,itmeansthatthewholeautomatonisnotrelevantincontextofconsideredproperties.Thesetofvariablesofthesliceconsistsofvariablesoftheoriginalsystemwhichappearinrelevantoperations.Infact,theonlyclocksthatarereducedareusedexclusivelytoensurethattimecannotprogressinsomelocations.Foreachautomatonthesetoftransitionsiscomposedoftransitionsoftheoriginalautomatongoingoutofrelevantlocations.Ifanoriginaltransitiongoestoanonrelevantlocation,thenthetargetofitscounterpartinthesliceistherelevantlocationtowhichaninvisiblepathexits.Itcanbeshownthatforarelevantlocationandeachofitsoutgoingtransitionsthereexistsexactlyonesuchlocation.7.4ApplyingtheModelSlicingontheAlternatingBitProtocolLetuspresenthowouralgorithmworksforourexample.TheconstructionofthesetsLandAstartswiththeinitialsetsLinitandRinit.Hence,atthebeginningA=fsbit=1 sbit;rbit=1 rbitgandL=fsinit;scheckg.AccordingtoLines4and5ofthealgorithm,thefollowingoperationsareaddedtosetA:sack==sbit,(sack!=sbit),rtbit==rbit,andrtbit!=rbit.Theoperationssack==sbitandsack!=sbitareaddedsincethelocationsinitisinLandcontroldependsonthelocationscheck.Theoperationsrtbit==rbitandrtbit!=rbitareaddedsincetheoperation(rbit=1 rbit)isinA.115Then,setAissuccessivelyaugmentedbytheoperationsthatdependontheoperationscurrentlyincludedinA.Thesenewlyaugmentedoperationsaresack=back,rtbit=bbit,bbit=sbit,andback=rbit.Theoperationsack=backisaddedsincesack==sbitisincludedinA.Likewise,theoperationrtbit=bbitisaddedasrtbit==rbitisincludedinA.Also,theoperationbbit=sbitisaddedastheoperationrtbit==bbitisincludedinA.Finally,theoperationback=rbitisaddedsincetheoperationsack==backisincludedinA.Next,thefollowinglocationsareaddedtosetL:sndsend,rcvack,bufferdataandbufferack.TheselocationsareaddedtoLsincetheiroutgoingtransitionscontainoperationsthatareincludedinA.Additionally,thealgorithmaddsthelocationssndwait,rcvinit,andbufferinittosetLsincetherearelocationscurrentlyincludeinLthataretimedependentonthem.Finally,theseconditerationdoesnotchangeanyofthesetsAandLand,asaresult,theloopends.Whenthesetsofrelevantlocationsandactions,LandA,areready,weutilizeAlgorithm3tobuildtheslicedtimedautomatamodel.TheautomatabuiltforSenderandFaultyBufferautomataareshowninFigures7.5and7.6respectively.InSenderautomaton(Figure7.5),thelocationsndproducedisappearsintheslicedversionsinceitappearstobenon-relevantasnolocationdependsonit.Also,therearenovariablessdata,rdataandbdataineitherSenderautomatonorFaultyBufferautomaton(Figure7.6)astheydonotoccurinanyofrelevantactions.Additionally,theReceiverautomatonremainsthesamesincenoneoftheaforementionednon-relevantvariablesisusedinthisautomaton. 7.5Summary Inthischapter,wespeci edourmodelingslicingtechniqueandexplaineditwitharunningexam-ple.Additionally,Weidenti edhowtoconductfunctionsandarraysinatimedautomatamodel.116Figure7.5:TheslicedSenderautomatonforthealternatingbitprotocol.Figure7.6:TheslicedFaultyBufferautomatonforthealternatingbitprotocol.117Wehavealsodevelopedatoolforourmodelslicingtechniquewhichwillbeintroducedinthenextchapter.118Chapter8 USlicer:AToolforModelSlicingUPPAAL TimedAutomataModels Inthischapter,wepresentthetoolUSlicer(UppaalSlicerfortimedautomata)andexplainitseffectivenessonverifyingtimedautomatamodels.Giventhefault-freeorfault-affectedtimedautomatamodelalongwithasetofproperties,USlicergeneratesaslicedversionofthemodelbasedonthepropertyunderconsideration.Ourresultsshowthat,insomecasesthattheveri cationofthemodelisnotpossibleduetocomplexity,utilizingUSlicerhelpsustomaketheveri cationpossibleinareasonabletimeandspace.8.1InternalsofUSlicer USlicertargetsUPPAALtimedautomatamodelsandslicesthembasedonasetofpropertiesofinterest.ItiswritteninPythonanditssourcecodeispubliclyavailable.TheinputofUSlicerisatimedautomatamodelinXMLformat.ForparsingtheXML le,weutilizeXMLElementTreelibraryofpython.TheElementtypeisa!exiblecontainerobject,designedtostorehierarchicaldatastructures,suchassimpli edXMLinfosets,inmemory.TheElementTreewrappertypeaddscodetoloadXML lesastreesofElementobjects,andsavethembackagain.Next,weexplaintheXML lethatUSlicerandUPPAALtool-setacceptasaninputinsomedetail.1198.1.1XMLformat XMLisamarkuplanguagethatisusedtodescribedata.ThebasicbuildingblockofanXML leisanelement,de nedbytags.AnXML lethatrepresentsanUPPAALtimedautomatamodelcontainsthefollowingmaintags:fistatements<=location>flandfistatements<=transition>fl.Theformershowsthelocationsandthelatterrepresentsthetransitionsofthetimedautomatamodel.Also,thestatementscanbeaname,aninvariant,oratype(e.g.,urgent,committed)forlocations,andasource,atarget,orlabelsfortransitions.Thesourceandtargettagsrepresentthepositionofthetransition.Thelabeltagshowswhetherthetransitionhasasynchronizationchannel,anassignmentoperation,and/oraguardcondition.USlicerutilizesXMLElementTreelibrarytoparsetheXML leofthegivenprogram.AsexplainedinAlgorithms2and3inChapter7,USlicerutilizesa2-stepapproachforslicingthetimedautomatamodel.ToevaluatetheeffectivenessofUSlicer,weconsidertwocasestudiesinthefollowingsections.The rstcasestudyisbasedontheproducer-consumerprogramandisconductedinLoosely-Timed(LT)codingstyle.Suchastyleofcodingheavilyreliesonablockingtransportinterfacebtransport().Thesecondcasestudyisbasedonthememory-mappedbusesandisconductedinApproximately-Timed(AT)codingstyle.Inthisstyleofcoding,designersbene tfromanon-blockingtransportinterfacenbtransport().Ingeneral,theblockingtransportinterfaceisonlyabletomodelthestartandendofatransaction,whereasthenon-blockinginterfaceallowsatransactiontobebrokendownintomultipletimingpoints.1208.2CaseStudy1:Producer-ConsumerProgram Inthisexample,aproducerandaconsumercommunicatethroughablockingtransport.Thepro-ducergeneratesapieceofdata,putsitintoashared xed-size(3here)bufferandwaitsfortheconsumertoconsumethedata.Whenthedataisconsumed,theproducergeneratesthenextpieceofdata.GiventheSystemCTLMprogramofthisexample, rst,weextractthetimed-automatamodel(asexplainedinChapter4).Toensurethatthetimed-automatamodelcapturestherequire-mentsoftheTLMprogram,wespecifythefollowingproperties/requirementsthatshouldholdintheabsenceoffaults:LT1:E<>producer.writenBuff LT2:producer.start-->producer.end LT3:A[](producer.writenBuff&&consumer.readBuffer)implyWriteIndex==ReadIndexLT4:A<>(WriteIndex==ReadIndex)) LT5:E<>consumer.readBuffer LT6:A[](WriteIndex==ReadIndex||WriteIndex==(ReadIndex+1)%n)The rstpropertyshowsthattheproducereventuallygeneratessomedata.Thesecondpropertyrepresentsthatwhentheproducerstartsgeneratingsomedata,thedatawillbeeventuallyconsumedbytheconsumerandtheproducercanstartgeneratingthenextpieceofdata.Thethirdpropertyensuresthatconsumerconsumesthedatawhichiscurrentlygeneratedbytheproducerandtheconsumerwon™ttrytoremovedatafromanemptybuffer.Thefourthpropertyshowsthatalwaysconsumerconsumesthedatageneratedbytheproducer.The fthpropertyrepresentsthattheconsumereventuallyconsumesthedata.Finally,thelastpropertyillustratesthattheconsumer™sandproducer™sindicesarenevermorethanoneapart.Wehavemodelcheckedtheseproperties121usingUPPAALandtheresultsareavailableinTable8.1.Forthemodelchecking,weuseapersonalcomputerwithquadcoreCPU(2.8GHZeach)and6GBmemory.Next,wecomparetheveri cationtimeandmemoryusageforverifyingtheabovepropertiesofthetimedautomatamodelanditsslicedmodelintheabsenceandpresenceoffaults.PropertyOriginalModelSlicedModelVeri cationMemoryNo.ofNo.ofVeri cationMemoryNo.ofNo.ofTime(ms)Usage(KB)statesvariablesTime(ms)Usage(KB)statesvariablesLT15529,288117904020,5328529LT281232,8921179018722,21210631LT331233,98511790521,888127LT431333,96611790421,876107LT55730,015117904120,5328529LT631133,98511790521,521127Table8.1:ComparisonoftheoriginalandslicedmodelsintheabsenceoffaultswhileusingLTcodingstyle.FaultLocationPropertyOriginalModelSlicedModelstatusVeri cationMemoryNo.ofstatusVeri cationMemoryNo.ofv/sTime(ms)Usage(KB)variabless/vTime(ms)Usage(KB)variablesFail-stopConsumerLT1s5530,11291s3920,53530Fail-stopConsumerLT2v4533,02391v4021,22132Fail-stopConsumerLT3s33535,65491s521,8108Fail-stopConsumerLT4v2635,36191v121,0938Fail-stopConsumerLT5v3530,11291v3220,43530Fail-stopConsumerLT6v5434,12091v121,3548Msg-lossProducerLT1v4830,85592v4020,61531Msg-lossProducerLT2v5132,10292v4522,33333Msg-lossProducerLT3s34436,34292s524,1099Msg-lossProducerLT4v1536,34592v123,0219Msg-lossProducerLT5v4830,85592v4020,61531Msg-lossProducerLT6s38134,35092s524,1099Table8.2:ComparisonoftheoriginalandslicedmodelsinthepresenceoffaultswhileusingLTcodingstyle. 8.2.1Slicingintheabsenceoffaults Oncewehavethefault-freetimedautomatamodel,weusethemodelandpropertiesprovidedabovetoslicethemodel.ConsiderthatwedonotuseUFITsincewewanttostudythemodelin122theabsenceoffaults.Foreachproperty,wegenerateaslicedmodelandcomparetheveri cationtime,memoryusage,numberofstates,andnumberofvariablesoftheoriginal/fault-freemodelandtheslicedmodelgeneratedbyourmodelslicer.Weobservethatourslicingtechniquehelpstosimplifythemodelandreducethetimeandmemoryneededforverifyingtheproperties(seeTable8.1).Forexample,forverifyingpropertyLT3,theveri cationtime,memoryusage,numberofstates,andnumberofvariablesarereducedby98%,35%,89%,and92%respectively.8.2.2Slicinginthepresenceoffaults Tostudythemodelinthepresenceoffaults,weconsidertwotypesoffaultsinthisexample:(1)fail-stopfaults,whereamodulefailsfunctionallyandtheothermodulescannotcommunicatewithit,and(2)messagefaults,whereamessagemaybelostwhileforwardingfromonemoduletoanother.WeutilizeUFITtoinjectthesefaultsintothefault-freemodelgeneratedbySTATE.Forfail-stop,weconsiderthescenarioswheretheconsumerfailsandisnotabletoconsumeanydatafromthebuffer.Forthemessagefaults,weassumethatthemessagesmaygetlostwhiletheproduceriswritingthemintothebuffer.Table8.2representstheresultsforverifyingtheoriginalmodelanditsslicedmodelinthepresenceoffaults.WedonotincludethenumberofstatesinthistablesinceUFITdoesnotintroducenewstatesintothemodel.Wenoticethattheveri cationtimefor ndingtheviolation,memoryusage,andthenumberofvariablesintheslicedmodelsarereducedby11%Œ99%,29%Œ32%,and66%Œ92%respectivelycomparetothoseintheoriginalmodel.Considerthat,whenthepropertyunderveri cationisviolatedinthepresenceoffaults,theveri cationtimemaybesmallerthanthatintheoriginalmodelsincetheveri cationisterminatedupon ndingtheviolation.1238.3CaseStudy2:Memory-MappedBuses Inthissection,wepresentanexamplethatutilizesATcodingstyleformodelinganon-chipmemory-mappedcommunicationbusesbetweenaninitiatormoduleandatarget/memorymodule.Inthisexample,adaptedfrom[1],theinitiatorandthememorymodulescommunicatethroughanon-blockingtransport.Thenon-blockingtransportisimplementedaccordingtotheTLMbaseprotocol,i.e.,itbreaksdowneachtransitionintofourphases,namelyBeginReq,EndReq,Be-ginResp,andEndResp,whereeachphaseinatransitionisassociatedwithatimingpoint.More-over,inanATcodingstyle,eachmodulehasaqueuecalledPayloadEventQueue(PEQ).ThePEQisatime-orderedlistofeventnoti cationintheTLMmodel.UtilizingSTATE,wegeneratethetimedautomatamodelfromthegivenSystemCTLMprogram(asexplainedinChapter4).Wealsode neasetofpropertiestoensurethatthegeneratedmodeliscorrectintheabsenceoffaults.Thesepropertiesareasfollows:AT1:E<>Init.SentBeginReqandMemory.RcvdBeginReq AT2:Initiator.SentBeginReq-->Memory.RcvdBeginReq AT3:A[](Initiator.sentBeginReq&&request_in_progress==0)imply(Memory.SentEndReqorMemory.SentBeginResp)AT4:(Memory.SentEndReqorMemory.SentBeginResp)-->(Init.EndResp)AT5:E<>Init.EndResp AT6:scheduler.inititate-->scheduler.executeThe rstpropertyrepresentsthattheinitiatoreventuallyinitiatesatransactionandthememoryeventuallyreceiveit.Thesecondpropertyshowsthatwhenevertheinitiatorstartsatransaction,thememorymodulewilleventuallyreceiveit.ThethirdpropertyensuresthatiftheinitiatorhassentatransactionandthePEQisempty,thememoryisinastatewhereeithertheEndReqmessage124ortheBeginRespmessagehasbeensent.Inaddition,ifthememorysendsaresponsewitheitherEndReqorBeginRespphases,theinitiatorwilleventuallybeableto nishthetransactionbysendingEndResp.Thisisshowninthefourthproperty.The fthpropertyshowsthatatleastoneofthetransactionswillbeexecutedcompletelyandtheinitiatorwilleventuallysendamessagewithanEndRespphase.Finally,thelastpropertyrepresentsthattheschedulereventuallyexecutessomeprocess.Next,wecomparethetimeandmemoryneededforverifyingthesepropertiesintheabsenceandpresenceoffaults. 8.3.1Slicingintheabsenceoffaults WeuseUPPAALtool-settoverifytheabovepropertiesonthesamepersonalcomputerasthatinSection8.2.However,wearenotabletoverifypropertiesAT2,AT3,AT4,andAT6sincethemodelgeneratedbySTATEistoocomplexandthecomputerrunsoutofmemorywhileverifyingthoseproperties(seeTable8.3).Also,thememoryneededtoverifyAT1andAT5,whichareonlyreachabilityproperties,is0.99GB.Therefore,weutilizeourslicingtechniquetosimplifythemodelbasedonthepropertiesgiven.UsingUPPAAL,weareabletoverifyallthepropertiesintheslicedmodelsandcheckiftheyaresatis ed(s)orviolated(v).Forexample,theveri cationofpropertyAT3inthecorrespondingslicedmodeltakes1sand476ms,andthememoryusageis51.5MB.Alsothenumberofvariablesneededforverifyingthispropertyintheslicedmodelin50,whichisreducedby81%. 8.3.2Slicinginthepresenceoffaults WeutilizeUFITtoinjectmessageandfail-stopfaultsintothetimedautomatamodelgeneratedbySTATE.Regardingthefail-stopfaults,weconsiderthescenarioswherethememorymoduleis125failedandtheinitiatormoduleisnotabletocommunicatewithit.Sinceinjectingthefaultsintothemodelmakesthemodelmorecomplex,veri cationofsomeproperties(i.e.,AT1andAT4)isnotfeasible.Therefore,wegivethefaultaffectedmodelandthedesirablepropertytotheslicer,andtheslicergeneratesasimpli edmodelbasedontheproperty.Surprisingly,weareabletoverifyallthepropertiesmentionedaboveintheslicedmodels(seeTable8.4).Asanillustration,veri cationofpropertyAT4,whichwasnotfeasibleintheoriginalmodel,takes1sand250msandneeds49.9MBmemory.Also,thenumberofthevariablesintheslicedmodelisreducedby79%.Inordertomodelthemessagefaults,weassumethatthemessageswithBeginregphasemaygetlostwhentheinitiatorisforwardingthemtothememorymodule.Havingthisfaultinjectedtothemodel,weareabletoverifyalltheabovepropertiesintheslicedmodels(seeTable8.4).Forinstance,verifyingpropertyAT2takes201msandneed43.9MBmemoryintheslicedmodel.Thisveri cationhasreducedthetimeandmemoryusageby14%and96%respectively.PropertyOriginalModelSlicedModelVeri cationMemoryNo.ofNo.ofVeri cationMemoryNo.ofNo.ofTime(ms)Usage(KB)statesvariablesTime(ms)Usage(KB)statesvariablesAT12,212991,76518827635038,98012243AT2N/AN/A18827682143,95013051AT3N/AN/A1882761,47651,50913750AT4N/AN/A1882761,25049,89813657AT52,643994,59218827635438,87512143AT6N/AN/A18827681543,65712947Table8.3:ComparisonoftheoriginalandslicedmodelsintheabsenceoffaultswhileusingATcodingstyle. 8.4Summary Inthischapter,weintroducedourmodelslicer,calledUSlicer,whichisdevelopedusingthealgo-rithmsexplainedinthelastchapter.WestudiedtheeffectivenessofUSlicerontwocasestudies.126FaultLocationPropertyOriginalModelSlicedModelstatusVeri cationMemoryNo.ofstatusVeri cationMemoryNo.ofv/sTime(ms)Usage(KB)variabless/vTime(ms)Usage(KB)variablesFail-stopMemoryAT1v180655,950277v15038,91044Fail-stopMemoryAT2v255898,750277v20043,99052Fail-stopMemoryAT3v2821,350,746277v25651,65651Fail-stopMemoryAT4N/AN/AN/A277s1,26649,91058Fail-stopMemoryAT5v187656,870277v15238,99044Fail-stopMemoryAT6N/AN/AN/A277s81743,67048Msg-lossInitiatorAT1v160655,950278v15538,91045Msg-lossInitiatorAT2v2351,165,655278v20143,99053Msg-lossInitiatorAT3N/AN/AN/A278s1,48051,72152Msg-lossInitiatorAT4N/AN/AN/A278s1,25249,92359Msg-lossInitiatorAT5v165657,750278v15538,99245Msg-lossInitiatorAT6v217899,677278v19543,67349Table8.4:ComparisonoftheoriginalandslicedmodelsinthepresenceoffaultswhileusingATcodingstyle. Ineachcasestudy,westudiedthreetypesofproperties:reachability(LT1,LT5,AT1,andAT5),liveness(LT2,LT4,AT2,AT4,andAT6),andsafety(LT3,LT6,andAT3)properties.IntheLTcodingstyle,ingeneral,veri cationtimesaresmallsincetheLTmodelsareef cientinna-ture.Inspiteofthis,theveri cationtimewasreducedby11%Œ99%.Nevertheless,slicingtheATcasestudywasessentialsincewewerenotabletoverifyanyofthelivenessorsafetypropertiesintheoriginalmodel.Theonlytypeofpropertywecouldverifywasreachabilitypropertysincetheveri cationterminatesupon ndingthe rstsolutioninverifyingsuchproperties.Bycontrast,withthehelpofslicing,itwaspossibletoverifyallpropertiesofinterestinareasonabletime.Thespeedupassociatedwithveri cationofsafetyandlivenesspropertieswassubstantial.Forexample,theproperty(speedup)combinationinourcasestudieswasLT1(1.375),LT2(4.34),LT3(62.4),LT4(78.25),LT5(1.39),andLT6(62.2).TheslicingwasespeciallyeffectivewithATmodelssinceveri cationofcertainproperties(AT2,AT3,AT4,andAT6)wasimpossiblewithoutslicing.Hence,weanticipatethatslicingwouldbeessentialforATmodelswhereveri -cationwithoutslicingisimpossibleevenforsimpleexamples.IncaseofLTmodels,veri cationwithoutslicingwaspossible.However,thereasonforconsideringthisexamplewastoquantifythebene tofslicing.(ATmodelsdonotprovideanopportunitytoquantifythisbene tsinceveri -127cationtimewithoutslicingisessentially1.)InLTmodels,slicingimprovedtheveri cationtimesubstantially.Weanticipatethatslicingwouldbeespeciallybene cialforlargerLTmodelswhereveri cationwithoutslicingisimpossible.Considerthat,theprogramsconsideredinourcasestudiesarethemostoptimalintermsofthe(SystemC)sourcecodeand,hence,slicingalgorithmswillnotchangethem.Whatwediscussedinthischapteristhatitispossibletoreducethecostofveri cationfurtherinthesecontextsviaslicingthetimedautomatamodelsextractedfromtheSystemCprograms.ItfollowsthatonecanutilizeexistingmethodstoslicetheSystemCprogramtoobtainthesmallestSystemCcodeandthenutilizeourapproachtoreducetheveri cationtimeandspaceofthatsmallestprogram.128Chapter9 ConclusionandFutureWork Theriseincomplexity,sizeandheterogeneityofmodernembeddedsystemdesignshaspushedmodelingtonewabstractionlevelsaboveRTL.TransactionLevelModelingusingSystemChasemergedasanewparadigmforsystemmodeling.Ontheotherhand,SoCdesignisbeingadaptedtocombinethebestfeaturesoftopdownandbottomupsystemdesign.AlthoughthemodelsinSystemCTLMaredesignedcarefully,theirveri cationisanimportanttask.Moreover,manyindustrialandacademicinstitutionssupportanduseSystemCandTransactionLevelModelingforsoftware/hardwareco-design.Thus,asystematic(andpossiblyautomatic)approachforver-i cationofSystemCTLMprogramshasasigni cantimpact.Tohaveasystematicmethodforveri cationofsuchprograms,inthisdissertation,wepresentedaframeworkthatcrosscutssev-eral eldssuchascompilers,veri cation,faulttolerance,andmodelchecking.Inparticularourframeworkinvolved vemainsteps,namelyde ningformalsemantics,modelextraction,faultmodeling,modelslicing,andmodelchecking.The rsttwostepsobtainanabstractmodeloftheSystemCprogram.WechosePromelaandUPPAALtimedautomataasthetargetmodelinglan-guagessincetheyallowedustoevaluatetheeffectoffaultswiththemodelcheckersSPIN[48]andUPPAAL[9].Weconsideredtwotypesarecodingstyle,Loosely-Timed(LT)andApproximately-Timed(AT),inourframework.TargetingPromelamodels,weproposedasetoftransformationrulesthathelpusextractaPromelamodelfromaLoosely-TimedSystemCTLMprograms.How-ever,thePromelamodelsextractedareuntimed.RegardingUPPAALtimedautomatamodels,weconsiderthenotionoftimeandtargetbothLoosely-TimedandApproximately-Timedcoding129styles.Inparticular,weproposeasetoftransformationrulesforextractingtimedautomatamod-elsfromLoosely-Timedprograms.Wealsoutilizedatool,calledSTATE,forextractingtimedautomatamodelsfromApproximately-TimedSystemCTLMprogram.Subsequently,inthethirdstep,weaugmentedtheextractedmodelwithfaults.Thisstepre-quiresustomodeltheimpactoffaultsonSystemCTLMprogramsandcapturetheminthecontextofPromela[3]ortimedautomata[5].Westudiedfourdifferenttypesoffaultsinthisdissertationnamely,messagefaults,permanentfaults,transientfaults,andtimingfaults.Weproposedatool,calledUFIT,thatmodelstheaforementionedfaultsinUPPAALtimedautomatamodelsandgen-eratesafault-affectedmodel.ThemodelsextractedfromtheSystemCTLMprogramsaremostlycomplexandgetevenmorecomplexafterinjectingfaultsintothem.Hence,inthefourthstep,weproposedamodelslicingtechniqueforslicingthetimedautomatamodels.Wedevelopedatool,calledUSlicer,thatgetsatimedautomatamodelalongwithapropertyofinterestandgeneratesasimpli edversionofthemodel.Thisstepimprovestheveri cationtimeandspace.Finally,inthelaststep,wemodelcheckthemodelandstudythebehaviorofthemodelsinthepresenceoffaults.Weillustratedourframeworkwithseveralcasestudies.ThesecasestudiescoveredprogramsthatutilizedLTandATcodingstyles.Ineachcasestudy,weextractedeitherthePromelamodelorthetimedautomatamodelfromthegivenSystemCTLMprogram.Thereafter,wemodeleddiffer-enttypesoffaultsandinjectedthefaultsintothemodels.Inparticular,WeanalyzedtheuntimedextractedPromelamodelsinthepresenceofcommunicationfaults.Sincetransactionlevelmod-elingisbasedontheprincipleofseparatinginter-componentcommunicationsfromcomputationsusingthenotionoftransactions,designingfault-tolerantcommunicationprotocolsisfundamentaltotransactionlevelmodeling.Thisexampleillustratestheroleofourframeworkindealingwithfaultsthatoccurinsuchinter-componentcommunications.Asimilarapproachcanalsobeeasily130appliedtoothercommunicationerrorsinsuchapplications.WealsoanalyzedthetimedUPPAALmodelsinpresenceofallfourtypesoffaults.Wewereeitherabletoverifythattheoriginalspeci -cationissatis edor ndacounterexampledemonstratingtheviolationoftheoriginalspeci cation.Moreover,thetimeforevaluatingtheeffectoffaultswascomparable(0-57%)totheveri cationintheabsenceoffaults.WealsousedUSlicertoslicethetimedautomatamodelsandimprovetheveri cationtimeandspace.IntheLTcodingstyle,ingeneral,veri cationtimesaresmallsincetheLTmodelsareef cientinnature.Hence,althoughutilizingmodelslicingimprovesthetimeandspaceef ciency,itisnotessential.Nevertheless,slicingtheATcasestudywasessentialsincewewerenotabletoverifyanyofthelivenessorsafetypropertiesintheoriginalmodel.Theonlytypeofpropertywecouldverifywasreachabilitypropertysincetheveri cationterminatesupon ndingthe rstsolutioninverifyingsuchproperties.Also,theslicedmodelcouldbeveri edinareasonabletimebothinthefault-freeandfault-affectedmodels.Thiscasestudyillustratesoneofthemainadvantagesofusingourmodelslicingtechniquewheretheslicingenabledveri cationwhereastheoriginalmodelwastoolargetoverify. 9.1Aroadmapforfutureresearch. Weproposeseveraldirectionsforfutureresearchonthisdissertation.Weplantoextendourpreviousworkonautomatedadditionoffaulttolerance[24,54]inordertoautomatethedesignoffaulttoleranceintheextractedPromelaandUPPAALmod-els.Inadditiontofacilitatingthedesignoffaulttolerance,wewouldliketoenablefault-containmentmechanisms,wheredesignerscanguaranteethatfaultsdonotgetpropagatedtoseveralcomponentsatonce.Thisinformationcanbeusedtoaddrestrictionsonthecom-municationamongstcomponentstoensurecompliancewiththisrequirement.131WewillextendourworkwithasetofreversetransformationrulestoensurethatthecodeaddedtomodelsinordertocapturefaulttolerancecanindeedberealizedinSystemCpro-gram.Forexample,weneedrulesthatspecifyhowatomicrecoveryactionswillbecapturedinSystemCwhilepreservingatomicityandrecovery.Onewaytoachievethisistore netheatomicactionstoacodeblockbetweentwowaitstatementsinSystemC.ThisrulereliesonthefactthattheschedulerofSystemCsimulatorhasarun-to-completionpolicyforcontextswitching.Wewillinvestigatedifferentscenariosunderwhichfaulttolerancefunctionalitiesaddedtomodelscanbepartitionedandassignedtosoftwareandhardware.Onepossibilityistousetherulethatanyfaulttolerancefunctionalitythatcanbeexecutedasynchronouslywiththerestofthemodelcanbecapturedasasoftwarecomponent,whereassynchronousfunction-alitiescanbeincludedinhardware.Nonetheless,thedecisionofincludingapieceofnewfunctionalitiesinhardware/softwaremaydependuponotherfactorssuchastimingissues,energyconsumption,overallsystemmodularity,etc.Weplantoinvestigatetheimpactofsuchfactorsonco-designoffaulttolerance.132BIBLIOGRAPHY133BIBLIOGRAPHY[1]Gettingstartedwithtlm-2.0.http://www.doulos.com/knowhow/systemc/tlm2/.[2]OpenSystemCInitiative(OSCI):De ningandadvancingSystemCstandardIEEE1666-2005.http://www.systemc.org/.[3]Spinlanguagereference.http://spinroot.com/spin/Man/promela.html/.[4]Transaction-LevelModeling(TLM)2.0ReferenceManual.http://www.systemc.org/downloads/standards/.[5]RajeevAlurandDavidL.Dill.Atheoryoftimedautomata.Theor.Comput.Sci.,126(2):183Œ235,1994.[6]RajeevAlur,ThomasA.Henzinger,andPei-HsinHo.Automaticsymbolicveri cationofembeddedsystems.InProceedingsoftheReal-TimeSystemsSymposium.Raleigh-Durham,NC,December1993,pages2Œ11,1993.[7]KeithA.Bartlett,RogerA.Scantlebury,andPeterT.Wilkinson.Anoteonreliablefull-duplextransmissionoverhalf-duplexlinks.Commun.ACM,12(5):260Œ261,1969.[8]GerdBehrmann,PatriciaBouyer,EmmanuelFleury,andKimGuldstrandLarsen.Staticguardanalysisintimedautomataveri cation.InToolsandAlgorithmsfortheConstructionandAnalysisofSystems,9thInternationalConference,TACAS2003,HeldasPartoftheJointEuropeanConferencesonTheoryandPracticeofSoftware,ETAPS2003,Warsaw,Poland,April7-11,2003,Proceedings,pages254Œ277,2003.[9]GerdBehrmann,AlexandreDavid,andKimGuldstrandLarsen.Atutorialonuppaal.InBernardoandCorradini[12],pages200Œ236.[10]JohanBengtsson,KimGuldstrandLarsen,FredrikLarsson,PaulPettersson,andWangYi.UPPAAL-atoolsuiteforautomaticveri cationofreal-timesystems.InHybridSystemsIII:Veri cationandControl,ProceedingsoftheDIMACS/SYCONWorkshop,October22-25,1995,RuttgersUniversity,NewBrunswick,NJ,USA,pages232Œ243,1995.[11]JohanBengtssonandWangYi.Timedautomata:Semantics,algorithmsandtools.InLec-turesonConcurrencyandPetriNets,AdvancesinPetriNets[Thistutorialvolumeoriginatesfromthe4thAdvancedCourseonPetriNets,ACPN2003,heldinEichst¨att,Germanyin134September2003.InadditiontolecturesgivenatACPN2003,additionalchaptershavebeencommissioned],pages87Œ124,2003.[12]MarcoBernardoandFlavioCorradini,editors.FormalMethodsfortheDesignofReal-TimeSystems,InternationalSchoolonFormalMethodsfortheDesignofComputer,Communica-tionandSoftwareSystems,SFM-RT2004,Bertinoro,Italy,September13-18,2004,RevisedLectures,volume3185ofLectureNotesinComputerScience.Springer,2004.[13]G´erardBerry.Thefoundationsofesterel.InGordonD.Plotkin,ColinStirling,andMadsTofte,editors,Proof,Language,andInteraction,pages425Œ454.TheMITPress,2000.[14]NicolasBlancandDanielKroening.RaceanalysisforSystemCusingmodelchecking.ACMTransactionsonDesignAutomationofElectronicSystems,15(3):21:1Œ21:32,2010.[15]MariusBozga,Jean-ClaudeFernandez,andLucianGhirvu.Usingstaticanalysistoimproveautomatictestgeneration.InToolsandAlgorithmsforConstructionandAnalysisofSystems,6thInternationalConference,TACAS2000,HeldasPartoftheEuropeanJointConferencesontheTheoryandPracticeofSoftware,ETAPS2000,Berlin,Germany,March25-April2,2000,Proceedings,pages235Œ250,2000.[16]MariusBozga,SusanneGraf,IleanaOber,IulianOber,andJosephSifakis.Theiftoolset.InBernardoandCorradini[12],pages237Œ267.[17]V´ ctorA.Braberman,DiegoGarbervetsky,andAlfredoOlivero.Improvingtheveri!cationoftimedsystemsusingin"uenceinformation.InToolsandAlgorithmsfortheConstructionandAnalysisofSystems,8thInternationalConference,TACAS2002,HeldasPartoftheJointEuropeanConferenceonTheoryandPracticeofSoftware,ETAPS2002,Grenoble,France,April8-12,2002,Proceedings,pages21Œ36,2002.[18]JerryR.Burch,EdmundM.Clarke,KennethL.McMillan,DavidL.Dill,andL.J.Hwang.Symbolicmodelchecking:1020statesandbeyond.Inf.Comput.,98(2):142Œ170,1992.[19]GiorgioC.Buttazzo.HardReal-TimeComputingSystems.Springer,NewYork,USA,2011.[20]Yung-YuanChen,Chung-HsienHsu,andKuen-LongLeu.SoC-levelriskassessmentusingFMEAapproachinsystemdesignwithSystemC.InInternationalSymposiumonIndustrialEmbeddedSystems,pages82Œ89,2009.[21]AlessandroCimatti,AlbertoGriggio,AndreaMicheli,ImanNarasamdya,andMarcoRoveri.KRATOS:AsoftwaremodelcheckerforSystemC.InProceedingsofthe23rdInternationalConferenceonComputerAidedVeri cation(CAV),pages310Œ316,2011.135[22]ConradoDawsandSergioYovine.Reducingthenumberofclockvariablesoftimedau-tomata.InProceedingsofthe17thIEEEReal-TimeSystemsSymposium(RTSS™96),Decem-ber4-6,1996,Washington,DC,USA,pages73Œ81,1996.[23]RolfDrechslerandDanielGroße.Reachabilityanalysisforformalveri!cationofsystemc.In2002EuromicroSymposiumonDigitalSystemsDesign(DSD2002),Systems-on-Chip,4-6September2002,Dortmund,Germany,pages337Œ340,2002.[24]AliEbnenasir.AutomaticSynthesisofFaultTolerance.PhDthesis,MichiganStateUniver-sity,2005.[25]AliEbnenasir,RezaHajisheykhi,andSandeepS.Kulkarni.Facilitatingthedesignoffaulttoleranceintransactionlevelsystemcprograms.InDistributedComputingandNetwork-ing-13thInternationalConference,ICDCN2012,HongKong,China,January3-6,2012.Proceedings,pages91Œ105,2012.[26]AliEbnenasir,RezaHajisheykhi,andSandeepS.Kulkarni.Facilitatingthedesignoffaulttoleranceintransactionlevelsystemcprograms.Theor.Comput.Sci.,496:50Œ68,2013.[27]AntoniodaSilvaFarinaandSebasti´anS´anchezPrieto.Ontheuseofdynamicbinaryinstru-mentationtoperformfaultsinjectionintransactionlevelmodels.InProceedingsofthe2009FourthInternationalConferenceonDependabilityofComputerSystems,pages237Œ244,2009.[28]AlessandroFin,FrancoFummi,MaurizioMartignano,andMirkoSignoretto.SystemC:Ahomogenousenvironmenttotestembeddedsystems.InProceedingsoftheninthinterna-tionalsymposiumonHardware/softwarecodesign,CODES™01,pages17Œ22,2001.[29]BeltraGiovanni,CristianaBolchini,andAntonioMiele.Multi-levelfaultmodelingfortransaction-levelspeci!cations.InProceedingsofthe19thACMGreatLakessymposiumonVLSI,pages87Œ92,2009.[30]DanielGroßeandRolfDrechsler.Checkersforsystemcdesigns.In2ndACM&IEEEInter-nationalConferenceonFormalMethodsandModelsforCo-Design(MEMOCODE2004),23-25June2004,SanDiego,California,USA,Proceedings,pages171Œ178,2004.[31]DanielGroßeandRolfDrechsler.Checksyc:anef!cientpropertycheckerforRTLsystemcdesigns.InInternationalSymposiumonCircuitsandSystems(ISCAS2005),23-26May2005,Kobe,Japan,pages4167Œ4170,2005.[32]DanielGroße,UlrichK¨uhne,andRolfDrechsler.HW/SWco-veri!cationofaRISCCPUusingboundedmodelchecking.InSixthInternationalWorkshoponMicroprocessorTestand136Veri cation(MTV2005),CommonChallengesandSolutions,3-4November2005,Austin,Texas,USA,pages133Œ137,2005.[33]DanielGroße,UlrichK¨uhne,andRolfDrechsler.HW/SWco-veri!cationofembeddedsys-temsusingboundedmodelchecking.InProceedingsofthe16thACMGreatLakesSympo-siumonVLSI2006,Philadelphia,PA,USA,April30-May1,2006,pages43Œ48,2006.[34]AliHabibi,HajaMoinudeen,andSo!`eneTahar.Generating!nitestatemachinesfromsys-temc.InGeorgesG.E.Gielen,editor,DATEDesigners™Forum,pages76Œ81.EuropeanDesignandAutomationAssociation,Leuven,Belgium,2006.[35]AliHabibiandSo!`eneTahar.Anapproachfortheveri!cationofsystemcdesignsusingasml.InDoronPeledandYih-KuenTsay,editors,ATVA,volume3707ofLectureNotesinComputerScience,pages69Œ83.Springer,2005.[36]RezaHajisheykhi,AliEbnenasir,andSandeepS.Kulkarni.Modelingandanalyzingtimingfaultsintransactionlevelsystemcprograms.InStabilization,Safety,andSecurityofDis-tributedSystems-15thInternationalSymposium,SSS2013,Osaka,Japan,November13-16,2013.Proceedings,pages344Œ347,2013.[37]RezaHajisheykhi,AliEbnenasir,andSandeepS.Kulkarni.Modelingandanalyzingtimingfaultsintransactionlevelsystemcprograms.InNetworkonChipArchitectures,NoCArc™13,inconjunctionwiththe46thAnnualIEEE/ACMInternationalSymposiumonMicroarchitec-ture,MICRO-46,Davis,CA,USA,December7,2013,pages65Œ68,2013.[38]RezaHajisheykhi,AliEbnenasir,andSandeepS.Kulkarni.Analysisofpermanentfaultsintransactionlevelsystemcmodels.In34thInternationalConferenceonDistributedComput-ingSystemsWorkshops(ICDCS2014Workshops),Madrid,Spain,June30-July3,2014,pages154Œ160,2014.[39]RezaHajisheykhi,AliEbnenasir,andSandeepS.Kulkarni.EvaluatingtheeffectoffaultsinsystemcTLMmodelsusingUPPAAL.InSoftwareEngineeringandFormalMethods-12thInternationalConference,SEFM2014,Grenoble,France,September1-5,2014.Proceedings,pages175Œ189,2014.[40]RezaHajisheykhi,AliEbnenasir,andSandeepS.Kulkarni.UFIT:AtoolformodelingfaultsinUPPAALtimedautomata.InNASAFormalMethods-7thInternationalSymposium,NFM2015,Pasadena,CA,USA,April27-29,2015,Proceedings,pages429Œ435,2015.[41]RezaHajisheykhi,MohammadRoohitavaf,AliEbnenasir,andSandeepS.Kulkarni.Aframeworkforveri!cationofSystemCTLMprogramswithmodelslicing:Acasestudy.In137TobeappearedDesignAutomationConference-53rdACM/EDAC/IEEE,DAC2016,Austin,TX,USA,June5-9,2016,Proceedings,2016.[42]NicolasHalbwachs,FabienneLagnier,andChristopheRatel.Programmingandverifyingreal-timesystemsbymeansofthesynchronousdata-"owlanguagelustre.IEEETrans.Soft-wareEng.,18(9):785Œ793,1992.[43]NesrineHarrathandBrunoMonsuez.Systemcwaitingstateautomata.IJCCBS,3(1/2):60Œ95,2012.[44]IanG.Harris.Faultmodelsandtestgenerationforhardware-softwarecovalidation.IEEEDesignandTestofComputers,20(4):40Œ47,2003.[45]JohnHatcliff,MatthewB.Dwyer,andHongjunZheng.Slicingsoftwareformodelconstruc-tion.Higher-OrderandSymbolicComputation,13(4):315Œ353,2000.[46]ThomasA.Henzinger,XavierNicollin,JosephSifakis,andSergioYovine.Symbolicmodelcheckingforreal-timesystems.Inf.Comput.,111(2):193Œ244,1994.[47]PaulaHerber,MarcelPockrandt,andSabineGlesner.Transformingsystemctransactionlevelmodelsintouppaaltimedautomata.InSatnamSingh,BarbaraJobstmann,MichaelKishinevsky,andJensBrandt,editors,MEMOCODE,pages161Œ170.IEEE,2011.[48]G.J.Holzmann.ThemodelcheckerSPIN.IEEETransactionsonSoftwareEngineering,23(5):279Œ295,May1997.[49]RavishankarK.Iyer,DavidJ.Rossetti,andMei-ChenHsueh.Measurementandmodelingofcomputerreliabilityasaffectedbysystemactivity.ACMTrans.Comput.Syst.,4(3):214Œ237,1986.[50]AgataJanowskaandPawelJanowski.Slicingtimedsystems.Fundam.Inform.,60(1-4):187Œ210,2004.[51]AgataJanowskaandPawelJanowski.Slicingoftimedautomatawithdiscretedata.Fundam.Inform.,72(1-3):181Œ195,2006.[52]DanielKarlsson,PetruEles,andZeboPeng.Formalveri!cationofsystemcdesignsusingapetri-netbasedrepresentation.InDATE,pages1228Œ1233,2006.138[53]DanielKroeningandNatashaSharygina.Formalveri!cationofsystemcbyautomatichard-ware/softwarepartitioning.InACM&IEEEInternationalConferenceonFormalMethodsandModelsforCo-Design(MEMOCODE),pages101Œ110,2005.[54]S.S.KulkarniandA.Arora.Automatingtheadditionoffault-tolerance.InFormalTech-niquesinReal-TimeandFault-TolerantSystems,pages82Œ93,London,UK,2000.Springer-Verlag.[55]SudiptaKundu,MalayGanai,andRajeshGupta.PartialorderreductionforscalabletestingofSystemCTLMdesigns.InProceedingsofthe45thannualDesignAutomationConference,DesignAutomationConference,pages936Œ941,2008.[56]K.G.Larsen,P.Pettersson,andW.Yi.Uppaalinanutshell.InternationalJournalonSoftwareToolsforTechnologyTransfer(STTT),1(1-2):134Œ152,1997.[57]ChrisLattnerandVikramS.Adve.LLVM:ACompilationFrameworkforLifelongProgramAnalysis&Transformation.InIEEE/ACMInternationalSymposiumonCodeGenerationandOptimization(CGO),pages75Œ88,2004.[58]HoangM.Le,DanielGroße,andRolfDrechsler.Automatictlmfaultlocalizationforsys-temc.IEEETrans.onCADofIntegratedCircuitsandSystems,31(8):1249Œ1262,2012.[59]KaL.Man.Formalcommunicationsemanticsofsystemc".InEighthEuromicroSymposiumonDigitalSystemsDesign(DSD2005),30August-3September2005,Porto,Portugal,pages338Œ345,2005.[60]KaLokMan,AndreaFedeli,MicheleMercaldi,MenouerBoubekeur,andMichelP.Schellekens.SC2SCFL:automatedsystemctosystemc"translation.InEmbeddedComputerSystems:Architectures,Modeling,andSimulation,7thInternationalWorkshop,SAMOS2007,Samos,Greece,July16-19,2007,Proceedings,pages34Œ45,2007.[61]K.Marquet,B.Jeannet,andM.Moy.Ef!cientEncodingofSystemC/TLMinPromela.TechnicalReportTR-2010-7,Verimag,France,2010.[62]KevinMarquetandMatthieuMoy.PinaVM:ASystemCfront-endbasedonanexecutableintermediaterepresentation.InInternationalconferenceonEmbeddedsoftware(EMSOFT),pages79Œ88,2010.[63]LynetteI.MillettandTimTeitelbaum.IssuesinslicingPROMELAanditsapplicationstomodelchecking,protocolunderstanding,andsimulation.STTT,2(4):343Œ349,2000.139[64]SilvioMisera,HeinrichTheodorVierhaus,andAndreSieber.FaultinjectiontechniquesandtheiracceleratedsimulationinSystemC.InProceedingsofthe10thEuromicroConferenceonDigitalSystemDesignArchitectures,MethodsandTools,pages587Œ595,2007.[65]M.Moy.TechniquesandToolsfortheVeri cationofSystems-on-a-ChipattheTransactionLevel.PhDthesis,INPG,Grenoble,France,2005.[66]MatthieuMoy,FlorenceMaraninchi,andLaurentMaillet-Contoz.Lussy:Atoolboxfortheanalysisofsystems-on-a-chipatthetransactionallevel.InInternationalConferenceonApplicationofConcurrencytoSystemDesign(ACSD),pages26Œ35,2005.[67]WolfgangM¨uller,J¨urgenRuf,andWolfgangRosenstiel.SystemC:MethodologiesandAp-plications,chapterAnASMbasedSystemCSimulationSemantics.KluwerAcademicPub-lishers,2003.[68]B.NiemannandCh.Haubelt.FormalizingTLMwithCommunicatingStatMachines.InProceedingsofForumonSpeci cationandDesignLanguages2006(FDL2006),pages285Œ292,2006.[69]HirenD.PatelandSandeepK.Shukla.Model-drivenvalidationofSystemCdesigns.EURASIPJournalonEmbeddedSystems-C-BasedDesignofHeterogeneousEmbeddedSystems,2008:4:1Œ4:14,January2008.[70]JonPerez,MikelAzkarate-askasua,andAntonioPerez.Codesignandsimulatedfaultinjec-tionofsafety-criticalembeddedsystemsusingSystemC.InProceedingsofthe2010Euro-peanDependableComputingConference,pages221Œ229,2010.[71]VenkateshPrasadRanganathandJohnHatcliff.Slicingconcurrentjavaprogramsusingindusandkaveri.STTT,9(5-6):489Œ504,2007.[72]J¨urgenRuf,DirkW.Hoffmann,JoachimGerlach,ThomasKropf,WolfgangRosenstiel,andWolfgangM¨uller.Thesimulationsemanticsofsystemc.InDATE,pages64Œ70,2001.[73]AshrafSalem.Formalsemanticsofsynchronoussystemc.In2003Design,AutomationandTestinEuropeConferenceandExposition(DATE2003),3-7March2003,Munich,Germany,pages10376Œ10381,2003.[74]AlperSen.MutationoperatorsforconcurrentSystemCdesigns.InInternationalWorkshoponMicroprocessorTestandVeri cation,2000.140[75]RishadAhmedSha!k,PaulRosinger,andBashirM.Al-Hashimi.SystemC-basedminimumintrusivefaultinjectiontechniquewithimprovedfaultrepresentation.InProceedingsofthe200814thIEEEInternationalOn-LineTestingSymposium,pages99Œ104,2008.[76]DonaldE.Thomas,ElizabethD.Lagnese,JohnA.Nestor,JayanthV.Rajan,RobertL.Black-burn,andRobertA.Walker.AlgorithmicandRegister-TransferLevelSynthesis:TheSystemArchitect™sWorkbench.KluwerAcademicPublishers,Norwell,MA,USA,1989.[77]ClausTraulsen,JeromeCornet,MatthieuMoy,andFlorenceMaraninchi.ASystemC/TLMsemanticsinPromelaanditspossibleapplications.InSPINWorkshop,pages204Œ222,2007.[78]MarkWeiser.Programslicing.IEEETrans.SoftwareEng.,10(4):352Œ357,1984.141