| 基于TLA的时序规约及TLC模型检测 |
| |
| 引用本文： | 张珺铭,王扣武,计伟.基于TLA的时序规约及TLC模型检测[J].贵阳学院学报(自然科学版),2015,10(2). |
| |
| 作者姓名： | 张珺铭 王扣武 计伟 |
| |
| 作者单位： | 1. 贵州建设职业技术学院,贵州贵阳,551400
2. 中国电建集团贵阳勘测设计研究院有限公司,贵州贵阳,550081 |
| |
| 摘 要： | 生产者与消费者系统(PCS)是一个经典的进程同步问题,Hocine等学者运用抽象状态机(ASMs)对该问题进行了时序规约.文中主要使用TLA语言对PCS给出了一个时序规约模型,并且利用模型检测工具TLC对PCS进行检测.同时对系统的活性和互斥性也进行了检测,检测结果都满足系统规约.ASMs主要采用转移规则来规约PCS模型,中间的转移过程是无法知道的,TLA能同时规约出PCS的执行过程和系统属性.
|
| 关 键 词： | 生产者与消费者系统(PCS) TLA 规约 TLA+ TLC |
Based on the temporal specification of TLA and TLC model checking |
| |
| ZHANG Jun-ming,WANG Kou-wu,JI Wei.Based on the temporal specification of TLA and TLC model checking[J].Journal of Guiyang College:Natural Science,2015,10(2). |
| |
| Authors: | ZHANG Jun-ming WANG Kou-wu JI Wei |
| |
| Abstract: | |
| |
| Keywords: | |
| 本文献已被 万方数据 等数据库收录！ |
|
