Abstract:This paper discusses two approaches to the specification of concurrent sys- terns:temporal logic approach and state machine approach.As a result of this discussion, the authors propose a new kind of formalisms of specification:fair transition system speci- fication(FTSS).This specification approach combines the best features of temporal logic and state machine methods and revises these drawbacks that temporal logic approach USU-ally is complicated and not easy to understand,especially,it fails to be used for "local"properties of concurrent systems.The authors further consider each component of FTSS and get conclusions that FTSS is machine closed and the specification process is consistent and complete.An example of a lossy—transmission protocol shows that the presented ap-proach is simple and easy to understand and to use.At the end of the paper,some applica-tions of FTSS are given.The approach provides a unified framework for program verifics-tion and step—wise refinement of concurrent systems.It has been successfully applied to program verification.