Abstract Model Checking and Its Applications.
|
Accession number;03A0714597
|
| Title;Abstract Model Checking and Its Applications. |
| Author;
HAGIYA MASAMI
(Univ. Tokyo, Graduate School, JPN)
|
Journal Title;Abstract Model Checking and Its Applications
|
Journal Code:N20031880
|
ISSN:
|
|
VOL.;NO.;PAGE.317P(2002)
|
| Figure&Table&Reference;FIG.61, TBL.28, REF.326 |
| Pub. Country;Japan |
| Language;Japanese |
| Abstract;Though the correctness verification of the information processing system mainly on the computer ( of the following, calculation system )was the field studied from old, the application of the computer would reach every corner of social life, and it became a problem in which to exactly guarantee the accuracy of the calculation system was more important. Especially, it is urgent to guarantee the security on the network by internet's popularization and progress of the electron money technology. Correctness verification of the security protocol is a very important research theme, and the validation technique using the computer is indispensable. There are two methods for verification, and one is a proof base method by the proof support system. Another is a method for verifying the accuracy of the calculation system without any human intervention by the combinative search of the state-space. It was a method of the model checking system, and the effectiveness was shown in advance from the software for the hardware. The hardware is suitable for the verification by the combinative search, because it can be formulated in the easiness as a finite state machine. However, the limitless state-space must be limitedly contracted by abstracting the condition, when the state-space of the calculation system is limitless, in order to carry out model checking. Model checking for the state-space abstracted is called "the abstract model inspection". The research purpose is that the abstract model inspection is done central, that the inspection method of the calculation system is researched and that it verifies the distribution system which makes security on the network to be a beginning based on it. Each research results in the fiscal 1999, 2000 and 2001 were shown. |
|
|
|
Related Articles;
|
|
