VERIFICATION METHOD, VERIFICATION DEVICE, AND VERIFICATION COMPUTER PROGRAM FOR HYBRID SYSTEM; AND MODEL CONVERSION METHOD, MODEL CONVERSION DEVICE, AND MODEL CONVERSION COMPUTER PROGRAM FOR HYBRID SYSTEM

摘要

PROBLEM TO BE SOLVED: To verify a hybrid system by a technique for software verification.SOLUTION: There is provided a verification method for a hybrid system in which a continuous value and a discrete value operate while affecting each other, the verification method including a generation step of generating a model by coding the operation of the hybrid system with a program language, and a verification step of verifying the hybrid system by verifying the code of the model by a program verifier 45 which performs format verification. The program language is a program language in which an infinitesimal can be described. The model has variation in the continuous value of the hybrid system coded using the infinitesimal.