时间自动机的事务级形式验证(英文)

Transaction level formal verification using Timed Automata

提出了一种形式方法用于验证TLM-2.0的设计方案.该方法中TLM-2.0设计方案将被转换成定时自动机形式模型.定义若干种属性,验证将根据这些属性执行,并引入一种模拟事务级设计方案差错的故障模型来评估这些属性.然后这些属性通过使用形式UPPAAL验证工具在系统的定时自动机表示上针对这些故障被验证.最后通过一个实例研究说明该方法的有效性.

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.