VERIFICATION PROPERTY INTEGRATION DEVICE, VERIFICATION PROPERTY INTEGRATION METHOD, AND RECORDING MEDIUM HAVING VERIFICATION PROPERTY INTEGRATION PROGRAM STORED THEREIN

摘要

Provided are a verification property integration device, a verification property integration method, and a verification property integration program that enable verification of a product or system coupling products verified by different formal techniques, such as by formal specification description or model inspection. A verification property integration device includes: a library (13) defining the semantics of formal specification description and model inspection description given with respect to a theorem proof assist-system description; a first theorem proof assist-system description generation unit (11) that converts, using the library (13), the formal specification description to an expression in terms of a theorem proof assist system; and a second theorem proof assist-system description generation unit (12) that converts, using the library (13), a model in the model inspection description and a temporal logic formula to an expression in terms of the theorem proof assist system.