One verification methodology involves developing a framework in which users conduct proofs that systems satisfy specifications. Researchers have investigated proof systems for different variants of temporal logic and a variety of behavioral relations, and we briefly review these here.
Traditional temporal-logic-based proof systems rely on proving implications between temporal formulas. To prove a system correct, one first translates it into an ``equivalent'' temporal formula and proves that this formula entails the specification. The virtue of this approach is that one can use (existing) axiomatizations of temporal logic to conduct proofs; the disadvantage is the translation requirement, which usually obscures the structure of the system. More recent proof systems such as UNITY adopt proof rules for specific system notations and temporal logics; other work has been devoted to the development of domain-specific rules for establishing certain classes of properties.
Behavioral-relation-based proof systems have typically been algebraic (hence the term process algebra); in order to prove that two systems are equivalent, one uses equational reasoning. Sound and complete proof system have been devised for a number of different equivalences, preorders, and description languages. Recent work has focused on incorporating reasoning about data into these algebraic proof systems.