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

Volume

2

fYear

1997

fDate

28-31 Oct 1997

Firstpage

1847

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Intelligent Processing Systems, 1997. ICIPS '97. 1997 IEEE International Conference on

Conference_Location

Beijing

Print_ISBN

0-7803-4253-4

Type

conf

DOI

10.1109/ICIPS.1997.669377

Filename

669377