View article

A specification is useless if it cannot be realized by any concrete implementation. There are obvious reasons why it might be unrealizable: it might require the computation of a nonrecursive function, or it might be logically inconsistent. A more subtle danger is specifying the behavior of part of the universe outside the implementor's control. This source of unreaiizability is most likely to infect specifications of concurrent systems or reactive systems [HP85]. It is this source of unrealizability that concerns us.

Formally, a specification is a set of sequences of states, which represents the set of allowed behaviors of a system. We do not distinguish between specifications and programs; a Pascal program and a temporal logic specification are both specifications, although one is at a lower level than the other.(Some may wonder which is the lowerlevel one.) A specification S1 is said to implement a specification S2 iff (if and only if …