On Synchronization and Its Specification
Computer Science (HMC)
We introduce a very high level language for specifying synchronization properties. It is designed using the primitives of temporal logic which facilitates the specification of both invariant and time-dependent properties. The paper begins with a discussion of properties that affect synchronization. The specification language then introduced features constructs to express each of these in a fairly natural and modular fashion. Since the statements in the language have intuitive interpretations, specifications are humanly readable. Also, since they possess appropriate formal semantics, unambiguous specifications result.
Ramamritham, K, Keller, RM. On synchronization and its specification. Lec Notes Comp Sci. 1981;111: 271-282.