A specifier's introduction to formal methods

1 September 1990

journal article
Published by Institute of Electrical and Electronics Engineers (IEEE) in Computer

Vol. 23 (9) , 8-22
https://doi.org/10.1109/2.58215

Abstract

Formal methods used in developing computer systems (i.e. mathematically based techniques for describing system properties) are defined, and their role is delineated. Formal specification languages, which provide the formal method's mathematical basis, are examined. Certain pragmatic concerns about formal methods and their users, uses, and characteristics are discussed. Six well-known or commonly used formal methods are illustrated by simple examples. They are Z, VDM, Larch, temporal logic, CSP, and transition axioms.

Keywords

This publication has 53 references indexed in Scilit:

Testing the correctness of tasking supervisors with TSL specifications
Published by Association for Computing Machinery (ACM) ,1989
Formal Verification of the Sobel Image Processing Chip
Published by Springer Nature ,1989
Hierarchical correctness proofs for distributed algorithms
Published by Association for Computing Machinery (ACM) ,1987
Knowledge-based programming: A survey of program design and construction techniques
IEEE Transactions on Software Engineering, 1986
Program specification and development in standard ML
Published by Association for Computing Machinery (ACM) ,1985
The Munich Project CIP
Lecture Notes in Computer Science, 1985
Proving Liveness Properties of Concurrent Programs
ACM Transactions on Programming Languages and Systems, 1982
Hierarchical program specification and verification ? a many-sorted logical approach
Acta Informatica, 1980
Edinburgh LCF
Lecture Notes in Computer Science, 1979
An interactive program verification system
IEEE Transactions on Software Engineering, 1975