Research on an efficient analysis method of real-time software based on a level oriented net model

基于面向层次网络模型的实时软件高效分析方法研究

• 批准号: 15300009
• 负责人: YONEDA Tomohiro
• 金额: $ 5.06万
• 依托单位: National Institute of Informatics
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (B)
• 财政年份: 2003
• 资助国家: 日本
• 起止时间: 2003 至 2004
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-15300009/
• 关键词: Level Time Petri net; Partial order reduction; Hierarchical verification; Real time software; Timed automaton; 形式的検証; レベルタイムペトリネット

It is well known that a timed automaton is a formal model for real-time systems which is level oriented and has rich expressiveness. Our experience, however, has found that its generality comes at an increase in analysis complexity, and this increased generality is not always necessary for verifying some class of real-time, systems. Thus, this work has tackled the challenge to develop an efficient tool based on a simpler model with still sufficient expressiveness.In the first step of this work, a new formal model has been obtained by extending the time Petri net model with preserving the simplicity of its analysis. In this new model called LTN (Level Time Petri net), firing an LTN transition can assign values to a set of boolean variables, and the validity of an expression over the boolean variables is also used as an enabling condition of an LTN transition in addition to the marking. Next, its efficient analysis procedure based on the partial order reduction has been developed and an prototype for it has been implemented. This algorithm also has an ability of verifying systems hierarchically, which sometimes reduces the average complexity of the verification of large systems. To demonstrate this ability, a little large case study for verifying the instruction cache mechanism of TITAC 2 asynchronous microprocessor has been done. Through the case study, the hierarchical verification technique has been evaluated. Finally, we have designed a graphical user interface (GUI) for especially supporting the hierarchical verification steps, and a verification tool VINAS-P(Ver.2) with it has been developed.

时间自动机是一种面向层次的、具有丰富表达能力的实时系统形式化模型。然而，我们的经验发现，它的一般性是在分析复杂性的增加，这种增加的一般性并不总是必要的验证某些类的实时系统。因此，这项工作已经解决的挑战，开发一个有效的工具，一个更简单的模型的基础上仍然有足够的expressions.In在这项工作的第一步，一个新的形式化模型已通过扩展的时间Petri网模型，保持其分析的简单性。在这个新的模型LTN（Level Time Petri net）中，触发LTN变迁可以为一组布尔变量赋值，并且除了标记之外，布尔变量上的表达式的有效性也被用作LTN变迁的启用条件。其次，它的有效的分析程序的基础上的偏序约简已被开发和原型已经实现。该算法还具有分层验证系统的能力，这有时会降低大型系统验证的平均复杂度。为了证明这种能力，我们进行了一个大型案例研究来验证TITAC 2异步微处理器的指令缓存机制。通过案例研究，对层次验证技术进行了评价。最后，我们设计了一个图形用户界面（GUI），特别是支持分层验证步骤，并与它的验证工具VINAS-P（Ver.2）已被开发。

项目成果

Partial Order Reduction for Timed Circuit Verification Based on a Level Oriented Model

基于面向水平模型的定时电路验证的偏阶约简

• 发表时间: 2003
• 期刊: 電子情報通信学会英文論文誌 Vol.E86-D
• 作者: Tomoya Kitai

Tomoya Kitai, Yusuke Oguro, Tomohiro Yoneda, Eric Mercer, Chris Myers: "Partial Order Reduction for Timed Circuit Verification Based on a Level Oriented Model"電子情報通信学会英文論文誌. E86D・12. 2601-2611 (2003)

Tomoya Kitai、Yusuke Oguro、Tomohiro Yoneda、Eric Mercer、Chris Myers：“基于面向水平模型的定时电路验证的部分阶次减少”IEICE 英文期刊，2601-2611（2003 年）。

Partial order Reduction for Detecting Safety and Timing Failures of Timed Circuits

用于检测定时电路的安全性和定时故障的偏序减少

• 期刊: 電子情報通信学会英文論文誌 (印刷中)
• 作者: Tomoya Kitai;Yusuke Oguro;Tomohiro Yoneda;Eric Mercer;Chris Myers;Denduang Pradubsuwun
• 通讯作者: Denduang Pradubsuwun

Failure Trace analysis of Timed Circuits for Automatic Timing Constraints Derivation

用于自动时序约束推导的定时电路的故障跟踪分析

• 期刊: 電子情報通信学会英文論文誌 (印刷中)
• 作者: Tomoya Kitai;Yusuke Oguro;Tomohiro Yoneda;Eric Mercer;Chris Myers;Denduang Pradubsuwun;Tomoya Kitai
• 通讯作者: Tomoya Kitai