Reply to 'Comment on: Development of a safety critical software requirements verification method with combined CPN and PVS: a nuclear power plant protection system application'

摘要

Kim and Cha recently issued a correspondence on an article that we have published. In their correspondence, they pointed out that the translation algorithm from CPN model to PVS specification needs to properly handle initial markings and to correctly reflect the firing rule of the CPN. In addition, Kim and Cha found a few errors such as misuse of timing constraints in the CPN model, wrong variable declaration and incorrect bounding through the quantifier FORALL. Accordingly, we try to reply to their comments and suggest future work to improve our research.