摘要
FiniteChuspacesareproposedforthemodelingandverificationofconcurrentprograms.Inordertomodelnotonlytypicalconcurrentbehaviorsbutalsomodernexceptionhandlingandsynchronizationmechanisms,wedesignanenrichedprocessalgebraofChuspacesfromapracticalpointofview.ToillustratethepoweroffiniteChuspacesandtheprocessalgebrawhileabstractingawayfromlanguage-specificdetails,animaginaryconcurrentprogramminglanguage(ICL)isdesigned.AdenotationalsemanticsofICLispresentedusingfiniteChuspacesandtheenrichedprocessalgebra.Thevaluationfunctionsarefairlystraightforwardsincethecarefullydesignedoperatorshavedonemuchofthejob.TheenrichedprocessalgebraisalsousedasthespecificationlanguageforChuspaces,withwhichprocess-algebraicpropertiescanbespecified.Verificationalgorithmsarepresentedwiththeirtimecomplexitiesdiscussed.
出版日期
2010年06月16日（中国期刊网平台首次上网日期，不代表论文的发表时间）
