Research on an efficient analysis method of real-time software based on a level oriented net model
| Project/Area Number |
15300009
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (B)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
Software
|
|---|
| Research Institution | National Institute of Informatics |
|---|
Principal Investigator |
YONEDA Tomohiro National Institute of Informatics, Infrastructure Systems Research Division, Professor, 情報基盤研究系, 教授 (30182851)
|
|---|
| Project Period (FY) |
2003 – 2004
|
| Project Status |
Completed (Fiscal Year 2004)
|
| 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)
|
|---|
| Keywords | Level Time Petri net / Partial order reduction / Hierarchical verification / Real time software / Timed automaton / 形式的検証 / レベルタイムペトリネット |
|---|
| 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.
|
Report
(3 results)
Research Products
(8 results)
