| Budget Amount *help |
¥7,900,000 (Direct Cost: ¥7,900,000)
Fiscal Year 2004: ¥5,700,000 (Direct Cost: ¥5,700,000)
Fiscal Year 2003: ¥2,200,000 (Direct Cost: ¥2,200,000)
|
|---|
| Research Abstract |
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.
|
