Using formal specification language in industrial software development

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.