时间符号迁移图及其互模拟判定
文献类型:期刊论文
作者 | 陈靖 ; 林惠民 |
刊名 | 计算机学报
![]() |
出版日期 | 2002 |
卷号 | 25期号:2页码:113-121 |
关键词 | 并发 实时系统 数据传送 互模拟 时间符号迁移图 concurrency real-time system value-passing bisimulation timed symbolic transition graph |
ISSN号 | 0254-4164 |
其他题名 | timed bisimulation over timed symbolic transition graph |
中文摘要 | 引入时间符号迁移图的概念,作为既涉及通讯又具有实时性的并发系统的模型。该文给出了这种迁移图时间互模拟的算法,并证明了该算法的正确性。 |
收录类别 | ei,wanfang,cscd |
资助信息 | National Natural Science Foundation of China; Public Administration and Civil Service Bureau of Macau SAR; Companhia de Telecomunicacoes de Macau S.A.R.L.; Macau SAR Government Tourist Office |
语种 | 中文 |
公开日期 | 2010-08-24 |
附注 | A new modeling language, Timed Symbolic Transition Graph (TSTG), is introduced which can characterize both real-time and value-passing systems. An algorithm checking the timed bisimulation between TSTGs is presented. Traditionally, Labeled Transition System (LTS) is used to characterize the behavior of systems with states connected by directed edges labeled by some actions. Since LTSs do not contain variables, they are not suitable for explicit manipulation of data transfer between systems. In this paper, we use TSTG to model value-passing processes where processes can communicate with each other by exchanging messages (data) via channels. Another capability of TSTG is that it can model real-time processes. To model the behavior of real-time processes, it uses some clock variables with values ranging over non-negative real numbers, where all the clocks will increment at the same speed in order to model time elapse. As value-passing systems and real-time systems are studied separately generally, TSTG is the first modeling language which can model such mixed systems under the unified framework. Bisimulation checking is a very important method in automatic verification of software and hardware systems, where timed bisimulation is a kind of equivalence relation between real-time systems. In this work, we present an algorithm for the timed bisimulation checking between TSTGs together with its correctness proof. |
源URL | [http://124.16.136.157/handle/311060/4460] ![]() |
专题 | 软件研究所_计算机科学国家重点实验室 _期刊论文 |
推荐引用方式 GB/T 7714 | 陈靖,林惠民. 时间符号迁移图及其互模拟判定[J]. 计算机学报,2002,25(2):113-121. |
APA | 陈靖,&林惠民.(2002).时间符号迁移图及其互模拟判定.计算机学报,25(2),113-121. |
MLA | 陈靖,et al."时间符号迁移图及其互模拟判定".计算机学报 25.2(2002):113-121. |
入库方式: OAI收割
来源:软件研究所
浏览0
下载0
收藏0
其他版本
除非特别说明,本系统中所有内容都受版权保护,并保留所有权利。