资源描述：
《model checking prioritized timed automata》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。
1、ModelCheckingPrioritizedTimedAutomataShang-WeiLin,Pao-AnnHsiung,Chun-HsianHuang,andYean-RuChenDepartmentofComputerScienceandInformationEngineering,NationalChungChengUniversity,Chiayi,Taiwan−621,ROChpa@computer.orgAbstract.Prioritiesareoftenusedtoresolveconflictsintimedsystems.How-ev
2、er,prioritiesarenotdirectlysupportedbystate-of-artmodelcheckers.Often,adesignerhastoeitherabstracttheprioritiesleadingtoahighdegreeofnon-determinismormodeltheprioritiesusingexistingprimitives.Inthiswork,itisshownhowprioritizedtimedautomatacanmakemodellingprioritizedtimedsys-temseas
3、ierthroughthesupportforpriorityspecificationandmodelchecking.Theverificationofprioritizedtimedautomatarequiresasubtractionoperationtobeperformedontwoclockzones,representedbyDBMs,forwhichweproposeanalgorithmtogeneratetheminimalnumberofzonespartitioned.Aftertheappli-cationofaseriesofDB
4、Msubtractionoperations,thenumberofzonesgeneratedbecomelarge.Wethusproposeanalgorithmtoreducethefinalnumberofzonespartitionedbymergingsomeofthem.Atypicalbusarbitrationexampleisusedtoillustratethebenefitsoftheproposedalgorithms.Duetothesupportforprioriti-zationandzonereduction,weobserv
5、ethatthereisa50%reductioninthenumberofmodesand44%reductioninthenumberoftransitions.Keywords:Prioritizedtimedautomata,DBMsubtraction,zonemerging,zonereduction.1IntroductionConcurrencyresultsinconflictswhenresourcesaresharedsuchastwoormoreprocess-estryingtousethesameprocessororthesame
6、peripheraldeviceinreal-timeembeddedsystems.Toresolvesuchconflicts,scheduling,synchronization,andarbitrationaresomewell-knownsolutionsthathavebeenpopularlyusedinoperatingsystemsandinhardwaredesigns.Acommonartifactofthesesolutionsistheprioritizationofcontendingparties.Alowpriorityproc
7、essisallowedtoexecuteonlywhenallprocesseswithhigherprioritiesaredisabled.Systemmodelsusedfordesignandverificationsuchastimedautomata,statecharts,andothersallownon-determinismswhichariseoutofconcurrency,interleaving,andin-formationhiding.However,non-determinismsoftenresultinunmanagea
8、blylargestate-spaces.Prior
