| 时间自动机的事务级形式验证 |
| |
| 引用本文： | 阿米拉里高弗兰尼, 法特穆加瓦河瑞, 哈米德诺瑞, 在那拉贝定纳瓦比.时间自动机的事务级形式验证[J].上海师范大学学报(自然科学版),2010,39(5). |
| |
| 作者姓名： | 阿米拉里高弗兰尼 法特穆加瓦河瑞 哈米德诺瑞 在那拉贝定纳瓦比 |
| |
| 作者单位： | 德黑兰大学电子计算机工程系 |
| |
| 摘 要： | 提出了一种形式方法用于验证TLM-2.0的设计方案.该方法中TLM-2.0设计方案将被转换成定时自动机形式模型.定义若干种属性,验证将根据这些属性执行,并引入一种模拟事务级设计方案差错的故障模型来评估这些属性.然后这些属性通过使用形式UPPAAL验证工具在系统的定时自动机表示上针对这些故障被验证.最后通过一个实例研究说明该方法的有效性.
|
| 关 键 词： | 形式验证 定时自动机 事务级模型 UPPAAL |
Transaction level formal verification using Timed Automata |
| |
| Amirali Ghofrani,Fatemeh Javaheri,Hamid Noori,Zainalabedin Navabi.Transaction level formal verification using Timed Automata[J].Journal of Shanghai Normal University(Natural Sciences),2010,39(5). |
| |
| Authors: | Amirali Ghofrani Fatemeh Javaheri Hamid Noori Zainalabedin Navabi |
| |
| Abstract: | In this paper a formal methodology is proposed to verify TLM-2.0 designs.In this approach TLM-2.0 designs are translated into Timed Automata formal model.Several properties are defined by which the verification will be performed and a fault model is introduced to evaluate these properties,which mimics the transaction level design errors.The properties are then verified on the Timed Automata representation of the system against the faults using the formal verifier of the UPPAAL tool.The efficiency of the approach is illustrated by a case study. |
| |
| Keywords: | formal verification timed automata transaction level modeling UPPAAL |
| 本文献已被 万方数据 等数据库收录！ |
| 点击此处可从《上海师范大学学报(自然科学版)》浏览原始摘要信息 |
| 点击此处可从《上海师范大学学报(自然科学版)》下载免费的PDF全文 |
