Formal verification of RGPS-G

Author

Liu, Yang ; Wu, Jinzhao

Author_Institution

Chengdu Inst. of Comput. Applic., Chinese Acad. of Sci., Chengdu, China

fYear

2011

fDate

27-29 June 2011

Firstpage

3248

Lastpage

3251

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Computer Science and Service System (CSSS), 2011 International Conference on

Conference_Location

Nanjing

Print_ISBN

978-1-4244-9762-1

Type

conf

DOI

10.1109/CSSS.2011.5974785

Filename

5974785