查看文章

This thesis investigates a particular approach, called state-transition specification, to the problem of describing the behavior of modules in a distributed or concurrent computer system. A state-transition specification consists of: (1) a state machine, which incorporates the safety or invariance properties of the module, and (2) validity conditions on the computations of the machine, which capture the desired liveness or eventuality properties.