Title :
Using formal specification language in industrial software development
Author :
Hui, Jiang ; Dong, Lin ; Xiren, Xie
Author_Institution :
Dept. of Graduates, Inst. of Commun. Eng., Nanjing, China
Abstract :
Formal specification methods have been widely adopted in recent software development in the industrial field. There exist a variety of specification languages that support it. The article summarizes the advantages of using formal methods in software development, and provides some criteria for selecting an appreciate specification language for a specific application. Two kinds of specification languages are discussed. TLA, which is rooted in logic, emphasizes system correctness and verification, and provides a powerful mechanism to compose specifications and manage specification modules. Larch, which is based on algebra, concentrates on abstract data types (ADT). It uses logic formulas to support reasoning about the data type and checking inconsistencies of design. Through inheritance, large specifications can be composed of separate, smaller specifications
Keywords :
formal specification; formal verification; inheritance; process algebra; specification languages; Larch; abstract data types; algebra; design inconsistency checking; formal specification language; formal specification methods; industrial software development; inheritance; logic; logic formulas; reasoning; specification module management; system correctness; system verification; Algebra; Application software; Communication industry; Computer industry; Energy management; Formal specifications; Ice; Logic; Logic design; Maintenance; Military computing; Power system management; Programming; Specification languages;
Conference_Titel :
Intelligent Processing Systems, 1997. ICIPS '97. 1997 IEEE International Conference on
Conference_Location :
Beijing
Print_ISBN :
0-7803-4253-4
DOI :
10.1109/ICIPS.1997.669377
