Formal verification of RGPS-G
Yang Liu, Jinzhao Wu · 2011
Based on the basic concept of the goal lay of the requirement meta-modeling frame for network software (RGPS-G), this paper advanced a new formal method to guarantee its correctness. The importance of introducing the formal method into RGPS-G was discussed based on the characters of RGPS-G. Theorem proving and model checking had merged in this formal method. Simple formal normative language was used to describe the relation between the subgoals in goal lay. With this formal method, it could automatically discover mistakes in forepart of software development and improve the validity. Also, it could reduce the cost of software development and maintenance.