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

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

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.