资源描述：
《A Logic to Specify and Verify Synchronous Transitions》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。
1、ALogictoSpecifyandVerifySynchronousTransitionsVanderleiMoraesRodriguesFl´avioRechWagnerInstitutodeInform´atica,UFRGSPortoAlegre,RS,Brazilfvandi,flaviog@inf.ufrgs.brAbstractThispaperintroducesaformalismnamedSINCaimedatthedesignandverificationofsynchronousconcurre
2、ntsystems.Thecomponentsofthisformalismareatransitionsystemandafirst-orderlinear-timetemporallogic.TheSINCtransitionsystemadoptsasynchronouscomputationmodel,includesamethodtosolvewrite-conflicts,andrepresentstransitionsaspossiblynon-terminatingimperativecommands.Th
3、eSINClogicallowsforformalreasoningaboutSINCtransitionsystemsusingcompositionalandmodularproofs.Suchfeaturesareimportanttotheverificationofalargeclassofsystems,buttheyaremissinginotherformalismsbasedontransitionsystemsandtemporallogics.Thispaperalsodiscussessomeof
4、thepragmaticsinspecifyingandverifyingsystemsusingSINC,andpresentsextensionstodealwithgenericparametersandregularstructures.SINCisbasedontheHoarelogicandtheUNITYformalism.1IntroductionTheclassofformalismscomposedofatransitionsystemandafirst-orderlinear-timetempora
5、llogicincludestheMannaandPnuelilogic[17,18],TLA[16],UNITY[8,20],ST[29],andotherformalisms[25,28].Duetotheirexpressivenessandflexibility,theyhavebeensuccessfullyemployedinthedescriptionandverificationofconcurrentorreactivesystemsinseveralapplicationfields.However,th
6、eseformalismsdealwithasynchronoussystemsmostly.Adistinctclassofcomputationalsystemsisthatofsynchronoussystems.ItincludesprogramminglanguagessuchasEsterel[2],hardwaredescriptionlanguagessuchasVHDL[22],andspecificationformalismssuchasevolvingalgebras[12,13,14].Work
7、sontheverificationofsuchsystemseitherexplorerestrictedtechniquessuchasfinitemodel-checkers,ordependonidiosyncrasiesofaparticularnotation,orarenotmatureyet.ThispaperintroducesaformalismnamedSINCaimedatthedescriptionandverificationofsynchronoussystemsusingatransition
8、systemandafirst-orderlinear-timetemporallogic.Besidesthesynchronouscomputationmodel,othersalientfeaturesofSINCarearepresentationfortransitionsas(possiblynon-terminatin
