In this paper an event-based operational interleaving semantics is proposed for real-time processes, for which action refinement and a denotational true concurrency semantics are developed and defined in terms of time...In this paper an event-based operational interleaving semantics is proposed for real-time processes, for which action refinement and a denotational true concurrency semantics are developed and defined in terms of timed event structures. The authors characterize the timed event traces that are generated by the operational semantics in a denotational way, and show that this operational semantics is consistent with the denotational semantics in the sense that they generate the same set of timed event traces, thereby eliminating the gap between the true concurrency and interleaving semantics. Keywords action refinement - real-time process algebra - semantics - timed event structure - formal method This work was supported by the National Natural Science Foundation of China (Grant No. 60373113) and the “Hundred-Talent Program” of Chinese Academy of Sciences.Xiu-Li Sun was born in 1975. She received her B.S. degree in 1998 and M.S. degree in 2002 from Taiyuan University of Technology, Shanxi. She is studying in the Institute of Computer Application, Chengdu for her doctorate.Wen-Ying Zhang was born in 1972. Now he is a Ph.D. candidate of Computer Application, the Chinese Academy of Sciences. His current research interests include formal verification, digital watermarking and pattern recognition.Jin-Zhao Wu was born in 1965. He obtained his Ph.D. degree in 1994 from the Institute of System Science, CAS. From 1994 to 1999 he was a postdoctoral researcher. His research interests include formal specification and verification, automatic reasoning, logic programming.展开更多
文摘In this paper an event-based operational interleaving semantics is proposed for real-time processes, for which action refinement and a denotational true concurrency semantics are developed and defined in terms of timed event structures. The authors characterize the timed event traces that are generated by the operational semantics in a denotational way, and show that this operational semantics is consistent with the denotational semantics in the sense that they generate the same set of timed event traces, thereby eliminating the gap between the true concurrency and interleaving semantics. Keywords action refinement - real-time process algebra - semantics - timed event structure - formal method This work was supported by the National Natural Science Foundation of China (Grant No. 60373113) and the “Hundred-Talent Program” of Chinese Academy of Sciences.Xiu-Li Sun was born in 1975. She received her B.S. degree in 1998 and M.S. degree in 2002 from Taiyuan University of Technology, Shanxi. She is studying in the Institute of Computer Application, Chengdu for her doctorate.Wen-Ying Zhang was born in 1972. Now he is a Ph.D. candidate of Computer Application, the Chinese Academy of Sciences. His current research interests include formal verification, digital watermarking and pattern recognition.Jin-Zhao Wu was born in 1965. He obtained his Ph.D. degree in 1994 from the Institute of System Science, CAS. From 1994 to 1999 he was a postdoctoral researcher. His research interests include formal specification and verification, automatic reasoning, logic programming.
