Title :
Formal verification of RGPS-G
Author :
Liu, Yang ; Wu, Jinzhao
Author_Institution :
Chengdu Inst. of Comput. Applic., Chinese Acad. of Sci., Chengdu, China
Abstract :
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.
Keywords :
formal verification; software maintenance; theorem proving; RGPS-G software; formal normative language; formal verification; model checking; network software; requirement metamodeling frame; role-goal-process-service-goal; software development; software maintenance; theorem proving; Computational modeling; Helium; ISO; Metamodeling; Presses; Programming; Software; RGPS-G; formal method; model checking; theorem proving;
Conference_Titel :
Computer Science and Service System (CSSS), 2011 International Conference on
Conference_Location :
Nanjing
Print_ISBN :
978-1-4244-9762-1
DOI :
10.1109/CSSS.2011.5974785
