Verification property integration apparatus, verification property integration method and verification property integration program

摘要

We provide verification nature integration device, verification property integration method and validation nature integration program which make it possible to verify products and systems combined by products verified using different formal methods such as formal specification description and model checking. A library 13 that defines the format specification description and the semantics of the model check description given to the theorem proving support system description and the first theorem for converting the format specification description to the expression on the theorem proving support system using the library 13 And a second theorem proving support system description generating section 12 for converting the model and the time phase logical expression in the model inspection description into the expression on the theorem proving support system using the certification support system description generating section 11 and the library 13 .