Event-based operational semantics and a consistency result for real-time concurrent processes with action refinement

被引:2
作者
Sun, XL [1 ]
Zhang, WY
Wu, JZ
机构
[1] Chinese Acad Sci, Chengdu Inst Comp Applicat, Chengdu 610041, Peoples R China
[2] Univ Mannheim, Fak Math & Informat, D-68131 Mannheim, Germany
基金
中国国家自然科学基金;
关键词
action refinement; real-time process algebra; semantics; timed event structure; formal method;
D O I
10.1007/BF02973446
中图分类号
TP3 [计算技术、计算机技术];
学科分类号
0812 ;
摘要
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.
引用
收藏
页码:828 / 839
页数:12
相关论文
共 24 条
[1]  
Baier C, 1998, LECT NOTES COMPUT SC, V1443, P568, DOI 10.1007/BFb0055085
[2]   THE CONNECTION BETWEEN AN EVENT STRUCTURE SEMANTICS AND AN OPERATIONAL SEMANTICS FOR TCSP [J].
BAIER, C ;
MAJSTERCEDERBAUM, ME .
ACTA INFORMATICA, 1994, 31 (01) :81-104
[3]  
Boudol G., 1988, Fundamenta Informaticae, V11, P433
[4]   FLOW MODELS OF DISTRIBUTED COMPUTATIONS - 3 EQUIVALENT SEMANTICS FOR CCS [J].
BOUDOL, G ;
CASTELLANI, I .
INFORMATION AND COMPUTATION, 1994, 114 (02) :247-314
[5]  
BOWMAN H, 1998, P INT C APPL CONC SY, P229
[6]   Bundle event structures: A revised cpo approach [J].
Fecher, H ;
Majster-Cederbaum, M ;
Wu, JZ .
INFORMATION PROCESSING LETTERS, 2002, 83 (01) :7-12
[7]  
Fecher H., 2002, Process Algebra and Probabilistic Methods. Performance Modeling and Verification. Second Joint International Workshop PAPM-PROBMIV 2002 Proceedings (Lecture Notes in Computer Science Vol.2399), P77
[8]  
FECHER H, 2002, ELECT NOTES THEORETI, V70
[9]  
Gorrieri Roberto, 2001, HDB PROCESS ALGEBRA, P1047
[10]   A consistent causality-based view on a timed process algebra including urgent interactions [J].
Katoen, JP ;
Langerak, R ;
Brinksma, E ;
Latella, D ;
Bolognesi, T .
FORMAL METHODS IN SYSTEM DESIGN, 1998, 12 (02) :189-216