VERIFICATION PROPERTY INTEGRATION APPARATUS, VERIFICATION PROPERTY INTEGRATION METHOD, AND STORAGE MEDIUM

摘要

A verification property integration device that enables verification of a product or system integrated by products verified by different formal techniques, such as by formal specification description or model inspection. The apparatus includes a library, a first theorem-proof-assistant description generating unit, and the second theorem-proof-assistant description generating unit. The library is configured to provide definition of semantics of a formal specification description and a model checking description which are to be provided to a theorem-proof-assistant description. The first theorem-proof-assistant description generating unit is configured to translate the formal specification description into a representation on a theorem proof assistant which is defined and to be verified by using the library. The second theorem-proof-assistant description generating unit is configured to translate a model and a temporal logic formula in the model checking description into a representation on the theorem proof assistant which is defined and to be verified by using the library.