| 摘要 |
PROBLEM TO BE SOLVED: To restrain state explosion of a problem at the time when conducting model inspection in verification of a source code. SOLUTION: This source code verification system 200 converts verification-objective source code 100 into a Kripke structure model 300, model-inspects the Kripke structure model 300, and verifies thereby the verification-objective source code 100. The Kripke structure model 300 is generated to eliminate a state not satisfying a condition described in contract information defined about the verification-objective source code 100. COPYRIGHT: (C)2009,JPO&INPIT
|
