Next: Verification Methodologies and
Up: Specification
Previous: Behavioral Relations.
The chief distinction
between the two specification approaches arises in the amount of information
they require users to specify. Logic-based approaches support very loose
specifications, as one is allowed to identify single properties that systems
should have. Relational approaches require fairly complete specifications of
required observable behavior; in this respect preorders generally allow looser
specifications than equivalences, however. Behavioral relations provide
support for step-wise refinement of systems as well as compositional approaches
to analyzing system behavior, which temporal logics in general do not, since
the specification and system notations differ.
Connections between the two approaches have also been explored. In particular,
a temporal logic induces an equivalence on systems as follows: two system are
equivalent if and only if they satisfy the same formulas. Using this
framework, relationships between different linear- and branching-time logics
and equivalences have been established.
Scott Smolka
Thu Aug 22 10:56:53 EDT 1996