| Verifying Automata Specification of Distributed Probabilistic Real-Time Systems |
| |
| 引用本文： | Luo Tiegeng,Chen Huowang,Wang Bingshan,Wang Ji,Gong Zhenghu,Qi Zhichang. Verifying Automata Specification of Distributed Probabilistic Real-Time Systems[J]. 计算机科学技术学报, 1998, 13(6): 588-596. DOI: 10.1007/BF02946502 |
| |
| 作者姓名： | Luo Tiegeng Chen Huowang Wang Bingshan Wang Ji Gong Zhenghu Qi Zhichang |
| |
| 作者单位： | [1]DepartmentofComputerScience,NationalUniversityofDerenseTechnologyChangsha410073,P,R.China [2]Departmento,NationalUniversityofDerenseTechnologyChangsha410073,P,R.China |
| |
| 摘 要： | In this paper,a qualitative model checking algorithm for verification of distributed probabilistic real-time systems(DPRS)is presented.The model of DPRS,called real-time proba bilistic process model(RPPM),is over continuous time domain.The properties of DPRS are described by using deterministic timed automata(DTA).The key part in the algorithm is to map continuous time to finite time intervals with flag variables.Compared with the existing algorithms,this algorithm uses more general delay time equivalence classes instead of the unit delay time equivalence classes restricted by event sequence,and avoids generating the equivalence classes of states only due to the passage of time.The result shows that this algorithm is cheaper.
|
| 关 键 词： | 计算机网络 自动化检验 实时系统 |
Verifying automata specification of distributed probabilistic real-time systems |
| |
| Tiegeng Luo,Huowang Chen,Bingshan Wang,Ji Wang,Zhenghu Gong,Zhichang Qi. Verifying automata specification of distributed probabilistic real-time systems[J]. Journal of Computer Science and Technology, 1998, 13(6): 588-596. DOI: 10.1007/BF02946502 |
| |
| Authors: | Tiegeng Luo Huowang Chen Bingshan Wang Ji Wang Zhenghu Gong Zhichang Qi |
| |
| Affiliation: | (1) Department of Computer Science, National University of Defense Technology, 410073 Changsha, P.R. China |
| |
| Abstract: | In this paper, a qualitative model checking algorithm for verification of distributed probabilistic real-time systems (DPRS) is presented. The model of DPRS, called real-time probabilistic process model (RPPM), is over continuous time domain. The properties of DPRS aredescribed by using deterministic timed automata (DTA). The key part in the algorithm is tomap continuous time to finite time intervals with flag variables. Compared with the existingalgorithms, this algorithm uses more general delay time equivalence classes instead of the unitdelay time equivalence classes restricted by event sequence, and avoids generating the equivalence classes of states only due to the passage of time. The result shows that this algorithm ischeaper. |
| |
| Keywords: | DPRS GSMP automatic verification model checking timed automata. |
| 本文献已被 CNKI 维普 SpringerLink 等数据库收录！ |
| 点击此处可从《计算机科学技术学报》浏览原始摘要信息 |
|
点击此处可从《计算机科学技术学报》下载免费的PDF全文 |
